As I mentioned some time ago, Mauro Jaskelioff and I have been working on a paper discussing Twan van Laarhoven’s representation of second order functionals used in van Laarhoven lenses and traversals.
Mauro’s theorem is a generalization of Milewski’s proof that, by using two applications of the Yoneda lemma, one can exhibit an isomorphism between PStore i j a and forall f. Functor f => (i -> f j) -> f a where PStore is the parameterized store comonad defined below.
data PStore i j a = PStore { pos :: i; peek :: j -> a }
Mauro’s theorem, discovered independently at the same time as Milewski’s, adds an adjunction to the mix leading to an isomorphism that works for lenses, traversals, affine traversals, and more. It is the ‘and more’ that I want to discuss.
One application of Mauro’s theorem is the van Laarhoven free monad
representation for algebraic effects, or van Laarhoven free monad for short.
The basic theorem states that FreeMonad (PStore i j) a and forall m. Monad m => (i -> m j) -> m a are isomorphic.
The advanced version states that FreeMonad (Σ n. PStore in jn) a and forall m. Monad m => (Π n. in -> m jn) -> m a are isomorphic.
data FreeMonad f a = Return a | FreeMonad (f (FreeMonad f a))
A free monad of a sum of store functors is the exactly the sort of free monad that Swierstra uses to model I/O interactions in Data Types à la Carte. For example, Swierstra models teletype I/O by a free monad generated from the following functor.
data Teletype a = GetChar (Char -> a) | PutChar Char a
The Teletype functor is isomorphic to PStore () Char + PStore Char (), thus is the sum of store functors.
This means FreeMonad Teletype a is isomorphic to the van Laarhoven free monad type forall m. Monad m => TeletypeOps m -> m a where TeletypeOps is the following record type.
data TeletypeOps m = TeletypeOps { getChar :: m Char; putChar :: Char -> m () }
A value of type forall m. Monad m => TeletypeOps m -> m a can be interpreted in the standard way by passing in the record TeletypeOps Prelude.getChar Prelude.putChar :: TeletypeOps IO, but we are free to give other interpretations.
For example, if we have a handle h :: Handle in our context then we can interpret our value by passing in the record
TeletypeOps (Prelude.hGetChar h) (Prelude.hPutChar h) :: TeletypeOps IO.
We could give a ‘pure’ interpretation to our value in order to use it in testing à la IOSpec library.
We could give a console interpretation where we also log all inputs.
We could give an interpretation where we replay logged inputs.
The list of possibilities is endless.
The van Laarhoven free monad is a monad. Below is how one can implement it in Haskell. Try not to let the impredicativity hurt your head too much.
-- (ops m) is required to be isomorphic to (Π n. i_n -> m j_n)
newtype VLMonad ops a = VLMonad { runVLMonad :: forall m. Monad m => ops m -> m a }
instance Monad (VLMonad ops) where
return a = VLMonad (\_ -> return a)
m >>= f = VLMonad (\ops -> runVLMonad m ops >>= f' ops)
where
f' ops a = runVLMonad (f a) ops
Swierstra notes that by summing together functors representing primitive I/O actions and taking the free monad of that sum, we can produce values use multiple I/O feature sets. Values defined on a subset of features can be lifted into the free monad generated by the sum. The equivalent process can be performed with the van Laarhoven free monad by taking the product of records of the primitive operations. Values defined on a subset of features can be lifted by composing the van Laarhoven free monad with suitable projection functions that pick out the requisite primitive operations. No doubt someone will develop a library implementing a type class(y) hierarchy to make this process transparent, which may or may not be a good idea.
The van Laarhoven free monad provides yet another way of representing a monadic foreign function interface to Kmett’s list of representations. Now, I am not much for practical applications of theory, so I will leave it to others to determine how practical the van Laarhoven free monad representation is. I am optimistic it will be competitive with Kmett’s representation, and might even be cheaper.