TypeFamilies vs. FunctionalDependencies & type-level recursion

[AntC]

 <oleg at ...> writes:

> I'd like to have type-level type representations to _implement_
> overlapping type function equations. With type level Typeable, you
> would not need to do anything about point 2 therefore. The problem 2
> will be solved.
> 
> > There seems no reason in principle to disallow
> > 	type instance F where
> > 	  F Int = Bool
> > 	  F a = [a]
> 
> I would implement this as follows:
> 
> > type instance F x = F' (EQ (TYPEOF x) INT) x
> > type family F' trep x
> > type instance F' TRUE  x = Bool
> > type instance F' FALSE x = [x]
> 

Thanks Oleg. I'm familiar with that style from HList, but it still seems 
cumbersome to me (compared to separate equations). I suppose a type-level if-
then-else would be possible? Does this read any better?

    type instance F x = IF (EQ (TYPEOF x) INT) Bool [x]

I note there by the way, that INT ~ (TYPEOF Int), is that upshifting the name 
going to work well for all Prelude types?
    How about (TYPEOF ()) or (TYPEOF [a])?
The EQ seems somehow redundant. We can only test type (reps) for equality, or 
do you envisage inducing some ordering over typereps?

How scalable is your approach with multi-argument type functions? Such as:

    module Mine where
      type family F a b

      data Mine = ...
      type instance F Mine Int = ...
      type instance F Mine y   = ...          -- overlap on 2nd arg

    module Yours where
      import Mine

      data Yours = ...
      type instance F Yours Bool = ...         -- no overlap with F Mine b
      type instance F Yours y   = ...          -- overlap on 2nd arg

We'd need a clan of helper functions F'Mine, F'Yours, etc.

This multi-argument example also goes against closed type families, I think.


> 
> Finally, could GHC automatically derive instances of TTypeable, which
> maps types to TYPEREP:
> 	type family TTypeable (x :: *) :: TYPEREP
> 

I can see that if we went the route of type-level Typeable, it would need 
compiler support. But do we need that? Would it be sufficient to have a 
compiler-supported if-then-else type equality? Perhaps IFEQ, like this:

    type instance F a = IFEQ a Int Bool [a]
    type instance F a = (a ?~ Int) Bool [a]     -- over-exotic syntax?

To be fair to the design you've put into TTypeable, we'd also need to handle 
polymorphic/partly-ground/higher-ranked types:

    type instance G a          = IFEQ a (Maybe b) b ()
    type instance IsFunction a = IFEQ a (_ -> _) TRUE FALSE   -- the classic
    type instance IsNum a      = IFEQ a (Num b => b) a Int

And that last example is a worry: what we're calling a type equality test is 
really a test for unifiability.

AntC