Sun Apr 10 19:26:15 UTC 2022

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