什么是Haskell的DataKinds扩展? [英] What is the DataKinds extension of Haskell?
问题描述
我试图找到DataKinds扩展的解释,这对我来说只有阅读学习你一个Haskell 才有意义。是否有一个标准的源代码可以帮助我理解我所学到的知识?
编辑:例如文档称:
-XDataKinds,GHC自动提升每个合适的数据类型
是一种类型,它的(值)构造函数是类型构造函数。
以下类型
并给出示例
数据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
因此 让我们来做一个使用GADTs的原型示例 现在我们看到我们的 这是基本的10k尺的概览。 **这个实际上, 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 With -XDataKinds, GHC automatically promotes every suitable datatype
to be a kind, and its (value) constructors to be type constructors.
The following types and gives the example give rise to the following kinds and type constructors: I am not getting the point. Although I don't understand what
Well let's start with the basics Kinds are the types of types*, for example Notice that We can ask GHCi to print the kind of something with Now this not very useful, since we have no way to make our own kinds! With GHC will promote this to create the corresponding kind So Let's do the prototypical kinds example using GADTs Now we see that our That's the basic, 10k foot overview. ** This actually continues, 这篇关于什么是Haskell的DataKinds扩展?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋! DataKind $ c
使用
数据Vec :: Nat - > *其中
无:: Vec Z
缺点::诠释 - > Vec n - > Vec(S n)
Vec $ c $ b> b
$ b
Values:Types:Kinds:Sorts ...
有些语言(Coq,Agda ..)支持这个无限的宇宙堆栈,但Haskell将所有东西都归入一类。
data Nat = Ze | Su Nat
Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat
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 ghciPrelude> :t Su
Su :: Nat -> Nat
Kinds
Int :: *
Bool :: *
Maybe :: * -> *
->
is overloaded to mean "function" at the kind level too. So *
is the kind of a normal Haskell type.:k
.Data Kinds
DataKinds
, when we write data Nat = S Nat | Z
Nat
and S :: Nat -> Nat
Z :: Nat
DataKind
s makes the kind system extensible.Uses
data Vec :: Nat -> * where
Nil :: Vec Z
Cons :: Int -> Vec n -> Vec (S n)
Vec
type is indexed by length.Values : Types : Kinds : Sorts ...
Some languages (Coq, Agda ..) support this infinite stack of universes, but Haskell lumps everything into one sort.