使用数据种类在类型签名中绑定名称

Question

所以，我终于找到了一个可以使用新的DataKinds扩展（使用 ghc 7.4.1）的任务。这是我正在使用的Vec：

data Nat = Z | S Nat deriving (Eq, Show)
data Vec :: Nat -> * -> * where
    Nil :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

现在，为了方便起见，我想实现fromList.简单的递归/折叠基本上没有问题 - 但我无法弄清楚如何给它正确的类型。作为参考，这是阿格达版本：

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)

我的Haskell方法，使用我在这里看到的语法：

fromList :: (ls :: [a]) -> Vec (length ls) a
fromList [] = Nil 
fromList (x:xs) = Cons x (fromList xs)

这给了我一个parse error on input 'a'.我发现的语法是否正确，还是他们改变了它？我还在链接的代码中添加了一些扩展，这也无济于事（目前我有GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances）。

我

的另一个怀疑是我只是不能绑定多态类型，但我对此的测试：

bla :: (n :: Nat) -> a -> Vec (S n) a
bla = undefined

也失败了，Kind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat'（真的不知道这意味着什么）。

谁能帮我提供一个工作版本的fromList并澄清其他问题？不幸的是，DataKinds还没有很好的记录，似乎假设使用它的每个人都有深厚的类型理论知识。

Answer 1

与 Agba 不同，Haskell 没有依赖类型，因此无法完全按照自己的意愿进行操作。 类型不能按值参数化，因为 Haskell 强制在运行时和编译时之间划分阶段。 DataKinds在概念上的工作方式实际上非常简单：数据类型提升为类型（类型类型），数据构造函数提升为类型。

 fromList :: (ls :: [a]) -> Vec (length ls) a

有几个问题：(ls :: [a])没有真正的意义（至少当你只是通过提升伪造依赖类型时），length是一个类型变量而不是一个类型函数。 你想说的是

 fromList :: [a] -> Vec ??? a

其中???是列表的长度。 问题是你无法在编译时获取列表的长度......所以我们可以尝试

 fromList :: [a] -> Vec len a

但这是错误的，因为它说fromList可以返回任何长度的列表。 相反，我们想说的是

 fromList :: exists len. [a] -> Vec len a

但哈斯克尔不支持这一点。 相反

 data VecAnyLength a where
     VecAnyLength :: Vec len a -> VecAnyLength a 
 cons a (VecAnyLength v) = VecAnyLength (Cons a v)
 fromList :: [a] -> VecAnyLength a
 fromList []     = VecAnyLength Nil
 fromList (x:xs) = cons x (fromList xs)

实际上，您可以通过模式匹配来使用VecAnyLength，从而获得（本地）依赖于伪的类型值。

同样地

bla :: (n :: Nat) -> a -> Vec (S n) a

不起作用，因为 Haskell 函数只能接受*类型的参数。 相反，您可以尝试

data HNat :: Nat -> * where
   Zero :: HNat Z
   Succ :: HNat n -> HNat (S n)
bla :: HNat n -> a -> Ven (S n) a

甚至可以定义

bla Zero a     = Cons a Nil
bla (Succ n) a = Cons a (bla n a)

Answer 2

你可以在这里使用一些typeclass魔法（参见HList了解更多信息）：

{-# LANGUAGE GADTs, KindSignatures, DataKinds, FlexibleInstances
  , NoMonomorphismRestriction, FlexibleContexts #-}
data Nat = Z | S Nat deriving (Eq, Show)
data Vec :: Nat -> * -> * where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a
instance Show (Vec Z a) where
  show Nil = "."
instance (Show a, Show (Vec m a)) => Show (Vec (S m) a) where
  show (Cons x xs) = show x ++ " " ++ show xs
class FromList m where
  fromList :: [a] -> Vec m a
instance FromList Z where
  fromList [] = Nil
instance FromList n => FromList (S n) where
  fromList (x:xs) = Cons x $ fromList xs
t5 = fromList [1, 2, 3, 4, 5]

但这并不能真正解决问题：

> :t t5
t5 :: (Num a, FromList m) => Vec m a

列表是在运行时形成的，它们的长度在编译时是未知的，所以编译器无法推断t5的类型，必须显式指定：

*Main> t5
<interactive>:99:1:
    Ambiguous type variable `m0' in the constraint:
      (FromList m0) arising from a use of `t5'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: t5
    In an equation for `it': it = t5
*Main> t5 :: Vec 'Z Int
*** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList
*Main> t5 :: Vec ('S ('S ('S 'Z))) Int
1 2 3 *** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList
*Main> t5 :: Vec ('S ('S ('S ('S ('S 'Z))))) Int
1 2 3 4 5 .
*Main> t5 :: Vec ('S ('S ('S ('S ('S ('S ('S 'Z))))))) Int
1 2 3 4 5 *** Exception: /tmp/d.hs:23:3-40: Non-exhaustive patterns in function fromList

具有依赖类型的语言具有从术语到类型的映射，类型也可以在运行时动态形成，因此不存在此问题。

Answer 3

在前面的答案之上：

• 价值级别，从[a]到exist n. Vec n a

值

• 到类型化值，从[a]到Vec 5 a，您必须在其中提供特定的n。

第一个变换的变体，如下所示

reify :: [a] -> (forall (n::Nat). Proxy n -> Vec n a -> w) -> w
reify [] k = k (Proxy @ 'Z) Nil
reify (x:xs) k = reify xs ((_ :: Proxy n) v -> k (Proxy @ ('S n)) (Cons x v))

它仍然从值[a]变为类型化值Vec n a其中n被（静态）量化。这类似于VecAnyLength方法，没有引入实际的数据类型来执行量化。

这里的proxy是将n显式为Nat。 它可以从代码中删除并n保持沉默，仅出现在类型 Vec n a 中，而不是像在 Proxy @ ('S n) 中那样提供给构造的值。