Re: [Haskell-cafe] ANN: haskell for mathematicians
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
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
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.
participants (2)
-
Keith -
Olaf Klinke