我从Haskell中的基本类型级编程学习Haskell的类型编程,但是当它引入DataKinds扩展时,这个例子似乎有些令人困惑:
{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat
现在,Nat升职Kind,没关系.但如何Zero和Succ？
我尝试从GHCi获取一些信息,所以我键入:
:kind Zero
它给
Zero :: Nat
没关系,Zero是一种类型Nat,对吗？我尝试:
:type Zero
它仍然给出:
Zero :: Nat
这意味着Zero有类型Nat,这是不可能的,因为Nat是一种不是类型,对吗？难道Nat是这两个类型和种类？
而其他令人困惑的事情是,上面的博客也提到,在创建Nat种类时,有两种新类型:'Zero并且'Succ是自动创建的.当我再次从GHCi尝试时:
:kind 'Zero
给
'Zero :: Nat
和
:type 'Zero
给
Syntax error on 'Zero
好的,它证明这'Zero是一种类型.但是创造'Zero和' …