使用haskell的单例,我怎么能写`fromList :: [a] - > Vec an`？

Question

作为理解之旅的一部分,我singletons试图弥合编译时安全性与将运行时值提升到相关类型安全性之间的差距.

我认为,"运行时"值的最小示例是一个采用无界列表的函数,并将其转换为大小索引的向量.以下骨架提供了长度索引向量,但我无法确定如何编写fromList.

我已经考虑过使函数采用size参数,但我怀疑它可以保持隐含.

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeInType           #-}
{-# LANGUAGE UndecidableInstances #-}

import           Data.Singletons
import           Data.Singletons.TH

$(singletons
  [d|
    data Nat = Z | S Nat deriving (Show)
  |])

data Vec a n where
  Nil :: Vec a Z
  Cons :: a -> Vec a n -> Vec a (S n)

instance Show a => Show (Vec a n) where
  show Nil = "Nil"
  show (Cons x xs) = show x ++ " :< " ++ show xs

fromListExplicit :: forall (n :: Nat) a. SNat n -> [a] -> Vec a n
fromListExplicit SZ _ = Nil
fromListExplicit (SS n) (x : xs) = Cons x (fromListExplicit n xs)

ex1 = fromListExplicit (SS (SS (SS SZ))) [1..99]
-- 1 :< 2 :< 3 :< Nil

fromListImplicit :: (?????) => [a] -> Vec a n
fromListImplicit = ?????

main :: IO ()
main = do
  xs <- readLn :: IO [Int]
  print $ fromListImplicit xs

Answer 1

这是不是可以使用哈斯克尔因为Haskell中还没有完全依赖类型(虽然GHC 将来可能).请注意

fromList :: [a] -> Vec a n

有两个a并且n普遍量化,这意味着用户应该能够选择他们n并获得Vec正确的大小.这是没有意义的!诀窍是n用户无法真正选择 - 它必须是输入列表的长度.(出于同样的原因,fromList :: Integer -> [a] -> Vec a n不会有任何用处 - 大小提示必须是类型级别的.)

寻找像Idris这样的依赖类型的语言,你可以定义

fromList : (l : List elem) -> Vec (length l) elem

事实上,他们在标准库中定义了这一点.

那么,什么可以做什么？没有说它Vec的长度等于输入列表的大小(需要将"输入列表的长度"提升到类型级别),你可以说它有一定的长度.

data SomeVec a where { SomeVec :: Vec a n -> SomeVec a }

list2SomeVec :: [a] -> SomeVec a
list2SomeVec [] = SomeVec Nil
list2SomeVec (x:xs) = case list2SomeVec xs of
                        SomeVec ys -> SomeVec (x `Cons` ys)

这并不是非常有用,但总比没有好.