[Haskell-cafe] Proposal to solve Haskell's MPTC dilemma

[Carlos Camarao]

On 21 May 2010 01:58, Carlos Camarao <carlos.camarao at gmail.com>  wrote:

>> But this type-correct program would become not typeable if
>> instances such as the ones referred to before (by Daniel Fischer) ...

> It seems that single param type classes enjoy a nice property: ...
> * Adding an instance to the module defining the class cannot conflict
> with any non-orphan instance defined elsewhere ...

Max, thanks very much for your message. I will defer comments about
definitions of orphan instances to a postscript. First I'd like to say the
following.

I think that a notion of orphan instances based on whether an
instance is defined or not in the module where the class of the
instance is defined is not very nice, because classes have global
scope and then it should not matter in which module a class is
defined, as long as it is defined somewhere in the current or some
imported module.

Let us thus not try to extend a definition based on this to MPTCs.
However, the module fragility issue you raised is quite relevant. Let
us call a type-correct module M fragile if definitions inserted in
modules imported by M cause M to become type-incorrect.

This issue is more relevant in Haskell than in other languages because
instance definitions are automatically imported when a module is
imported, and importation of an instance cannot be forbidden.

Our "unreacheable_var-implies-overloading_resolution_test" proposal
can be viewed as a proposal to
"test-visible-instances-before-considering-types-as-ambiguous".
Ambiguity means the existence of two or more conflicting definitions
that could be used in an expression (and the inexistence of a
reasonable criteria for selecting between conflicting definitions). In
Haskell, nowadays, ambiguity is reported without looking to see if
there really are conflicting definitions. What FDs do is to require
programmers to specify dependencies between class variables which make
the compiler look to see if there exist definitions that can satisfy
such dependencies, before reaching any conclusion that an expression
is ambiguous. What we propose (relieving the burden on programmers) is
to make the compiler look itself to see if there exist two or more
(well, or none) definitions and report error only if this is the case
(again, before reaching any conclusion that an expression is
ambiguous). If there is exactly one instance definition, there is no
ambiguity (there is no conflict); in such case, then: use that single
definition that the programmer defined.

A benefit of adopting our approach would be that defaulting would
become unnecessary (defaulting always occurring in favor of visible
definitions).

Module robustness can be achieved --- even maintaining automatic
importation of instance definitions --- by considering, for each
instance definition, say I, defined by

   instance C bla1 I bla2 where ...

that an automatic defaulting rule that names C
(see hackage.haskell.org/trac/haskell-prime/wiki/Defaulting) is
virtually and automatically inserted, namely:

   default C bla1 I bla2

It should perhaps be noted though that one could have more than one such
automatic default rule for the same class.

Cheers,

Carlos

=====================================================================
PS: I think that a definition of orphan/non-orphan instance definition
for MPTCs should be different.

Letting:
   defM(C)               = module where C is defined
   local-datatype(T,M,C) = T is defined in M or T is defined in defM(C)

   import-list(M,C) = {M} U { import-list(M') | M imports M'}
   instance-def(I,C,M,tv) = I is an instance definition of class C,
occurring in
                              module M, that instantiates class variable tv
then you consider (if I have correctly understood and expressed what
you wrote):

Non-orphan = [for all I,C,M,tv: instance-def(I,C,M,tv) =>
local-datatype(T,M,C)]
Orphan     = [there exists I,C,M,tv: instance-def(I,C,M,tv) ^ not
local-datatype(T,M,C)]

And I think a correct definition of orphan/non-orphan for MPTCs should
be along the line:

Non-orphan = [there exists I,C,M,tv: instance-def(I,C,M,tv) ^
local-datatype(T,M,C)
Orphan     = [forall I,C,M,tv: instance-def(I,C,M,tv) ^ not
local-datatype(T,M,C)]

That is, an instance should be considered non-orphan if there exists
at least one datatype to which a class type variable in such instance
is instantiated, because other instances which instantiated such class
type variable to such datatype would be non-orphan.

GHC is thus correct, I think.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100522/509b1876/attachment-0001.html