[Haskell] Re: type class instance selection & search

[apfelmus]

Conal Elliott wrote:
> I keep running into situations in which I want more powerful search in
> selecting type class instances.  One example I raised in June, in which all
> of the following instances are useful.
> 
>> instance (Functor g, Functor f) => Functor (O g f) where
>>   fmap h (O gf) = O (fmap (fmap h) gf)
> 
>> instance (Cofunctor g, Cofunctor f) => Functor (O g f) where
>>   fmap h (O gf) = O (cofmap (cofmap h) gf)
> 
>> instance (Functor g, Cofunctor f) => Cofunctor (O g f) where
>>   cofmap h (O gf) = O (fmap (cofmap h) gf)
> 
>> instance (Cofunctor g, Functor f) => Cofunctor (O g f) where
>>   cofmap h (O gf) = O (cofmap (fmap h) gf)
> 
> My understanding is that this sort of instance collection doesn't work
> together because instance selection is based only on the matching the head
> of an instance declaration (part after the "=>").  I'm wondering why not use
> the preconditions as well, via a Prolog-like, backward-chaining search for
> much more flexible instance selection?

There are some fundamental problems/design choices for type classes in
conjunction with separate compilation/modularity that need to be
researched before trying anything like that. In particular, any ad-hoc
Prolog, CHR or -fallow-undecidable-instances just ignores these problems
and doesn't solve them.

The problem with the Functor/Cofunctor instances is that they are
ambiguous as soon as a type constructor  X  is made an instance of both
 Functor  and  Cofunctor . Of course, such an  X  cannot exist in a
mathematically useful way (really ?) but the current system doesn't
allow to tell this to the compiler. Alas, we can always say

  instance Functor F where
    fmap   = undefined
  instance Cofunctor F where
    cofmap = undefined

The problem is not so much that there might be ambiguities, but how to
detect and when to report them. Consider:

  module F where
    class Functor f
    class Cofunctor f

  module O where
    import F

    data O f g a
    instance (Functor g,   Functor f  ) => Functor (O g f)
    instance (Cofunctor g, Cofunctor f) => Functor (O g f)

  module X where
    import F

    data X a
    instance Functor   X
    instance Cofunctor X

  module Unsound where
    import F
    import O
    import X

    type Unsound a = O X X a

The current design rejects module O.
- Another possible design choice is to reject only module Unsound, i.e.
when the conflicting instance declarations both come into scope. But it
may be tricky/undecidable to to detect such conflicting instances.
- A third possibility is to reject module X based on hypothetical
information from module F that states that the instances of Functor and
Cofunctor are disjoint.
- The fourth choice is to not reject any module but to wait until a
function really uses the type  Unsound a  and to reject this function.
This is probably a bad idea since this may delay the error even further
to modules that import Unsound.


While we're at it, another rather often requested feature of type
classes that needs considerable thinking is explicit instance
import/export. With this one, we could make module X "locally sound" by
simply not exporting either the Functor or the Cofunctor instance.

  module X (X, instance Functor X) where ...

Currently, all instances are globally visible. The problem with explicit
import/export is that program correctness depends on global visibility!
Consider the following example (due to Bertram Felgenhauer):

  module A where
    newtype A = A Int deriving (Eq)

  module OrdA1 (lookup1) where
    import A
    import Data.Map

       -- don't export this instance
    instance Ord A where
      compare (A x) (A y) = compare x y

    lookup1 :: A -> Data.Map A a -> Maybe a
    lookup1 = Data.Map.lookup

  module OrdA2 (lookup2, m) where
    import A
    import Data.Map

       -- don't export this instance
    instance Ord A where
      compare (A x) (A y) = compare y x

    lookup2 :: A -> Data.Map A a -> Maybe a
    lookup2 = Data.Map.lookup

    m       = Data.Map.fromList $ zip [1..] [1,2,3,4]

  module Wrong where
    import Data.Map
    import OrdA1
    import OrdA2

    wrong = lookup1 1 m == lookup2 1 m

Here, the module Wrong has two lookup functions with different
invariants on one and the same map type. In other words, the different
Ord instances for A will mess up the invariants of the  Map A a
implementation and will eventually even lead to pattern match failures.
Being able to mess up invariants by class export/import is quite dangerous.


Regards,
apfelmus