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).
1. What is the problem ?
The order relationship (:<:), defined in my previous post, is working if the type has the shape of a list:
which can also be written:
since (:+:) is defined with
When I read about type synonym for the first time in the Haskell report I was confused by the sentence:
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 TB = C :+: D
type T' = TA :+: TB
If I expand the type synonyms, I get:
So the shape of T' is the shape of a tree and not of a list like T above.
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 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))
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.
3. 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.
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:
The recursion is:
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 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:
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:
b' = flatten b
c = treeConcat a' b'
And, I also need several instances for the phantom types. They are replacing the line flatten (L x) = L x
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:
instance Elem a c => (:<:) a c
instance ((:<:) a c, (:<:) b c) => (:<:) (a :+: b) c
Now, it is:
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 = undefined
testb :: T -> T
testb = undefined
In ghci, type :
and you get:
So, (A :+: C) is included in T in as a consequence, testa can be used. Now, if you change the code into:
testa :: ((:<:) (A :+: E) f) => (A :+: E) -> f
testa = undefined
and do the same test you get:
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 !
(This post was imported from my old blog. The date is the date of the import. The comments where not imported.)