TypeFamilies vs. FunctionalDependencies & type-level recursion

[dm-list-haskell-prime at scs.stanford.edu]

Thanks for the responses.  I realized after sending the message that
it wasn't clear exactly what I was advocating, which is probably more
modest that what people are thinking.

Mostly I was hoping the AssociatedTypes wiki page could be updated to
reflect that AssociatedTypes can't replace FunctionalDependencies.
(After reading the FunctionalDependencies page, I converted a bunch of
code over to TypeFamilies, thinking this would be more future-proof,
only to realize it couldn't work.)  I'm not sure what the process is
for updating the wiki, as the page is locked down, but mailing
haskell-prime seemed like a reasonable start.

I'm absolutely not advocating making overlapping instances (or, worse,
overlapping types) part of Haskell', nor under the impression that the
committee would ever consider doing so.  I'm just pointing out that
right now OverlappingInstances are the only way to do recursive
programming at the type level, for the specific reasons I outlined.  I
hope that before FunctionalDependencies or TypeFamilies or any other
type-level programming becomes part of Haskell', there is a way to
differentiate base and recursive cases *without* overlapping
instances.

The fact that TypeFamilies made it somewhat far into the process
without a way to do recursion and that the limitation is not even
documented on the wiki suggests that the Haskell' committee either
thinks people don't care or thinks about the question differently.
Either way, the point seemed worth noting somewhere.

I don't have any great ideas on supporting recursion, so I suggested a
not so great idea in my last email that abused the context.  Here's
another not so great idea that doesn't abuse the context... The point
is just that it's possible to support recursion without overlapping
instances:

Add an annotation like "| x /~ y, ..."  to instances denoting that the
instance cannot be selected unless types x and y are known to be
different.  So the code from my previous message becomes:

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

	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) | h /~ (k, v) where
            -- This is how we avoid overlap ------------> ^^^^^^^^^^^
	    type HLookupResult k (HCons h t) = HLookupResult k t
	    hLookup k (h :* t) = hLookup k t

I'm under no illusions that this specific syntax would fly, but
possibly some other proposal will allow the equivalent.

David