The first definition is only used as an analogy, it’s a way to represent Peano numbers as values.

The second definition is only related to the first in that it uses the same concept. It is not a breakdown of the first one, it is a completely separate (and incompatible) way to represent Peano numbers at the type level (and only as types, notice there are no constructors). You can not define both of these in the same module with the same names.

In Haskell a kind is (basically) the type of a type. In modern GHC to make it even more clear (and to free up * for type operators) you can say Type instead of *.

Zero has the kind Type (or *) because it has no arguments, just like Zero has the type Peano because the constructor has no arguments.

Succ has the kind Type -> Type because you pass it a Type as an argument to get a concrete Type. Maybe also has the kind Type -> Type, as does [].

Generally, beginner Haskell doesn’t use any of this type level programming. If this is a topic of interest, I recommend this book:

https://thinkingwithtypes.com

On Fri, Mar 12, 2021 at 22:19 Galaxy Being <borgauf@gmail.com> wrote:

I found this interesting page at Wiki Haskell. Confusing, however, is how it first establishes

data Peano = Zero | Succ Peano

It says

Here Zero and Succ are values (constructors). Zero has type Peano,
and Succ has type Peano -> Peano.

but then it breaks down each member further a few lines later

data Zero
data Succ a

and then says

Zero has kind *, and Succ has kind * -> *. The natural numbers are represented by types (of kind *) Zero, Succ Zero, Succ (Succ Zero) etc.

Why is it giving two separate treatments and what is meant by the * and * -> * ? There's something fundamental I'm missing.

If anyone knows of a really thorough and definitive and understandable treatment of Haskell types, I'd appreciate it.

LB
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners