haskell - 使用haskell的单例，如何编写 `fromList::[a] -> Vec a n` ？

Question

作为我理解单例旅程的一部分，我试图弥合编译时安全性和将运行时值提升到依赖类型安全性之间的差距。

我认为“运行时”值的一个最小示例是一个接受无界列表并将其转换为大小索引向量的函数。以下骨架提供了长度索引向量，但我无法完全确定如何编写 fromList。

我考虑过让函数采用大小参数，但我怀疑可以保持隐式。

{-# 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 不可能实现这一点，因为 Haskell 还没有完全的依赖类型(尽管 GHC might in the future )。请注意

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

事实上他们 define this in the standard library .

那么，您可以做什么？不用说 Vec 的长度等于输入列表的大小(这需要将“输入列表的长度”提升到类型级别)，您可以说它有 some 长度。

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)

这并不是很有用，但总比没有好。