[Haskell-cafe] ANN: haskell for mathematicians

[Keith]

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`.

Sent from my phone with K-9 Mail.

On 10 April 2022 19:26:15 UTC, Olaf Klinke <olf at aatal-apotheke.de> wrote:
>>Dear Olaf,
>>
>>On Sat 09 Apr 2022 10:45:56 PM GMT, Olaf Klinke wrote:
>>> my monograph "Haskell for Mathematicians" has found a home online:
>>> https://hub.darcs.net/olf/haskell_for_mathematicians
>>
>>I just had a first look, your monograph looks awesome! Thank you for
>>sharing!
>>
>>In haskell_for_mathematicians.tex, you mention as a further idea that
>>Hask is like a Heyting algebra. Could you elaborate on that point? Are
>>you thinking of types as propositions here?
>>
>>Cheers,
>>Ingo
>
>Hi Ingo,
>
>Types as propositions is dealt with in haskell_for_logicians.lhs. 
>Hask has an arrow that is a right adjoint, just like a Heyting algebra. It 
>is less clear, however, whether the the arrow gives rise to a partial 
>order as it does in Heyting algebras. I am interested in the complete 
>Heyting algebras, a.k.a. frames a.k.a. locales. Many concepts in 
>point-free topology heavily rely on partial orders and lattice theory, so 
>without a good analogue I would not dare declare a similarity.
>For example, in a Heyting algebra x <= y iff x -> y equals the top 
>element.
>But then, what is the top element of Hask? Do we declare x <= y if x -> y 
>is inhabited? That seems to collapse all inhabited types.
>
>In a future chapter I would like to tell a story around this:
>In point-free topology (locale theory), there are several inter-definable 
>concepts of sub-object. One of them is a "nucleus", that is an 
>endo-function j with the following properties. 
>x <= y implies j(x) <= j(y)    (j is a functor)
>x <= j(x)                      (return :: x -> j x)
>j(j(x)) <= j(x)                (join :: j (j x) -> j x)
>j(x) /\ j(y) <= j(x /\ y)      (liftM2 (,) :: j x -> j y -> j (x,y))
>
>In other words: sub-objects of point-free spaces are (strong) monads.
>In that respect, every monad j is a sub-object of Hask, and indeed it is: 
>It defines the sub-category (Kleisli j). There are more analogues: The 
>identity function is a nucleus and corresponds to the greatest sub-object, 
>and in Hask (Kleisli Identity) is the largest Kleisli category. Nuclei can 
>not be combined easily, and neither can monads.
>
>Another interesting question is: What are the "points" of Hask? A point of 
>a locale is a mapping from opens (types of Hask) to Bool that preserves 
>finite products and arbitrary coproducts, where True is considered as the 
>empty product and False as the empty coproduct. How many of such mappings 
>can be defined in Haskell? How would we implement them? As a class? Type 
>family? GADT? 
>The funny thing about locales is that one can have few or no points but 
>still a rich supply of sub-objects.
>
>Olaf
>_______________________________________________
>Haskell-Cafe mailing list
>To (un)subscribe, modify options or view archives go to:
>http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220410/43948c59/attachment.html>