I can only answer some of your questions.

To start, perhaps an analogy would help: Kinds are to types as types are to values. So in regards to the title of the thread, "Type * and * -> *" is confused in that * and * -> * are kinds, not types.

That might not exactly make sense, but leaving it aside for the moment, to two treatments are at different levels - data and type level. I'll try to be explicit as to what are type constructors and what are data constructors by appending T to the type constructors:

data PeanoT = Zero | Succ PeanoT

In the first treatment, we define a type PeanoT. This is the type you would use in function signatures, etc. At the term / values level, we can construct values of type PeanoT through either the 'Zero' or 'Succ' data constructors.

The second treatment encodes the Peano numbers at the type level, not value level - note that both lines are type constructors (both lacking corresponding data constructors):

data ZeroT
data SuccT a

I'm a little bit at my limit of type level programming in haskell, so I'm not 100% sure about this, but in the second treatment, without any data constructors, I don't think there is any way to actually construct a run-time value with either of these types. You can only use them at the type level.

Back to the analogy: In the first treatment, we can construct values of type PeanoT through either `Zero :: PeanoT` or `Succ :: PeanoT -> PeanoT`, data constructors of the given type. In the second treatment, we have two types. But similar to how we have to provide a value of type PeanoT to Succ to create the final PeanoT type, we have to provide a type to SuccT to get a concrete type.

Now while there are a great many types, I believe at the kind level we only really care if we have a concrete type ('ZeroT, of kind *), or a type constructor that needs to be applied to concrete type to actually construct the type (kind * -> *). For example,

data K3T a b

has kind * -> * -> * (you have to provide two concrete types for 'a' and 'b' to get out a concrete type).

I don't have any good references for formal type theory stuff, but I found https://haskellbook.com/ to be the resource that got me over the various failed attempts at learning haskell. It stops a bit short of type level programming, but does a good job distinguishing between data constructors and type constructors, and makes the analogy for how kinds arise when you take that 'one level up'. Also its not free.

On Fri, Mar 12, 2021 at 11:18 PM 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