[Haskell-cafe] ANN: haskell for mathematicians

[Olaf Klinke]

>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