Re: coherence when overlapping?
It seems that the subject is a bit more complex, and one can force GHC to choose the less specific instance (if one confuses GHC well enough): see the example below. First of all, the inequality constraint is already achievable in Haskell now: "TypeEq t1 t2 False" is such a constraint. One can write polymorphic functions that distinguish if the argument a list (any list of something) or not, etc. One can write stronger invariants like records where labels are guaranteed to be unique. There are two problems: first there are several notions of type inequality, all of which are useful in different circumstances. http://www.haskell.org/pipermail/haskell-prime/2006-March/000936.html Second, how inequality interacts with functional dependencies -- and in general, with the type improvement. And here, many interesting things emerge. For example, the following code
{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} {-# OPTIONS -fallow-overlapping-instances #-}
module Foo1 where
class C a b | a -> b where f :: a -> b
instance C Int Bool where f x = True
instance TypeCast Int b => C a b where f x = typeCast (100::Int)
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
class D a b | a -> b where g :: a -> b
instance D Bool Bool where g x = not x
instance TypeCast a b => D a b where g x = typeCast x
test1 = f (42::Int) -- ==> True test2 = f 'a' -- ==> 100
test3 = g (1::Int) -- ==> 1 test4 = g True -- ==> False
bar x = g (f x) `asTypeOf` x
We see that test1 through test4 behave as expected. We can even define the function 'bar'. It's inferred type is *Foo1> :t bar bar :: (C a b, D b a) => a -> a The question becomes: is this a function? Can it be applied to anything at all? If we apply it to Int (thus instantiating the type a to Int), the type b is instantiated to Bool, and so (following the functional dependency for class D), the type a should be Bool (and it is already an Int). OTH, if we apply bar to anything but Int, then the type b should be Int, and so should the type a. Liar's paradox. And indeed, bar cannot be applied to anything because the constraints are contradictory. What is more interesting is the slight variation of that example:
class C a b | a -> b where f :: a -> b
instance C Int Int where f x = 10+x
instance TypeCast a b => C a b where f x = typeCast x
class D a b | a -> b where g :: a -> b
instance D Int Bool where g x = True
instance TypeCast Int b => D a b where g x = typeCast (10::Int)
test1 = f (42::Int) test2 = f 'a'
test3 = g (1::Int) test4 = g True
bar x = g (f x) `asTypeOf` x
test5 = bar (1::Int)
*Foo> :t bar bar :: (C a b, D b a) => a -> a If bar is applied to an Int, then the type b should be an Int, so the first instance of D ought to have been chosen, which gives the contradiction a = Bool. And yet it works (GHC 6.4.1). Test5 is accepted and even works *Foo> test5 10
one can force GHC to choose the less specific instance (if one confuses GHC well enough): see the example below.
your second example doesn't really do that, though it may look that way.
class D a b | a -> b where g :: a -> b instance D Int Bool where g x = True instance TypeCast Int b => D a b where g x = typeCast (10::Int) .. bar x = g (f x) `asTypeOf` x test5 = bar (1::Int) *Foo> :t bar bar :: (C a b, D b a) => a -> a
If bar is applied to an Int, then the type b should be an Int, so the first instance of D ought to have been chosen, which gives the contradiction a = Bool. And yet it works (GHC 6.4.1). Test5 is accepted and even works *Foo> test5 10
your argument seems to imply that you see FD range parameters as outputs of the instance inference process (*), so that the first Int parameter in the constraint D Int Int is sufficient to select the first instance (by ignoring the Int in the second parameter and using best-fit overlap resolution), leading to the contradiction Int=Bool. alas, current FD implementations don't work that way.. Hugs will complain about the overlap being inconsistent with the FD, for both C and D - does it just look at the instance heads? GHC will accept D even without overlapping instances enabled, but will complain about C, so it seems that it takes the type equality implied by FDs in instance contexts into account, seeing instances D Int Bool and D a Int - no overlaps. similarly, when it sees a constraint D Int Int, only the second instance head will match.. if you comment out the second C instance, and disable overlaps, the result of test5 will be the same.
First of all, the inequality constraint is already achievable in Haskell now: "TypeEq t1 t2 False" is such a constraint.
as you noted, that is only used as a constraint, for checks after instantiation, which is of little help as current Haskell has corners that ignore constraints (such as instance selection). specifically, there is a difference between the handling of type equality and type inequality: the former can be implied by FDs, which are used in instance selection, the latter can't and isn't (which is why I'd like to have inequality constraints that are treated the same way as FD-based equality constraints, even where constraints are otherwise ignored). if we want to formalise the interaction of FDs and overlap resolution, and we want to formalise the latter via inequality guards, then it seems that we need to put inequality constraints (negative type variable substitutions) on par with equality constraints (positive type variable substitutions). cheers, claus (*) or does it seem to me to be that way because that is how I'd like FD range parameters to be treated?-)
participants (2)
-
Claus Reinke -
oleg＠pobox.com