本文介绍了什么是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扩展?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!

08-14 18:22