TypeFamilies vs. FunctionalDependencies & type-level recursion

[Dan Doel]

On Sun, May 29, 2011 at 6:45 PM, Ben Millwood <haskell at benmachine.co.uk> wrote:
> It would seem very strange to me if haskell-prime made the choice of
> fundeps/type families based on the behaviour with
> OverlappingInstances. I'm under the impression that Overlapping is
> generally considered one of the more controversial extensions, and on
> the LanguageQualities wiki page [1] it's explicitly given as an
> example of something which violates them. So not only is Overlapping
> not in the language, but I imagine there are many people (myself
> included) who would like to ensure it stays out.
>
> My personal opinion is that if Haskell wants a more complete facility
> for type-level programming, that should be addressed directly, instead
> of via creative abuse of the class system and related machinery.

It should also be noted: the fact that functional dependencies work
with overlapping instances, while type families don't is not really
inherent in functional dependencies, but is instead related to choices
about how functional dependencies work that differ from how type
families do. And mainly, this is because functional dependencies fail
to incorporate local information, meaning they fail to work
appropriately in various situations (for instance, matching on a GADT
may refine a type, but that new information may not propagate through
a fundep).

In my experience, you can construct examples that should lead to type
soundness issues with fundeps, and only fail because of peculiarities
in fundep handling. But fundeps could (and arguably should, to
interact with GADTs and the like) be reworked to behave 'properly'.
It's just that type families already do.

I can't really recall what example I used in the past, but here's one
off the cuff:

  module A where
    class C a b | a -> b where

    instance C a a where

    data T a where
      CT :: C a b => b -> T a

  module B where
    import A

    instance C Int Char where

    c :: Char
    c = case t of { CT x -> x }

So, the question is: what should happen here?

We've created a T Int in a context in which C Int Int, so it wraps an
Int. Then we match in a context in which C Int Char. But the fundep
tells us that there can only be one S such that C Int S. So we have
some choices:

1) Disallow the overlapping instance C Int Char, because it is
incompatible with the C Int Int from the other module. This is what
GHC 7 seems to do.

2) Pretend that there may in fact be more than one instance C Int a,
and so we can't infer what a is in the body of c. I think this is what
GHC used to do, but it means that whether a fundep "a -> b" actually
allows us to determine what b is from knowing a is kind of ad-hoc and
inconsistent.

3) Allow c to type check. This is unsound.

1 is, I think, in line with type families. But it rules out the
computation that fundeps + overlapping can do and type families
cannot.

Also, in an unrelated direction: there are conditions on type families
that can allow some overlapping to be permitted. For instance, if you
simply want a closed type function, like, taking the above as an
example:

    type family F a :: * where
      instance F Int = Char
      instance F a   = a

Then this is a sufficient condition for overlapping to be permissible.
And it covers a lot of the use cases for overlapping instances, I
think.

-- Dan