<div dir="ltr">Thanks for the book recommendation!<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Mar 12, 2021 at 11:52 PM Bob Ippolito <<a href="mailto:bob@redivi.com">bob@redivi.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="auto">The first definition is only used as an analogy, it’s a way to represent Peano numbers as values.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">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 *.</div><div dir="auto"><br></div><div dir="auto">Zero has the kind Type (or *) because it has no arguments, just like Zero has the type Peano because the constructor has no arguments.</div><div dir="auto"><br></div><div dir="auto">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 [].</div><div dir="auto"><br></div><div dir="auto">Generally, beginner Haskell doesn’t use any of this type level programming. If this is a topic of interest, I recommend this book: <div><a href="https://thinkingwithtypes.com" target="_blank">https://thinkingwithtypes.com</a></div></div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Mar 12, 2021 at 22:19 Galaxy Being <<a href="mailto:borgauf@gmail.com" target="_blank">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 style="font-family:monospace;color:rgb(0,0,0)" face="monospace">data Peano = Zero | Succ Peano<br></font></div><div><font style="font-family:monospace;color:rgb(0,0,0)" face="monospace"><br></font></div><div><font style="font-family:arial,sans-serif;color:rgb(0,0,0)" face="arial, sans-serif">It says</font></div><div><font style="font-family:arial,sans-serif;color:rgb(0,0,0)" face="arial, sans-serif"><br></font></div><div>Here <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Zero</font> and <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Succ</font> are values (constructors). <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Zero </font>has type <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Peano</font>, </div><div>     and <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Succ</font> has type <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Peano -> Peano</font>. <font style="font-family:arial,sans-serif;color:rgb(0,0,0)" 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 style="font-family:monospace;color:rgb(0,0,0)" face="monospace">data Zero<br>data Succ a<br></font></div><div><br></div><div>and then says </div><div><br></div><div><font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Zero </font>has kind <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">*</font>, and <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">Succ </font>has kind <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">* -> *</font>. The natural numbers are represented by types (of kind <font style="font-family:monospace;color:rgb(0,0,0)" face="monospace">*</font>) <font style="font-family:monospace;color:rgb(0,0,0)" 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 style="font-family:monospace;color:rgb(0,0,0)" face="monospace">*</font> and <font style="font-family:monospace;color:rgb(0,0,0)" 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></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>