<div dir="ltr"><div>I can only answer some of your questions.</div><div><br></div><div>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.</div><div><br></div><div>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:</div><div><br></div><div><font face="monospace">data PeanoT = Zero | Succ PeanoT</font></div><div><font face="monospace"><br></font></div><div><font face="monospace"><font face="arial,sans-serif">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.</font></font></div><div><font face="monospace"><font face="arial,sans-serif"><br></font></font></div><div><font face="monospace"><font face="arial,sans-serif">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):</font></font></div><div><font face="monospace"><font face="arial,sans-serif"><br></font></font></div><div><font face="monospace"><font face="arial,sans-serif"><font face="monospace">data ZeroT</font></font></font></div><div><font face="monospace"><font face="arial,sans-serif"><font face="monospace">data SuccT a</font></font></font></div><div><font face="monospace"><font face="arial,sans-serif"><font face="monospace"><br></font></font></font></div><div><font face="monospace"><font face="arial,sans-serif"><font face="monospace"><font face="arial,sans-serif">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.</font></font></font></font><br></div><div><br></div><div>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 <i>type</i> to SuccT to get a concrete type.</div><div><br></div><div>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,</div><div><br></div><div><font face="monospace">data K3T a b</font></div><div><font face="monospace"><br></font></div><div><font face="monospace"><font face="arial,sans-serif">has kind * -> * -> * (you have to provide two concrete types for 'a' and 'b' to get out a concrete type).</font></font><br></div><div><br></div><div>I don't have any good references for formal type theory stuff, but I found <a href="https://haskellbook.com/">https://haskellbook.com/</a> 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.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Mar 12, 2021 at 11:18 PM Galaxy Being <<a href="mailto:borgauf@gmail.com">borgauf@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">I found <a href="https://wiki.haskell.org/Peano_numbers" target="_blank">this interesting page</a> at Wiki Haskell. Confusing, however, is how it first establishes <div><br></div><div><font face="monospace">data Peano = Zero | Succ Peano<br></font></div><div><font face="monospace"><br></font></div><div><font face="arial, sans-serif">It says</font></div><div><font face="arial, sans-serif"><br></font></div><div>Here <font face="monospace">Zero</font> and <font face="monospace">Succ</font> are values (constructors). <font face="monospace">Zero </font>has type <font face="monospace">Peano</font>, </div><div>     and <font face="monospace">Succ</font> has type <font face="monospace">Peano -> Peano</font>. <font face="arial, sans-serif"><br></font></div><div><br></div><div>but then it breaks down each member further a few lines later</div><div><br></div><div><font face="monospace">data Zero<br>data Succ a<br></font></div><div><br></div><div>and then says </div><div><br></div><div><font face="monospace">Zero </font>has kind <font face="monospace">*</font>, and <font face="monospace">Succ </font>has kind <font face="monospace">* -> *</font>. The natural numbers are represented by types (of kind <font face="monospace">*</font>) <font face="monospace">Zero, Succ Zero, Succ (Succ Zero)</font> etc.<br></div><div><br></div><div>Why is it giving two separate treatments and what is meant by the <font face="monospace">*</font> and <font face="monospace">* -> * </font>? There's something fundamental I'm missing.</div><div><br></div><div>If anyone knows of a really thorough and definitive <i>and </i>understandable treatment of Haskell types, I'd appreciate it.</div><div><br></div><div>LB</div></div>
_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br>
</blockquote></div>