Archive for February, 2008

Unimo

Wednesday, February 27th, 2008 by Nils Anders Danielsson

The discussions on Feb 15 concerned correct-by-construction methods for defining monads.

“Programming Monads Operationally with Unimo” (Chuan-kai Lin, ICFP’06) presents a data type Unimo which can be used to construct monads. These monads are supposed to satisfy the monad laws by construction. Furthermore they make use of the associative law to avoid the quadratic behaviour that sometimes affects left-nested uses of bind (analogously to the quadratic complexity of (...(xs_1 ++ xs_2) ++ ...) ++ xs_n).

Unfortunately there are some flaws in the paper; the right unit monad law is not actually satisfied in general, and the termination of the main run function is not established properly. Instead I presented a simplified variant which is less efficient, but perhaps more elegant.
(more…)

Standard Haskell

Sunday, February 24th, 2008 by Conor

Spotted this on my way from London to Glasgow last Thursday.

Quite right!

FP -vs- OO bialgebraically (“Expression Lemma”)

Friday, February 22nd, 2008 by Ondrej

Today I showed how distributive laws of a monad over a comonad and adequacy results for bialgebraic operational semantics [Plotkin & Turi] can be used to formalize the correspondence between (certain) FP algebraic datatypes with functions (essentially implementations of abstract data types) and recursive OO structures (collections of classes with the same interface).

In short, given a functor \Sigma standing for the signature of a datatype and a (finite) collection of functions f_i\,:\,\mu\Sigma\rightarrow B_i\mu\Sigma (where \mu\Sigma is the least fixed point of \Sigma and each B_i is a functor), we can form the tupple \langle f_i \rangle_i\,:\,\mu\Sigma\rightarrow(\Pi_i B_i)\mu\Sigma. Let B be defined as the product B\triangleq\Pi_i B_i. This arrow \langle f_i \rangle_i is quite often a catamorphism whose algebra factors through a natural transformation \lambda:\Sigma B \Rightarrow B \Sigma, thus \langle f_i \rangle_i \;=\;\textsf{fold}(B \textsf{in}\circ\lambda), where \textsf{in} is the initial \Sigma-algebra. Informally, \lambda here combines recursive results from subterms and B\textsf{in} packs recursive results into a new instance of \mu\Sigma (for instance in a catamorphically defined map).

On the other hand, let us take the colagebraic view of objects [e.g. Jacobs] where interfaces are (certain) polynomial endofunctors, classes are coalgebras and object types are carriers of terminal coalgebras. Then a collection of classes with the same interface, B, whose carriers are respectively given by the cases of the algebraic datatype functor \Sigma are defined by a single coalgebra \phi\,:\,\Sigma\nu B \rightarrow B\Sigma \nu B (where \nu B is the greatest fixed point of B, i.e. the carrier of the terminal B-coalgebra). Let us take \phi\,\triangleq\,\lambda\circ\Sigma\mathsf{out}. This corresponds to the classes recursively delegating to their subcomponents and then combining the resulting collection of behaviours into a behaviour on a collection.

Now \mathsf{unfold}(\mathsf{fold}(B\mathsf{in}\circ\lambda))\;=\;\mathsf{fold}(\mathsf{unfold}(\lambda\circ\Sigma\mathsf{out}))\;:\;\mu\Sigma\rightarrow\nu B. This means that the functional program defined by a fold over an algebraic datatype, when wrapped up as an abstract datatype with interface B, is bisimilar to the object constructed by folding a class constructor over a tree of object states. Note that in the latter case, each layer is first turned into a collection of objects (by \mathsf{unfold}(\lambda\circ\Sigma\mathsf{out})) which are then used to construct an object at the next level (as common in OO). In the first functional case, the functions are defined directly on an open datatype and the whole result is then interpreted as an abstract data type (object).

The situation generalizes straightforwardly for more general distributive laws of a monad over a comonad, in particular when the monad is free and comonad cofree. Thus \lambda:T_\Sigma D_B \Rightarrow D_B T_\Sigma. This allows us to express a larger class of OO and FP programs while still preserving their bisimilarity.

A paper about this has been recently submitted for conference publication. The preliminary version and some relevant Haskell implementation can be found here.

Associated Types and Open Type Families

Saturday, February 16th, 2008 by Peter

Neil Ghani asked what Associated Types were, so I tried to give an introduction to them. Starting the story with Multi-Parameter Type classes and the short-comings of Functional Dependencies and ending with extending the idea of ATs to Type Families. For the curious, this stuff all relies on System F with Type Equality Coercions.

Monad Transformers

Monday, February 4th, 2008 by Mauro Jaskelioff

Monad transformers were introduced as a programming technique many years ago, but we are still not sure what mathematical structure they are. For example, we still don’t know if every monad has an associated monad transformer, or even if every monad should have just one associated monad transformer.

John Power argues that monad transformers should come before monads since every M-monad transformer gives raise to a monad M by applying it to the identity monad. One structure that comes before monads is adjunctions: every adjunction $\langle F,G,\eta,\varepsilon\rangle\colon\mathbb{C}\rightharpoonup\mathbb{D}$ gives rise to a monad $\langle FG, \eta, G\varepsilon F\rangle$. Also, every monad can be split into an adjunction. There are usually many adjunctions a monad can be split into, but there are two canonical ones: the Kleisli and the Eilenberg-Moore (which are the initial and the final splittings in some sense).

Now, given an adjunction $\langle F,G,\eta,\varepsilon\rangle\colon\mathbb{C}\rightharpoonup\mathbb{D}$ and a monad $\langle M, \eta^{M}, \mu^{M}\rangle$ on $\mathbb{D}$, we can choose any adjunction giving rise to it and use adjoint composition to obtain a monad $\langle GMF,G\eta^{M}F\cdot\eta,G\mu^{M}F\cdot GM\varepsilon MF\rangle$ on $\mathbb{C}$.

So, a monad transformer for a monad $T$ might be explained by a choice of an adjunction $\langle F,G,\eta,\varepsilon\rangle\colon\mathbb{C}\rightharpoonup\mathbb{D}$ splitting $T$ and a lifting of monads in $\mathbb{C}$ to monads in $\mathbb{D}$.

If the choice of the adjunction is the Eilenberg-Moore one, then the lifting of $M$ is given by a distributive law of monads
$\lambda\colon TM\rightarrow MT$, and the obtained monad is $\langle MT,\eta^{M}\cdot\eta^{T},\mu^{T}\cdot \mu^{M}\cdot M\lambda_{T}\rangle$. For example, this explains the standard Haskell monad transformers for Maybe and Writer.

If the choice of the adjunction is the Kleisli one, then the lifting of $M$ is given by a distributive law of monads
$\lambda\colon MT\rightarrow TM$, and the obtained monad is $\langle TM,\eta^{T}\cdot\eta^{M},\mu^{M}\cdot \mu^{T}\cdot T\lambda_{M}\rangle$. For example, this explains the standard Haskell monad transformers for Reader and Cont.

The State monad transformer is not explained by any of the canonical adjunctions splitting the monad, but by the currying/uncurrying adjunction characterizing exponentials:

$\langle S\times -,S\Rightarrow -,\eta^{S},\varepsilon^{S}\rangle\colon\mathbb{C}\rightharpoonup\mathbb{C}$

Note that here the lifting is trivial, as the category on the left and the right of the adjunction is the same.