使用DataKind的类型签名中的绑定名称
所以，我终于找到了一个可以使用新的DataKinds扩展(使用GHC7.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方法，使用我看到的here语法
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 = undefinedKind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat'也失败了(我真的不知道这是什么意思)。
有没有人能帮我弄清楚fromList的工作版本和其他问题？不幸的是，DataKinds还没有很好的文档记录，似乎假设每个使用它的人都有深厚的类型理论知识。
Stack Overflow用户
发布于 2012-06-28 19:50:32
与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)https://stackoverflow.com/questions/11243227
复制相似问题
腾讯云开发者
