HTTP content-type comparison at the type level

Posted by alpheccar - Dec 23 2007 at 22:24 CEST

If you read my previous post, you'll be interested by this one. Indeed, I have discovered that the idea introduced in the previous post is working but not practical at all since it does not work with type synonym definitions. But, without synonyms, you can't really write the kind of types required to do http content-type comparison at the type level. By luck, some additional type hacking is solving the problem. Moreover, I think it can be useful to show in a very informal way a few applications of computations at type level. It is not so hard (but not totally trivial. I had to make several experiments to get it right).

What is the problem ?

The order relationship (:<:), defined in my previous post, is working if the type has the shape of a list:

type T = A :+: (B :+: (C :+: D))

which can also be written:

type T = A :+: B :+: C :+: D

since (:+:) is defined with

infixr 6 :+:

When I read about type synonym for the first time in the Haskell report I was confused by the sentence:

Type synonyms are a convenient, but strictly syntactic, mechanism to make type signatures more readable.

I was stupid to think that type synonyms were a bit like preprocessing directives. It is not the case and that's why the following type is not equivalent to the one above:

type TA = A :+: B
type TB = C :+: D
type T' = TA :+: TB

If I expand the type synonyms, I get:

type T' = (A :+: B) :+: (C :+: D)

So the shape of T' is the shape of a tree and not of a list like T above.

Solution

To be able use (:<:) with types built from type synonyms, I need to define a function on types transforming a tree to a list ! Then, I'll be able to compare easily any expression built from phantom types, the type constructor (:+:) and type synonyms. I am not interested in the shape of the type. The types that I am building are just encodings for set of types.

If the function was a normal Haskell function, I could define:

data MyTypes = A | B | C | D deriving(Show)
data Tree a = (:+:) (Tree a) (Tree a) | L a deriving(Show)

flatten :: Tree MyTypes -> Tree MyTypes
flatten (L x) = L x
flatten (a :+: b) = treeConcat (flatten a) (flatten b)

treeConcat :: Tree MyTypes -> Tree MyTypes -> Tree MyTypes
treeConcat (L x) b = (L x) :+: b
treeConcat (x :+: xs) ys = x :+: (treeConcat xs ys)

t = ((L A) :+: (L B)) :+: ((L C) :+: (L D))

Just type:

flatten t 

and you'll see that's the result has the shape of a list. treeConcat is just the list concat but where the lists are implemented with the Tree datatype.

Implementation at the type level

I am just going to translate this to the type level. It is nearly a direct translation. First, let's translate the algebraic datatype.

data A
data B
data C
data D

Tree is already defined as (:+:) at the type level in the previous post, and we do not need to define the L since at the type level I can make a distinction between a phantom type and a type like (a :+: b) which is not atomic.

Now, let's translate the treeConcat:

class TreeConcat l1 l2 l | l1 l2 -> l

The recursion is:

instance (TreeConcat xs ys zs ) => TreeConcat (x :+: xs ) ys (x :+: zs )

But, I also need to write instances for the leaves. I do not have a L like in the algebraic datatype. So, I need one instance per phantom type:

instance TreeConcat A b (A :+: (b))
instance TreeConcat B b (B :+: (b))
instance TreeConcat C b (C :+: (b))
instance TreeConcat D b (D :+: (b))

I am nearly done. Now, I just need to implement flatten:

class Flatten a b | a -> b

instance (Flatten a a', Flatten b b', TreeConcat a' b' c) => Flatten (a :+: b) c

It should be easy to decode it. The flatten a of the normal definition becomes Flatten a a', the flatten b becomes Flatten b b' and the treeConcat a' b' becomes TreeConcat a' b' c'. It should be clearer if I write the normal Haskell function as:

flatten (a :+: b) = let a' = flatten a
                        b' = flatten b
                        c = treeConcat a' b' 
                    in
                        c

And, I also need several instances for the phantom types. They are replacing the line flatten (L x) = L x

instance Flatten A A  
instance Flatten B B
instance Flatten C C
instance Flatten D D

Finally, I need to change the definition of (:<:) to use flatten. The old definition was:

class (:<:) a b

instance Elem a c => (:<:) a c
instance ((:<:) a c, (:<:) b c) => (:<:) (a :+: b) c

Now, it is:

class (:<:) a b

instance (Elem a c', Flatten c c') => (:<:) a c
instance ((:<:) a c', (:<:) b c',Flatten c c') => (:<:) (a :+: b) c

You see the difference ? Instead of using c, I use c' which is the flat version.

That's it ! We can check that it is working.

testa :: ((:<:)  (A :+: C) f) => (A :+: C) -> f
testa = undefined

testb :: T -> T
testb = undefined

In ghci, type :

:t testb . testa

and you get:

testb . testa :: (A :+: C) -> T

So, (A :+: C) is included in T in as a consequence, testa can be used. Now, if you change the code into:

data E
testa :: ((:<:)  (A :+: E) f) => (A :+: E) -> f
testa = undefined

and do the same test you get:

No instance for (Elem E D)

The type checker is preventing you to use testa because A :+: E is not included in T.

Both tests are failing with the old definition for (:<:). The use of Flatten is really required.

MERRY CHRISTMAS !

Tags type-level computation | haskell | web | http