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 :: (* -> * -> *) -> * -> * -> * whereLet'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:

Nil :: Thrist p a a

Cons :: p a b -> Thrist p b c -> Thrist p a c

data Arrow' :: (* -> * -> *) -> * -> * -> * whereArr 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.

Arr :: Arrow a => a b c -> Arrow' a b c

First :: Arrow a => Arrow' a b c -> Arrow' a (b, d) (c, d)

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 CharThis is just the plain chaining of functions as a thrist. Here is the Arrow' embedding:

t1 = Cons ord (Cons chr Nil)

t2 :: Arrow' (->) Char IntWe make a thrist of length 1:

t2 = Arr ord

t3 :: Thrist (Arrow' (->)) Char IntThis is bit more involved, adding a constant second pair component:

t3 = Cons t2 Nil

t4 :: Arrow' (->) a (a, Int)Now it is time to form a longer thrist:

t4 = Arr (\a -> (a, 42))

t5 :: Thrist (Arrow' (->)) Int (Int, Int)So, this corresponds to what? Intuitively, it could mean

t5 = Cons (Arr chr) (Cons t4 (Cons (First t2) Nil))

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 cSome people call this an (operational) interpreter.

recover Nil = arr id

recover (Cons (Arr f) r) = f >>> recover r

recover (Cons (First a) r) = first (recover $ Cons a Nil) >>> recover r

Finally, a little test:

*Embeddings> (recover t5) 55Cute, isn't it?

Loading package haskell98 ... linking ... done.

(55,42)

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

## No comments:

Post a Comment