technique to allow innocuous ambiguity in instance declarations?
Brief disclaimer: I'm using GHC 6.4.1 and haven't looked into Hugs; but I don't suspect there's much difference on this issue. Could easily be wrong there. I've hit a bit of a road bump in ambiguity regarding type class instances and transformer types (in the style of monad transformers). The interesting point is that, in this case, I believe that the ambiguity is harmless and that all possible derivations of instances would be extensionally equivalent. But the typechecker won't let me get far enough to test that hypothesis. So, I have a relation C and intuition that the property can be carried through transformations on either of its related types. I'm seeking 1) a suggested technique for formulating that intuition in such a way that the type-checker could act on it 2) a suggestion claiming that such a harmless ambiguity is down right impossible Below is pseudo-code outlining the shape of my problem. Consider a 2 parameter (both are type constructors) class:
class C f g where nest :: f a -> g a
I have instances for base types (analogous to the Identity monad).
class C IdL IdR where nest = ...
I also have transformers that I can apply to these base types and instances that correspond to "lifting" the C type class property through the transformers.
class C f g => C f (TransR g) where nest = ... code that involves the "nest" of the C f g instance ...
or
class C f g => C (TransL f) g where nest = ... code that involves the "nest" of the C f g instance ...
The simple version of my issue is that, give the instances so far, the compiler won't derive an instance for T.
type T = C (TransL IdL) (TransR IdR)
The impasse is the ambiguity in the derivation from C IdL IdR to T. One could apply first TransL or apply first TransR. The "-fallow-overlapping-instances" type system extension fails to help because there is no "most specific" instance. The order of application of my transformers (i.e. transforming the left or transforming the right parameter) does not seem to matter--I have found no intuition that says the derivations ought to be distinguishable in anyway. My question: Is there a technique to allow such innocuous ambiguity in instance declarations? I experimented with introducing something akin to a trace in a third parameter to the class which would disambiguate the derivation (by specifying the order of the transformations; reminded me of "Strongly typed heterogeneous collections"), but had no luck there (perhaps someone else would). Because the ambiguity does not matter to me, I'd be fine implementing a rule such as "always transform the left parameter first", but I don't know how to/if I can formulate that in Haskell. I also tried to reduce the class to a single parameter, which incorporated the the functors into a single type. The method of the class needs those functor types available, so that approach sputtered out. Another issue is modularity: both of my attempts above would have bloated the code using the class with the details needed to disambiguate it. I certainly prefer the context "C f g" to one that exposes the disambiguation. That is, I would highly prefer a solution that allows h1 instead of h2.
h1 :: C f g => a type h1 = ... some code with nest ...
h2 :: (C f g, DisambiguationHelper f g ?) => a type h2 = ... some code with nest ...
My harrowing suspicion is that I will need to split the property into two--something I can't readily see how to do. Thanks for your time, Nick
Nicolas Frisby posed a problem about controlling the order of instance selection rules (or, the application of type improvement rules) Given the following code
newtype IdL a = IdL a newtype IdR a = IdR a
class C f g where nest :: f a -> g a
instance C IdL IdR where nest (IdL x) = IdR x
newtype TransR f a = TransR (f a) newtype TransL f a = TransL (f a)
instance C f g => C (TransL f) g where -- Instance1 nest (TransL x) = nest x
instance C f g => C f (TransR g) where -- Instance2 nest x = TransR (nest x)
we can quite happily write
test1 :: TransL IdL a -> IdR a test1 = nest
and ditto
test2 :: IdL a -> TransR IdR a test2 = nest
but we can't write
testx :: TransL IdL a -> TransR IdR a testx = nest
because the typechecker doesn't know which instance to choose: either to attempt to improve constraints as C (TransL IdL) (TransR IdR) --> C IdL (TransR IdR) --> C IdL IdR (choosing the Instance1 first) or C (TransL IdL) (TransR IdR) --> C (TransL IdL) IdR --> C IdL IdR choosing Instance2 first. One can see that the end result is just the same. But the typechecker doesn't actually know that instances commute, so it reports the ambiguity and quits. But suppose we do know that these particular instances commute. How to impart this knowledge to the typechecker? Or, simply, how to tell the typechecker to remove the ambiguity by choosing Instance1 first? It turns out, there is a simple way. It relies again on this quite useful contraption, TypeCast. The idea is to introduce the most general instance C f g. The typechecker will choose it if nothing more specific applies. And then we examine f and g to see what we've got and how to proceed from that. At that point, it's us who decides what to improve first. The idea is similar to the one described in http://pobox.com/~oleg/ftp/Haskell/types.html#is-function-type The complete code follows. Now testx typechecks.
{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} {-# OPTIONS -fallow-overlapping-instances #-}
module N where
newtype IdL a = IdL a newtype IdR a = IdR a
class C f g where nest :: f a -> g a
instance C IdL IdR where nest (IdL x) = IdR x
newtype TransR f a = TransR (f a) newtype TransL f a = TransL (f a)
instance (IsTransL f b, C' b f g) => C f g where nest = nest' (undefined::b)
class C' b f g where nest' :: b -> f a -> g a
instance C f g => C' HTrue (TransL f) g where nest' _ (TransL x) = nest x
instance C f g => C' HFalse f (TransR g) where nest' _ x = TransR (nest x)
{- From the first attempt instance C f g => C (TransL f) g where nest (TransL x) = nest x
instance C f g => C f (TransR g) where nest x = TransR (nest x) -}
test1 :: TransL IdL a -> IdR a test1 = nest
test2 :: IdL a -> TransR IdR a test2 = nest
testx :: TransL IdL a -> TransR IdR a testx = nest
data HTrue data HFalse
class IsTransL (a :: * -> * ) b | a -> b instance TypeCast f HTrue => IsTransL (TransL y) f instance TypeCast f HFalse => IsTransL a f
-- Our silver bullet
class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x
participants (2)
-
Nicolas Frisby -
oleg＠pobox.com