TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

> 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.