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

[jeff p]

Hello,

  The HList paper (http://homepages.cwi.nl/~ralf/HList/) presents a
reasonable general type level equality (though it requires GHC). The
paper also describes some other implementations including the
interpretation of types as type-level nats.

-Jeff

On Mon, Aug 25, 2008 at 8:11 PM, Marc Weber <marco-oweber at gmx.de> wrote:
> 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
> elements.
> (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
> this:
> data Zero
> data Succ a
>
> class Eq a b c | a b -> c
>
> instances:
> 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.
>
> Sincerly
> Marc Weber
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>