[Haskell-cafe] How to implement type level type equality?

Marc Weber marco-oweber at gmx.de
Mon Aug 25 20:11:02 EDT 2008

I'm trying to write a validating XML library. 
I'm struggling with implementnig the choice alternative.

Once piece of the code is

Where st is the state representing the subelemnts which may still be
attached to the current element. (Basically some tree containing
Seq, Or, one or more, 0 or more, 0 or 1)
Each xml tag is represented by it's own type. el is the element which
should be added.

(1): match of types, I'd like to return a C(onsumed)
(2): no match, I'd like to return a F(ailure)

        class Consume st el r | st el -> r -- result is on of C,R,F 

        -- element 
        instance Consume ANY el C
        instance Consume (Elem el) el C                         -- (1)  
        instance Consume (Elem el') el (F ExpectedButGot el' el) --(2)

Of course this results in:
||     Functional dependencies conflict between instance declarations:

Is there a nice way to implement this type level equality function?
Of course I could give an instance for each possible comparison
instance EQ TAG_A TAG_A HTrue
instance EQ TAG_A TAG_DIV HFalse
instance EQ TAG_A TAG_HTML HFalse
which would work find but would also be a mess if a xml dtd has many
(100 elements means 100 * 100 comparisons = 10.000 *shrug*)
I fear this slowing down compilation time a way too much.

So my current idea is to assign numbers to all tags and do some type
level number comparison. This will work resulting in something like
data Zero
data Succ a

class Eq a b c | a b -> c

Eq (Succ a) Zero HFalse
Eq Zero Zero HFalse
Eq Zero (Succ a) HFalse
Eq (Eq a b c) => (Succ b) (Succ a) c

I want to know wether you know about a more elegant solution.

Marc Weber

More information about the Haskell-Cafe mailing list