UndecidableInstances: Ugly or Evil incarnate?

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

Okay, we seem to be having a debate where, to caricature only a
little, I'm arguing that Fundeps/UndecidableInstances are ugly but
useful, and other people are arguing that they are truly absolutely
horrible in their current GHC implementation.  I think the debate
boils down to where you see the scope of the implicit universal
quantification of free type variables in instances.

Consider the following:

    class C a b | a -> b where
       aDefault :: a
       aTobC :: a -> b
    class D a b where                     -- no fundep
       aTobD :: a -> b
    instance (D Int b) => C Int b where   -- should this be allowed?
       aDefault = 0
       aTobC = aTobD

GHC accepts this above code, which makes sense to me because I read
the instance declaration as essentially (in pseudo-Haskell):

	forall b. instance (D Int b) => C Int b

or, equivalently:

	instance C Int (forall b. (D Int b) => b)

In English, "there's only one instance of C with (a ~ Int), but, in
that instance, the aTobC method returns a value of type b for any b
you want, except that in order to produce the value, it needs access
to an appropriate dictionary of class D."  One corollary of this view
is that it is impossible to violate functional dependencies without
defining more than one instance of a class.

The alternate reading (and please correct me if I'm mis-characterizing
the argument), is that we should apply the functional dependencies of
a class to each individual instance, where any universal
quantification happens across the fundep.  According to this view, we
should read C's instance declaration as:

	forall b. (instance (D Int b) => C Int b | Int -> b)

and find that "forall b. ... | Int -> b" fails.  Hence, we have
violated functional dependencies with a single instance of the class.


There's a less explicit but equally important question underlying this
discussion about how much contexts should play into instance
validation.  Some have suggested GHC should reject the above instance
of C, but should nonetheless accept the following instance of C':

	class C' a b | a -> b
	class E a b | a -> b       -- unlike above, we now have a fundep
	instance (E a b) => C' a b

Oleg, you haven't weighed in this specific question, but I think many
of your ideas require the ability to write instances like C', even if
you advocate disallowing C.

On this question, I am opposed, because I find it too reminiscent of
an aspect of C++ I dislike, namely that ad-hoc polymorphism interacts
with templates, implicit promotion, and the most-specific match rule
to make it hard to understand code.  (And since, unlike C++, Haskell
allows polymorphic return types, there's a potential for things to get
even more complicated.)

Fortunately, GHC's current approach is quite simple:  The instance
head is always sufficient to determine whether or not an instance
matches, two instances overlap, or functional dependencies are
violated.  The context may tell you what dictionaries must be around
if you actually want to use an instance, but if you know that a
program compiles, you can ignore the context when reading and
reasoning about the code.

Another reason that I oppose too much reliance on the context is that
I want the ability to load code dynamically.  If the assumption about
ground type equality is pushed too far--e.g., allowing coercion based
on reasoning about fundeps--then dynamically loading modules with
contradictory fundeps could undermine memory safety.  One of my
objections to type families is the difficulty of guaranteeing safety
in the presence of dynamic loading.


At any rate, this is the haskell-prime mailing list, not the
how-much-do-you-hate-some-current-ghc-option-implementation list.
I've already taken a lot of people's time with this thread, so let me
propose to do something useful for the haskell prime effort.  I could
start a compilation (probably a wiki page) of things you can do or
might want to do with fundeps and undecidable/overlapping instances.
This could serve as a kind of wish list for Haskell prime.  Examples
off the top of my head might be:

   - Type-safe dynamic loading

   - Sqrt(N) reduction in code size for mtl instances

   - HList/OO-Haskell

   - Enforcing simple recursively-defined properties on types.  (E.g.,
     with GHC 7.2's new generic deriving framework, you might want to
     specify the constraint that a type's Representation doesn't
     include NoSelector.)

   - Using data types to represent ad-hoc polymorphic functions you
     can pass as arguments to functions.  E.g., using a class like:

         class Function f a b | f a -> b where
            funcall :: f -> a -> b

     you can define types f of class Function and use them to do maps
     over tuples.

Someone thinking of implementing an idea (e.g., closed type families)
could look at the wish list and determine out how much of it the new
feature would cover.  Others could add to the wish list.  Oleg, I
realize the list might resemble your bibliography, but the idea would
be to list the simplest possible cases (like C' above), rather than
examples that unleash the full power of the extension.  We can link to
your web site for people who want to delve deeper into the motivation.

If that sounds like a useful idea, the next question is where to put
such a list.  The Haskell prime wiki seems like a logical place, but
it should be someplace where multiple people can edit it.  (And,
though I have an account on the Haskell prime wiki, username David, I
can't seem to edit stuff there.)

David