Subject: Re: type class instance selection & search Newsgroups: gmane.comp.lang.haskell.general Date: Wednesday 1st August 2007 12:41:22 UTC (over 10 years ago) 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 |
|||