<div dir="ltr">This is great stuff. I thank everybody.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Mar 14, 2021 at 5:42 AM Erik Dominikus <<a href="mailto:erik.dominikus71@gmail.com">erik.dominikus71@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"><div>> There's something fundamental I'm missing.</div><div><br></div><div>It is not necessarily true, but useful, to think that:</div><div><br></div><div>- A <i>type is</i> a set of values.</div><div>- A <i>kind</i> as a set of types.</div><div><div>- The <i>kind</i> * is the set of all types.</div><div>- The <i>kind</i> * -> * is the set of every function with domain * and codomain *.<br></div><div>- The <i>type</i> T -> U is the set of every function with domain T and codomain U, if each of T and U is a type (a set of values).</div></div><div><br></div><div>For example:</div><div><br></div><div>- The type <b>Bool</b> is the set {False, True}.</div><div>- The type <b>Maybe Bool</b> is the set {Nothing, Just False, Just True}.</div><div>- <b>Maybe</b> is a function such that Maybe(T) = { Nothing } union { Just t | t in T }.</div><div>- <b>Maybe</b> is not a type; <b>Maybe Bool</b> is a type.</div><div>- <b>a -> a</b> is the set { \ x -> x }.</div><div><br></div><div>Currying and application can happen at both the value level and the type level:<br></div><div><br></div><div>- The kind of <b>Either</b> is <b>* -> * -> *</b>.<br></div><div>- The kind of <b>Either a</b> is <b>* -> *</b>, if the kind of <b>a</b> is <b>*</b>.<br></div><div>- The kind of <b>Either a b</b> is <b>*</b>, if the kind of <b>a</b> is <b>*</b> and the kind of <b>b</b> is <b>*</b>.<br></div><div><div></div><div>- The type of <b>Just</b> is <b>a -> Maybe a</b>.<br></div></div><div><div>- The type of <b>Just x</b> is <b>Maybe a</b>, if the type of <b>x</b> is <b>a</b>.</div></div><div><br></div><div>> Why is it giving two separate treatments?<br></div><div><br></div><div>It is to show the various ways one <b>can</b> implement/represent/realize/concretize/encode/model a mathematical construction in Haskell.</div><div><br></div><div>You <b>can</b> (do type-level programming in Haskell, use all features of C++, eat spaghetti with a straw, etc.), but the real question has always been: <b>should</b> you?</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>If you mean Haskell 98, then the Haskell 98 Report [1] (especially Chapter 4) seems "thorough and definitive", but I don't know whether you will find it "understandable".<div><br></div><div>If you mean the latest Haskell as implemented by GHC, I don't know.<br><div><br></div><div>[1] <a href="https://www.haskell.org/onlinereport/" target="_blank">https://www.haskell.org/onlinereport/</a></div><div></div></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>