TypeFamilies vs. FunctionalDependencies & type-level recursion
anthony_clayden at clear.net.nz
Thu May 24 02:37:56 CEST 2012
<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
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
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.
More information about the Haskell-prime