[Haskell-cafe] ANN: haskell for mathematicians
Keith
keith.wygant at gmail.com
Sun Apr 10 19:57:20 UTC 2022
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>
More information about the Haskell-Cafe
mailing list