什么是Haskell的DataKinds扩展？

问题描述

我试图找到DataKinds扩展的解释，这对我来说只有阅读才有意义。是否有一个标准的源代码可以帮助我理解我所学到的知识？

编辑：例如称：

并给出示例

 数据Nat = Ze | Su Nat 
  

产生以下类型和类型的构造函数：

  Nat :: BOX 
 Ze :: Nat 
 Su :: Nat  - > Nat 
  

我不明白这一点。虽然我不明白 BOX 是什么意思，但是 Ze :: Nat 和 Su :: Nat - > Nat 似乎表明Ze和Su是正常的数据构造函数，正如你期望用ghci看到的一样。

 前奏> ：t Su 
 Su :: Nat  - > Nat 
  

解决方案

那么让我们从基础开始吧

种类

种类是种类型*，例如

  Int :: * 
 Bool :: * 
也许:: *  - > * 
  

注意 - > 过载也意味着在种类层面上的功能。所以 * 是一种普通的Haskell类型。

我们可以要求GHCi打印某种东西：k 。

数据种类

不是很有用，因为我们无法做出自己的种类！使用 DataKinds 时，当我们写入时

 数据Nat = S Nat | z 
  

GHC将促进这一点，以创建相应的类别 Nat 和

  S :: Nat  - > Nat 
 Z :: Nat 
  

因此 DataKind

使用

让我们来做一个使用GADTs的原型示例

 数据Vec :: Nat  - > *其中
无:: Vec Z 
缺点::诠释 - > Vec n  - > Vec（S n）
  

现在我们看到我们的 Vec b
$ b

这是基本的10k尺的概览。

**这个实际上， Values：Types：Kinds：Sorts ... 有些语言（Coq，Agda ..）支持这个无限的宇宙堆栈，但Haskell将所有东西都归入一类。

I am trying to find an explanation of the DataKinds extension that will make sense to me having come from only having read Learn You a Haskell. Is there a standard source that will make sense to me with what little I've learned?

Edit: For example the documentation says

and gives the example

data Nat = Ze | Su Nat

give rise to the following kinds and type constructors:

Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat

I am not getting the point. Although I don't understand what BOX means, the statements Ze :: Nat and Su :: Nat -> Nat seem to state what is already normally the case that Ze and Su are normal data constructors exactly as you would expect to see with ghci

Prelude> :t Su
Su :: Nat -> Nat

解决方案

Well let's start with the basics

Kinds

Kinds are the types of types*, for example

Int :: *
Bool :: *
Maybe :: * -> *

Notice that -> is overloaded to mean "function" at the kind level too. So * is the kind of a normal Haskell type.

We can ask GHCi to print the kind of something with :k.

Data Kinds

Now this not very useful, since we have no way to make our own kinds! With DataKinds, when we write

 data Nat = S Nat | Z

GHC will promote this to create the corresponding kind Nat and

 S :: Nat -> Nat
 Z :: Nat

So DataKinds makes the kind system extensible.

Uses

Let's do the prototypical kinds example using GADTs

 data Vec :: Nat -> * where
    Nil  :: Vec Z
    Cons :: Int -> Vec n -> Vec (S n)

Now we see that our Vec type is indexed by length.

That's the basic, 10k foot overview.

** This actually continues, Values : Types : Kinds : Sorts ... Some languages (Coq, Agda ..) support this infinite stack of universes, but Haskell lumps everything into one sort.

这篇关于什么是Haskell的DataKinds扩展？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！