使用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还没有很好的文档记录，似乎假设每个使用它的人都有深厚的类型理论知识。
回答 3
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)Stack Overflow用户
发布于 2012-06-28 21:09:23
你可以在这里使用一些类型类魔术(更多信息请参见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带有依赖类型的语言有从术语到类型的映射，类型也可以在运行时动态形成，所以这个问题不存在。
Stack Overflow用户
发布于 2019-01-10 18:39:24
在前面的答案之上：
- 值级别，从
[a]到exist n. Vec n a - value到类型值，从
[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)中那样提供给构造的值。
https://stackoverflow.com/questions/11243227
复制相似问题
腾讯云开发者
