使用DataKind在类型签名中绑定名称 [英] Binding name in type signature using DataKind

问题描述

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

 数据Nat = Z | S Nat推导（Eq，Show）
 
数据Vec :: Nat  - > *  - > *其中
无:: Vec Z a 
缺点:: a  - > Vec n a  - > Vec（S n）a 
  

现在，为了方便起见，我想实现 fromList 。基本上没有问题简单的递归/折叠 - 但我不知道如何给它正确的类型。作为参考，这是Agda版本：

  fromList：∀{a} {A：Set a}→（xs：List A）→Vec A（List.length xs）
  

我使用Haskell方法， a href =http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinion-constraints-contexts-td5689436.html =nofollow noreferrer> here a>：

  fromList ::（ls :: [a]） - > Vec（length ls）a 
 fromList [] =无
 fromList（x：xs）= Cons x（from List xs）
  

这给我输入'a'的一个解析错误。我发现的语法甚至是正确的，还是他们改变了它？我还在链接的代码中添加了一些更多的扩展，这些扩展并没有帮助（目前我有 GADT，DataKinds，KindSignatures，TypeOperators，TypeFamilies，UndecidableInstances ） 。



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



  bla ::（n :: Nat） - > a  - > Vec（S n）a 
 bla =未定义
  

也失败了，种类不符合预期种类'ArgKind'，但'n'种类'Nat'（实际上并不知道这意味着什么）。



任何人都可以帮我使用 fromList 的工作版本，并澄清其他问题吗？不幸的是， DataKinds 没有被很好地记录下来，似乎认为每个人都使用它有深刻的类型理论知识。

解决方案

Haskell和Agda不同，没有依赖类型，所以没有办法做到你想要的东西。类型不能通过值来参数化，因为Haskell在运行时和编译时间之间强制执行相位区分。在概念上， DataKinds 的工作方式实际上非常简单：数据类型被提升为种类（类型），数据构造函数被提升为类型。



  fromList ::（ls :: [a]） - > Vec（长度ls）a 
  

有两个问题：（ls： ：[a]）没有任何意义（至少当你只是用升级来伪装依赖类型时）， length 是一个类型变量而不是一个类型函数。你想说的是：



  fromList :: [a]  - > Vec？ a 
  

其中 ??? 是长度的名单。问题是你没有办法在编译时获得列表的长度......所以我们可以尝试从$ List



  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无
 fromList（x：xs）= cons x（fromList xs）
  

你可以通过模式匹配实际使用 VecAnyLength ，从而得到一个（局部）伪随机的类型值。

同样，

  bla ::（n :: Nat） - > a  - > Vec（S n）a 
  

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

  data HNat :: Nat  - > *其中
 Zero :: HNat Z 
 Succ :: HNat n  - > HNat（S n）
 
 bla :: HNat n  - > a  - > Ven（S n）a 
  

甚至可以定义

  bla零a =缺一个
 bla（Succ n）a =缺一个（不详）
  pre> 
So, I finally found a task where I could make use of the new DataKinds extension (using ghc 7.4.1). Here's the Vec I'm using:
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
Now, for convenience I wanted to implement fromList. Basically no problem with simple recursion/fold -- but I can't figure out how to give it the correct type. For reference, this is the Agda version:
fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)
My Haskell approach, using the syntax I saw here:
fromList :: (ls :: [a]) -> Vec (length ls) a
fromList [] = Nil 
fromList (x:xs) = Cons x (fromList xs)
This gives me a parse error on input 'a'. Is the syntax I found even correct, or have they changed it? I also added some more extensions which are in the code in the link, which didn't help either (currently I have GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances).

My other suspicion was that I just can't bind polymorphic types, but my test for this:
bla :: (n :: Nat) -> a -> Vec (S n) a
bla = undefined
failed, too, with Kind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat' (don't really know what that means).

Could anyone help me with a working version of fromList and also clarify the other issues? Unfortunately, DataKinds isn't documented very well yet and seems to assume that everybody using it has profound type theory knowledge. 
解决方案
Haskell, unlike Agda, does not have dependent types, so there is no way to do exactly what you want.  Types cannot be parameterized by value, since Haskell enforces a phase distinction between runtime and compile time.  The way DataKinds works conceptually is actually really simple: data types are promoted to kinds (types of types) and data constructors are promoted to types.  
 fromList :: (ls :: [a]) -> Vec (length ls) a
has a couple of problems: (ls :: [a]) does not really make sense (at least when you are only faking dependent types with promotion), and length is a type variable instead of a type function.  What you want to say is
 fromList :: [a] -> Vec ??? a
where ??? is the length of the list.  The problem is that you have no way of getting the length of the list at compile time... so we might try
 fromList :: [a] -> Vec len a
but this is wrong, since it says that fromList can return a list of any length.  Instead what we want to say is
 fromList :: exists len. [a] -> Vec len a
but Haskell does not support this.  Instead
 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)
you can actually use a VecAnyLength by pattern matching, and thus getting a (locally) psuedo-dependently typed value.

similarly, 
bla :: (n :: Nat) -> a -> Vec (S n) a
does not work because Haskell functions can only take arguments of kind *.  Instead you might try
data HNat :: Nat -> * where
   Zero :: HNat Z
   Succ :: HNat n -> HNat (S n)

bla :: HNat n -> a -> Ven (S n) a
which is even definable
bla Zero a     = Cons a Nil
bla (Succ n) a = Cons a (bla n a)


                        
这篇关于使用DataKind在类型签名中绑定名称的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！