How to implement type level type equality?
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
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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Mon, Aug 25, 2008 at 09:17:19PM -0400, jeff p wrote:
The HList paper (http://homepages.cwi.nl/~ralf/HList/) presents a
Thanks Jeff -- packages: HList {-# OPTIONS_GHC -fallow-undecidable-instances -XEmptyDataDecls -XMultiParamTypeClasses #-} module Main where import Data.HList import HAppS.Data import System.Environment class TypeToNat typE nr | typE -> nr instance ( TypeToNat a elNr , TypeToNat b elNr' , HEq elNr elNr' r) => HEq a b r data Id_A instance TypeToNat Id_A HZero data Root_T instance TypeToNat Id_A nr => TypeToNat Root_T (HSucc nr) main = do putStrLn (show (undefined :: (HEq Id_A Id_A a) => a )) || [1 of 1] Compiling Main ( test.hs, test.o ) || test.hs|19 error| || Context reduction stack overflow; size = 20 || Use -fcontext-stack=N to increase stack size to N || `$dHEq :: {HEq elNr elNr' a}' || arising from instantiating a type signature at test.hs:20:18-52 || `$dHEq :: {HEq elNr elNr' a}' However adding a dummy type T works fine: -- packages: HList {-# OPTIONS_GHC -XEmptyDataDecls -XMultiParamTypeClasses -fallow-undecidable-instances #-} module Main where import Data.HList import HAppS.Data import System.Environment data T a class TypeToNat typE nr | typE -> nr instance ( TypeToNat a elNr , TypeToNat b elNr' , HEq elNr elNr' r) => HEq (T a) (T b) r data Id_A instance TypeToNat Id_A HZero data Root_T instance TypeToNat Id_A nr => TypeToNat Root_T (HSucc nr) main = do putStrLn (show (undefined :: (HEq (T Id_A) (T Id_A) a) => a )) I don't see what's wrong with the first version.. Can you help me understand this implicationa ? Sincerly Marc Weber
-- packages: HList {-# OPTIONS_GHC -fallow-undecidable-instances -XEmptyDataDecls -XMultiParamTypeClasses #-} module Main where import Data.HList import HAppS.Data import System.Environment
class TypeToNat typE nr | typE -> nr instance ( TypeToNat a elNr , TypeToNat b elNr' , HEq elNr elNr' r) => HEq a b r
data Id_A instance TypeToNat Id_A HZero data Root_T instance TypeToNat Id_A nr => TypeToNat Root_T (HSucc nr)
main = do putStrLn (show (undefined :: (HEq Id_A Id_A a) => a ))
|| [1 of 1] Compiling Main ( test.hs, test.o ) || test.hs|19 error| || Context reduction stack overflow; size = 20 || Use -fcontext-stack=N to increase stack size to N || `$dHEq :: {HEq elNr elNr' a}' || arising from instantiating a type signature at test.hs:20:18-52 || `$dHEq :: {HEq elNr elNr' a}'
I should have added that Data.HList exposes the more specific instances
instance HEq HZero HZero HTrue
instance HNat n => HEq HZero (HSucc n) HFalse
instance HNat n => HEq (HSucc n) HZero HFalse
instance (HNat n, HNat n', HEq n n' b )
=> HEq (HSucc n) (HSucc n') b
That's why I think ghc tries to resolve the wrong instance first:
summary:
class TypeToNat a b | a -> b
class HEq a b c | a b -> c
instance ( TypeToNat a elNr -- (1)
, TypeToNat b elNr' -- (2)
, HEq elNr elNr' r) => HEq a b r -- (3)
putStrLn (show (undefined :: (HEq Id_A Id_A a) => a ))
When ghc tries to resolve HEq it starts with
TypeToNat ( TypeToNat Id_A <unkown type elNr>
, TypeToNat Id_A
Marc Weber wrote:
Now ghc can try to resolve (1),(2),(3) in arbitrary order.. What happens if ghc starts with (3)? It tries to find an instance for not known types.. Damn. There is even a matching instance.. , the same one. This time it starts even with HEq <unkown> <unkown> <unkown> which is even more bad! after the second recursion it already knows that won't find a solution, because it will try to resolve HEq <unkown> <unkown> <unkown> again and again..
What happens if ghc starts with (1 or 2)? It happily finds an instance *and* it can even resolve elNr and elNr' Those can then be used to find an instance for (3) easily
So I think the behaviour of ghc should be changed to prefer resolving class constraints which reduce the amount of unkown types first
I even consider this beeing a bug ?
So maybe this thread should be moved to glasgow-haskell-users ?
There are a number of issues like this due to the fact that typeclass instances aren't determined by full SLD resolution. More particularly the determinism information in fundeps seems to be ignored in this whole process. Not that I'm a GHC hacker (yet), but research in this area is at the top of my to-do stack; alas that's still a ways away. To put a refinement on your proposal, I'd suggest that fundeps be used to construct a dataflow graph in order to know which instances to pursue first (namely, the leaves). To resolve the ordering any toposort of the dataflow graph should be fine. This still has the problem of if there's no toposort, though: class Foo a b | a -> b class Bar a b | b -> a class Wtf a b instance (Foo a b, Bar a b) => Wtf a b There are a few standard approaches to break the cycle, though if instances of Foo or Bar are given inductively we might run into the same problems as your code. Here's another proposal, and perhaps an easier one to hack together for the time being. When pursuing the context of an instance for some class A, resolve all instances for non-A classes before pursuing instances for A. It's not a general solution, but it's closer to correct at least. -- Live well, ~wren
participants (3)
-
jeff p -
Marc Weber -
wren ng thornton