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
I found this interesting page https://wiki.haskell.org/Peano_numbers 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