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
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
