Wow Juan! You skipped past puzzle #1 and answered #2!

My answer to #1 was based on Oleg's lecture notes (page 27):


newtype R h a = R {unR :: h -> a}

--- ...

run e = unR e ()



I later saw the slick solution. You skipped to it right away!

Also, I love these explanations you are giving.

I had a random thought regarding your first puzzle:

> *What property of the Galois connection is proved by the implementation of bind `(>>=)` ?*

Consider `flip (>>=) :: Monad m => (a -> m b) -> m a -> m b`. Prelude calls this `(=<<)`.

This is intimately related to the definition of the closure of `a` in topology. From [Wikipedia](https://en.wikipedia.org/wiki/Closure_(topology)#Definitions):

> cl(*S*) is the smallest closed set containing *S*

Symbolically:

$$
(a \subseteq cl(b)) \Longrightarrow cl(a) \subseteq cl(b)
$$

Every topology gives rise to a preorder, called its [*specialization order*](https://en.wikipedia.org/wiki/Specialization_(pre)order). I mentioned this in the Chapter 1 thread. And you can recover an isomorphic [Alexandrov topology](https://en.wikipedia.org/wiki/Alexandrov_topology) from every preorder. You can also map all of the monotonically increasing functions \\(f\\) to continuous functions and vice versa. So these topics are related.

----------------------------------------------------

I think the finally tagless DSL I gave needs some work to properly fit it into Conal Elliot's framework. Also, it's probably best to build up with fragments. I am hoping to start this next week.