Free functors, free applicatives, free monads I'm now inclined to think that category theory, type theory, and intuitionistic logic can be merged into a "functional programming theory" that is more directly relevant to practical programming. Programmers do not have to think that they are doing calculations in some abstract mathematical domain. In fact, too much abstraction without a perceptible gain in productivity is a big turn-off for lots of people, myself included.
Part of finding a useful subset of theory is a good choice of notation -- more concise than a programming language and yet fully expressive, so that one can perform long calculations in it. At this point, I'm tending towards Haskell-like notation, e.g., F s t = R s -> t, instead of the more familiar algebraic notation F(s,t) = R(s) -> t that I've been using in these notes so far.
Previously I thought that the "free monad" is a fixpoint functor of the form Fix
x(t + A x), where A is a given functor. It turns out that people use at least three different definitions of a "free monad".
1.
http://www.haskellforall.com/2012/06/you-could-have-invented-free-monads.htmlIn Haskell:
Free F t = Pure t | F (Free F t)
The same definition is used by Kiselyov,
http://okmij.org/ftp/Computation/free-monad.html and in many other places.
In the short notation, this is
Free
1 F t = Fix
s(t + F s).
I thought this was the standard definition of the free monad; this is the definition I considered in my previous posts. However, recently some friends pointed me to the following two talks (both also available in video):
2.
http://www.slideshare.net/KelleyRobinson1/why-the-free-monad-isnt-free-61836547This definition is in Scala, and can be rewritten in Haskell like this,
Free F t = Pure t | Suspend (F t) | FlatMap (Free F a, a -> Free F t)
In the short notation,
Free
2 F t = Fix
G(t + F t + ∃a. G a * (a -> G t) )
Note that the fixpoint is taken with respect to the functor G, and the "exists" quantifier plays an important role, which can appear mysterious at first.
3.
http://functionaltalks.org/2014/11/23/runar-oli-bjarnason-free-monad/This is again in Scala, and is rewritten in Haskell as
Free F t = Pure t | Bind (F a, a -> Free F t)
In the short notation,
Free
3 F t = Fix
s( t + ∃a. F a * (a -> s) ).
Here, the fixpoint is taken with respect to a type s, not with respect to a functor. However, the existential quantifier is still present. Also, F does not have to be a functor for this definition to work!
So, I have these questions:
- What is actually the definition of the "free monad", such that it does not specify a particular implementation but specifies some properties that are fulfilled by all three implementations shown above? Does a "free monad" require a functor?
- Are these three implementations of the "free monad" equivalent, and if not, what are the differences?
- Are there still other implementations? How can we "derive" the implementations systematically from some principles, instead of guessing?
Trying to get to the bottom of this, I found that these alternative definitions use some tricks that are relevant to functional programming, but perhaps not so easily described in pure category theory. However, I do not yet have full clarity on all my questions.
What I also found is that there are similar definitions for a "free functor" and a "free applicative functor". But then, the same questions will apply to each of those.
(to be continued)