<html><head></head><body>You've probably heard this before, but `()` and `Void` are often described like the Booleans you refer to, but their algebra is noncommutative. Another interesting Haskell type is `GHC.Exts.Any`.<div style='white-space: pre-wrap'><br>Sent from my phone with K-9 Mail.</div><br><br><div class="gmail_quote">On 10 April 2022 19:26:15 UTC, Olaf Klinke <olf@aatal-apotheke.de> wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<pre dir="auto" class="k9mail"><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #729fcf; padding-left: 1ex;">Dear Olaf,<br><br>On Sat 09 Apr 2022 10:45:56 PM GMT, Olaf Klinke wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #ad7fa8; padding-left: 1ex;">my monograph "Haskell for Mathematicians" has found a home online:<br><a href="https://hub.darcs.net/olf/haskell_for_mathematicians">https://hub.darcs.net/olf/haskell_for_mathematicians</a><br></blockquote><br>I just had a first look, your monograph looks awesome! Thank you for<br>sharing!<br><br>In haskell_for_mathematicians.tex, you mention as a further idea that<br>Hask is like a Heyting algebra. Could you elaborate on that point? Are<br>you thinking of types as propositions here?<br><br>Cheers,<br>Ingo<br></blockquote><br>Hi Ingo,<br><br>Types as propositions is dealt with in haskell_for_logicians.lhs. <br>Hask has an arrow that is a right adjoint, just like a Heyting algebra. It <br>is less clear, however, whether the the arrow gives rise to a partial <br>order as it does in Heyting algebras. I am interested in the complete <br>Heyting algebras, a.k.a. frames a.k.a. locales. Many concepts in <br>point-free topology heavily rely on partial orders and lattice theory, so <br>without a good analogue I would not dare declare a similarity.<br>For example, in a Heyting algebra x <= y iff x -> y equals the top <br>element.<br>But then, what is the top element of Hask? Do we declare x <= y if x -> y <br>is inhabited? That seems to collapse all inhabited types.<br><br>In a future chapter I would like to tell a story around this:<br>In point-free topology (locale theory), there are several inter-definable <br>concepts of sub-object. One of them is a "nucleus", that is an <br>endo-function j with the following properties. <br>x <= y implies j(x) <= j(y) (j is a functor)<br>x <= j(x) (return :: x -> j x)<br>j(j(x)) <= j(x) (join :: j (j x) -> j x)<br>j(x) /\ j(y) <= j(x /\ y) (liftM2 (,) :: j x -> j y -> j (x,y))<br><br>In other words: sub-objects of point-free spaces are (strong) monads.<br>In that respect, every monad j is a sub-object of Hask, and indeed it is: <br>It defines the sub-category (Kleisli j). There are more analogues: The <br>identity function is a nucleus and corresponds to the greatest sub-object, <br>and in Hask (Kleisli Identity) is the largest Kleisli category. Nuclei can <br>not be combined easily, and neither can monads.<br><br>Another interesting question is: What are the "points" of Hask? A point of <br>a locale is a mapping from opens (types of Hask) to Bool that preserves <br>finite products and arbitrary coproducts, where True is considered as the <br>empty product and False as the empty coproduct. How many of such mappings <br>can be defined in Haskell? How would we implement them? As a class? Type <br>family? GADT? <br>The funny thing about locales is that one can have few or no points but <br>still a rich supply of sub-objects.<br><br>Olaf<hr>Haskell-Cafe mailing list<br>To (un)subscribe, modify options or view archives go to:<br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>Only members subscribed via the mailman list are allowed to post.</pre></blockquote></div></body></html>