TypeFamilies vs. FunctionalDependencies & type-level recursion

[David Mazieres]

I'm not sure if these extensions are still under discussion or if the
topic is dead (wiki pages 5 years old).  However, the Haskell' wiki
page for FunctionalDependencies suggests AssociatedTypes is a more
promising approach, yet the AssociatedTypes page misses a major Con
compared to FunctionalDependencies that I think should be there.

One of the more disgusting but also powerful implications of
FunctionalDependencies is that, in conjunction with
OverlappingInstances and UndecidableInstances, you can do recursive
programming at the type level.  This has been (ab)used to do some cool
things (e.g., HList, HaskellDB, OOHaskell).

As an example, consider the following simple (key, value) lookup
function that operates at the type level (inspired by HList):

	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE OverlappingInstances #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE UndecidableInstances #-}

	data HNil = HNil deriving (Show)
	data HCons h t = h :* t deriving (Show)
	infixr 2 :*

	data A = A deriving (Show)
	data B = B deriving (Show)
	data C = C deriving (Show)

	abc :: HCons (A, Int) (HCons (B, Int) (HCons (C, Int) HNil))
	abc = (A, 1) :* (B, 2) :* (C, 3) :* HNil

	class HLookup k l v | k l -> v where
	    hLookup :: k -> l -> v
	instance HLookup k (HCons (k, v) l) v where
	    hLookup _ (h :* t) = snd h
	instance (HLookup k l v) => HLookup k (HCons h l) v where
	    hLookup k (h :* t) = hLookup k t

	b :: Int
	b = hLookup B abc               -- Returns 2

The key to hLookup is that OverlappingInstances selects the most
specific match, thereby breaking the recursion when the requested key
type matches the key of the pair at the head of the list.  By
contrast, TypeFamilies cannot permit a function such as hLookup.  One
may try something along the lines of:

	class HLookup k l where
	    type HLookupResult k l
	    hLookup :: k -> l -> HLookupResult k l
	instance HLookup k (HCons (k, v) l) where
	    type HLookupResult k (HCons (k, v) l) = v
	    hLookup _ (h :* t) = snd h
	instance (HLookup k l) => HLookup k (HCons h l) where
	    type HLookupResult k (HCons h t) = HLookupResult k t
	    hLookup k (h :* t) = hLookup k t

But now you have overlapping type synonyms, which pose a safety threat
where the more-specific instance is not in scope.  Therefore, Haskell
likely cannot be extended to accept code such as the above.

One possible extension that *would* enable type-level recursive
programming is the ability to constrain by inequality of types.  I
noticed GHC is on its way to accepting "a ~ b" as a constraint that
types a and b are equal.  If there were a corresponding "a /~ b", then
one might be able to say something like:

	instance HLookup k (HCons (k, v) l) where
	  ...
	instance (h /~ (k, v), HLookup k l) => HLookup k (HCons h l) where
	  ...

Of course, I have no idea how the compiler could know such constraints
are sufficient to avoid overlapping types.  I suspect figuring it out
would be hard given that instance matching happens before context
verification and that the overlapping errors must happen at instance
matching time.

My bigger point is that if the Haskell' committee ever considers
adopting one of these proposals or one intended to supersede them, I
hope there is a way to do recursive type-level programming.  A likely
corollary is the need for a mechanism to avoid instance overlap
between recursive and base cases by asserting type inequality in the
recursive case.

David