> But you have just pushed the problem off to the definition of EQ. And > your definition of EQ requires a finite enumeration of all types, I > think. But * is open, so that's hard to do. What you want is > type instance EQ where > EQ a a = TRUE > EQ _ _ = FALSE > and now we are back where we started.
Not at all. In the first approximation, EQ is the _numerical_ equality, equality of two type-level naturals. Since Goedel numbering is no fun in practice, I agree on the second approximation, described in TTypeable.hs. I quote the beginning of that file for reference: > module TTypeable where > {- > It helps in understanding the code if we imagine Haskell had > algebraic data kinds. We could then say > > kind TyCon_name -- name associated with each (registered) type constructor > > kind NAT -- Type-level natural numbers > kind BOOL -- Type-level booleans > > kind LIST a = NIL | a :/ LIST a > > -- Type-level type representation > kind TYPEREP = (TyCon_name, LIST TYPEREP) > -} > > -- Type-lever typeOf > -- The more precise kind is * -> TYPEREP > type family TYPEOF ty :: * > > -- Auxiliary families > > -- The more precise kind is TyCon_name -> NAT > type family TC_code tycon :: * > > -- Sample type reps (the rest should be derived, using TH, for example) > -- Alternatively, it would be great if GHC could provide such instances > -- automatically or by demand, e.g., > -- deriving instance TYPEOF Foo > data TRN_unit > type instance TC_code TRN_unit = Z > type instance TYPEOF () = (TRN_unit, NIL) > data TRN_bool > type instance TC_code TRN_bool = S Z > type instance TYPEOF Bool = (TRN_bool, NIL) I could write a TH function tderive to be used as follows. When the user defines a new data type data Foo = ... then $(tderive ''Foo) expands in > data TRN_package_name_module_name_Foo > type instance TC_code TRN_package_name_module_name_Foo = > <very long type-level numeral that spells package_name_module_name_Foo in > unary> > type instance TYPEOF Foo = (TRN_package_name_module_name_Foo, NIL) I think I can write such tderive right now. So, the EQ (or, TREPEQ as I call it) is defined in closed form: > -- Comparison predicate on TYPEREP and its parts > > -- TYPEREP -> TYPEREP -> BOOL > type family TREPEQ x y :: * > > type instance TREPEQ (tc1, targ1) (tc2, targ2) = > AND (NatEq (TC_code tc1) (TC_code tc2)) > (TREPEQL targ1 targ2) > > -- LIST TYPEREP -> LIST TYPEREP -> BOOL > type family TREPEQL xs ys :: * > > type instance TREPEQL NIL NIL = HTrue > type instance TREPEQL NIL (h :/ t) = HFalse > type instance TREPEQL (h :/ t) NIL = HFalse > type instance TREPEQL (h1 :/ t1) (h2 :/ t2) = > AND (TREPEQ h1 h2) (TREPEQL t1 t2) That is it. These are the all clauses. Again, I have already defined them, and it works in GHC 7.0. Certainly I would be grateful if GHC blessed them with a special attention so they run faster. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime