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