使用DataKind在类型签名中绑定名称

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.简单的递归/折叠基本上没有问题 - 但我无法弄清楚如何给它正确的类型.作为参考,这是Agda版本:

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

与Agda不同,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

但是Haskell并不支持这一点.代替

 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)