Embeddings, Part Two: Monad --> Thrist

Here comes the second part of my promised embeddings, this time I'll embed any monadic chain (corresponding to the do-syntax in Haskell) into a thrist and provide a semantics. Later I'll try to discuss some convenience features and try my luck with mfix (and the mdo-notation).

As in my post dealing with arrows, we have to define an adapter GADT:

data Monad' :: (* -> *) -> * -> * -> * where
Feed :: Monad m => m b -> Monad' m a b
Digest :: Monad m => (a -> m b) -> Monad' m a b

The semantics is a bit trickier as in the arrow case, but let's find out the type signature first...
Feed sounds like an introduction of a new monadic value, we would like to interpret it as the (>>) connective. Digest on the other hand transforms, and thus corresponds to (>>=). Both expect an already formed monadic value, so we can state:

recoverM :: Monad m => m a -> Thrist (Monad' m) a b -> m b

The effect of an empty thrist is trivial:

recoverM mon Nil = mon

And the other two connectives turn out to be the only sensible way to do it:

recoverM mon (Cons (Feed m) rest) = recoverM (mon >> m) rest
recoverM mon (Cons (Digest f) rest) = recoverM (mon >>= f) rest

Now, we can build up chains:

*Embeddings> :t Cons (Feed getChar) $ Cons (Digest (return . ord)) Nil
Cons (Feed getChar) $ Cons (Digest $ (return . ord)) Nil :: forall a. Thrist (Monad' IO) a Int

and execute them too:

*Embeddings> recoverM getChar (Cons (Feed getChar) $ Cons (Digest (return . ord)) Nil)
Loading package haskell98 ... linking ... done.
GG71

The first 'G' is consumed by the getChar invocation that is given to recoverM, but its result is ignored. The second is having an effect too, and its result is used to obtain the ASCII value. The overall monadic action is then run by ghci, printing the 71.

We have converted >> getChar >>= (return . ord) into a thrist and got it back by means of recoverM! And this works for any monad.

Two shortcuts come to my mind, they can be modelled by adding two simpler variants to the GADT:

Feed' :: Monad m => b -> Monad' m a b
Digest' :: Monad m => (a -> b) -> Monad' m a b

The semantics should be clear, I leave the extension of recoverM to the reader.

Now what about the value fixpoint mfix? Can we dress it in thristy clothes? Frankly, I have no idea, but I would be happy to hear from you. It is late, I need sleep now. Bye.

Embeddings, Part One: Arrow --> Thrist

Dan Weston asked me how the embeddings of arrows and monads into thrists would look like.
Took me some effort, but I think I have found something that appears to be satisfactory.

This time I shall prove my claim that in Haskell any Control.Arrow instance can be rewritten as a Thrist data structure. I shall also provide a semantics for the resulting data that shall recover the original arrow. Let me recapitulate the Thrist definition before diving in:

data Thrist :: (* -> * -> *) -> * -> * -> * where
Nil :: Thrist p a a
Cons :: p a b -> Thrist p b c -> Thrist p a c

Let's begin with the embedding part. Since the members of thrists are constructors of a two-parameter GADT, we have to construct the Arrow' GADT first. Here is the adapter:

data Arrow' :: (* -> * -> *) -> * -> * -> * where
Arr :: Arrow a => a b c -> Arrow' a b c
First :: Arrow a => Arrow' a b c -> Arrow' a (b, d) (c, d)

Arr takes any arrow and wraps it. This constructor is responsible for the actual embedding and it is easy to see that it is completely general.
First is responsible for defining a transformation on a pair's first component. Clearly this corresponds to the Arrow type class's first member. I refrain from doing the same to the other functions in the Arrow type class. You may scratch your head now, asking whether I have forgotten to handle the >>> member... The answer is no, I'll come back to this later.

Let's see how this works out in the practice...

t1 :: Thrist (->) Char Char
t1 = Cons ord (Cons chr Nil)

This is just the plain chaining of functions as a thrist. Here is the Arrow' embedding:

t2 :: Arrow' (->) Char Int
t2 = Arr ord

We make a thrist of length 1:

t3 :: Thrist (Arrow' (->)) Char Int
t3 = Cons t2 Nil

This is bit more involved, adding a constant second pair component:

t4 :: Arrow' (->) a (a, Int)
t4 = Arr (\a -> (a, 42))

Now it is time to form a longer thrist:

t5 :: Thrist (Arrow' (->)) Int (Int, Int)
t5 = Cons (Arr chr) (Cons t4 (Cons (First t2) Nil))

So, this corresponds to what? Intuitively, it could mean
chr >>> (\a -> (a, 42)) >>> first ord.
The Cons data constructor assumes the rôle of >>>.

To obtain a meaning at all, we have to define a semantics for it! Here it comes, and allows us to recover the embedded arrow:

recover :: Arrow a => Thrist (Arrow' a) b c -> a b c
recover Nil = arr id
recover (Cons (Arr f) r) = f >>> recover r
recover (Cons (First a) r) = first (recover $ Cons a Nil) >>> recover r

Some people call this an (operational) interpreter.

Finally, a little test:

*Embeddings> (recover t5) 55
Loading package haskell98 ... linking ... done.
(55,42)

Cute, isn't it?

PS: To embed monads, you can try embedding them via Kleisli to obtain an arrow and then via Arrow' to construct a thrist. Alternatively wait for a future post here :-)

PPS: For running the above you will need these preliminaries:

module Embeddings where
import Prelude
import Control.Arrow
import Char

What Ωmega has joined, no one can take apart

Some days ago I became enthusiastic about creating data structures with some pretty strong invariants. What I did not expect were the difficulties actually providing the evidence that the preconditions hold, and that taking apart the the data into pieces without losing the constraints can become a challenge. In fact, when embarking on programming with SingleLabel, a bunch of proof obligations arise.

So the title is actually misleading (sounds cool nevertheless!) and should read "... no one can take apart losslessly". Of course a non-empty SingleLabel can be taken apart by pattern matching! This article is about propositional facts, and their propagation.

The More data constructor is only accessible if the constraint Equal rest {drop l rest} is given. Last time no evidence was needed, because rest was explicitly known, so the drop type function could be evaluated and the equality checked. But when we just want to join a new head with an unknown tail?
This should still be possible in case that a witness is provided, that testifies that the tail does not contain the label occurring in the new head. Simple enough,

join :: Label a -> v -> SingleLabel tail -> Equal {drop a tail} tail -> SingleLabel {a=v; tail}r
join a v t Eq = {a=v; t}s

should do it. Unfortunately I am running against the wall again. The Eq witness is not accepted by Ωmega, on the grounds that no refinement can be established. The debugging session tomorrow promises to become an adventure!

When this problem is fixed, I'll come back and tell you the story of the lossless decomposition (so that calling join with the results gives us the original back).

Only one of each, please!

Must be all those sleepless nights (no, I do not want to blame my 6 month old daughter) that light the fire of creativity sometimes...

Two nights ago I had this marvelous idea: how to say that a list is indeed a set. Dear reader, if you do not like maths, please go home now. I am in the happy state of a half bottle of Shiraz and only want people around who share my interests!

Okay let's come to the point. As you probably know, Ωmega provides a Row kind, it is a classifier for associations at the type level.

The shorthand notation {`a=Int, `b=Char}r can express a record where a component labelled with `a contains values of type Int while under the key `b we can store Chars. This is probably boring stuff if you already understand extensible records.

Now let's descend to the value plane. A value can have a type SingleLabel {`a=Int, `b=Char}r when we define following datatype:

data SingleLabel :: Row Tag * ~> * where

None :: SingleLabel RNil

More :: Label l -> t -> SingleLabel rest -> SingleLabel {l=t;rest}r

deriving Record(s)

As usual we have two data constructors, one for the empty record and one for augmenting an existing one. The "deriving" clause just tells Ωmega to enable the following syntactic sugar for None and More: More `lab 42 None === {`lab=42}s, nothing exciting.

But no one can hinder us to define a record value with repeated identical keys: {`a=25, `a="42"}s is a perfectly legal value of type {`a=Int, `a=[Char]}s but it really is incompatible with our aim of defining a one-to-one correspondence between labels and values.

Now enters my cunning idea: using a constraint, we can restrict the tail of the list to not contain a key we are about to add. Constraints are much like Haskell's type classes, but they are less ad-hoc and mirror propositional facts (properties). The new definition could look like this:

data SingleLabel :: Row Tag * ~> * where

None :: SingleLabel RNil

More :: Equal rest {drop l rest} => Label l -> t -> SingleLabel rest ->
SingleLabel {l=t;rest}r

deriving Record(s)

We have defined following semantics: Under the restriction that dropping the tag l from the tail does not change it at all (a fixpoint!), we can construct an augmented list. We have almost reached our self imposed objective: it only remains to provide a suitable definition for drop!

Now, Ωmega helps us in this respect too (but not entirely so for Tags), as we can define functions on types (or kinds for that matter). We can do it this way:

drop :: Tag ~> Row Tag * ~> Row Tag *

{drop o RNil} = RNil

{drop `a (RCons `a v r)} = {drop `a r}

{drop `b (RCons `b v r)} = {drop `b r}

{drop `b (RCons `a v r)} = RCons `a v {drop `b r}

{drop `a (RCons `b v r)} = RCons `b v {drop `a r}

This should be enough for demonstration purposes. (We get a quadratic blowup with increasing number of desired labels, since we have to write our definition in an inductively sequential fashion).

With all of this in place we can give a whirl to our SingleLabel datatype:

prompt> {`a=42}s

--> {`a=42}s :: SingleLabel {`a=Int}r

prompt> {`a=42,`b='K'}s

--> {`a=42,`b='K'}s :: SingleLabel {`a=Int,`b=Char}r

prompt> {`a=42,`a='K'}s

--- Type error: cannot find a solution for equation {`a=Char}r == {}r

We can now go to bed with the feeling of having accomplished a thing...

PS: Ωmega in its last released form cannot compile the code presented here. You will need some patches to get various bugs ironed out. With some luck this all will work out of the box in the next release!

Trendy Topics

There seem to be two important trends in the Haskell universe and I must admit, that I do not want to stay away from them either...

• The first one is the exploration of category-theoretic concepts and their showing-off in the blogosphere. Generalizations of monads or the category type class are just two recent picks from the bottomless supply of ideas.
• The second trend is more subtle and one has to dive into the recent ICFP papers to perceive it. I have already mentioned the Unimo framework, which guarantees the monad laws and allows to represent the monadic computation as a pure data structure which is then run by recursive analysis. Wouter Swierstra et al. introduced another concept to capture monads (also strongly resembling the free monad) and they have improved testing ability on their minds when doing this. The third paper that comes to my mind is about speeding up arrow computations by analysis and optimization of a data structure closely resembling arrows.

So I am not in bad company announcing that I am preparing a paper about thrists which are the moral equivalents of free categories. The rest of this article gives an appetizer about thrists.

data Thrist :: (* -> * -> *) -> * -> * -> * where
Nil :: Thrist p a a
Cons :: p a b -> Thrist p b c -> Thrist p a c

The definition makes it clear that Thrist is a GADT (I use the Haskell way of defining a GADT here, the paper will use the slightly different Ωmega syntax) and it is a curious mixture of listness and threadedness (this is the reason for its name). The types of the thrist elements must match up in a certain way, resembling function composition.
Indeed, instead of composing functions, we can put them into a thrist:

Cons ord $ Cons chr Nil

gives us an arrow thrist (Thrist (->) Char Char) only showing the start and end types, with the internal types abstracted away existentially.
Of course we have to supply an interpreter for this data structure to get the functionality (the semantics) of function composition, but this easy exercise is left to you.

But... What do thrists buy us?
Two very important things:

• Unlike function composition, we can take the thrist apart, analyse and transform it, and
  
• a vast field opens up with the first (p) parameter to the Thrist. It can be the pair constructor (,) or the LE (less-or-equal) proposition, there are many sensible instantiations -- especially with two-parameter user-defined GADTs.

Finally, the category-theoretic twist: think of the parameter p as the morphisms of a category C (with C's objects being the morphisms' domains and ranges) then Thrist p is essentially the free category of C, often written as C*.

I hope you enjoyed reading this in the same way as me writing it!

Traumzimmer

Some people know, but many more don't, that my wife Patricia is an artist specializing in designing babies' or children's rooms. Back in Brazil she even made a living out of this.
After some creative pause and the arrival of our baby (she has also decorated her space) it is time to get back to work. I am very proud of what she is accomplishing, so I'd love to show you some pieces at Traumzimmer. The website is pretty new, but taking shape slowly, and documents the progress of the firm she opened with another brazilian girl.
Enjoy!

Comonads

Slowly recovering from vacation-induced ignorance, today I printed out some interesting papers about type-preserving compilation, plans for type-level functions in GHC and dataflow implementations using comonads. Another one about Hoare Type Systems remained on my screen, too heavy for me, a.t.m.
So I am wrapping my head around category theory again. Somehow all these topics seems to interact, and I continuously am trying to fit them into my Thrist framework. Today I tried to implement a Comonad to Thrist adapter (in my mind at least, no code written yet).