#1241: Functional dependencies not checked.
-------------------------------------+--------------------------------------
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal | Milestone: _|_
Component: Compiler (Type checker) | Version: 6.6
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-------------------------------------+--------------------------------------
Comment (by claus):
{{{
> GHC 6.6 (with flags {{{-fglasgow-exts -fallow-undecidable-instances}}})
is
> too liberal when accepting instances. Here is an example:
> {{{
> class F a b | a -> b where f :: (a,b)
> instance F Int b
> }}}
> The instance violates the functional dependency constraint of {{{F}}}
> because (in theory) it can be used to solve both {{{F Int Bool}}} and
{{{F
> Int Char}}}.
}}}
doesn't that depend on the interpretation of the instance? since we can
formalise any
consistent interpretation, we need to think about the intended
interpretation before we
dive into formalisations. i can think of three interpretations, in two of
which the instance
is valid because it is interpreted _as constrained by the FD_. the third
interpretation,
which Hugs seems to apply, is to interpret the instance _independent of
the FD_, then
use the FD to check whether the instance conforms to it.
i've always had problems with that third interpretation, because it
pretends that
FDs are just a _check_ on which constraints are valid. whereas the major
purpose
of FDs has always been to reduce the set of FD-valid instantiations to a
singleton
if possible, and then _to go beyond mere checking_ by _instantiating type
variables_
to the only possibly valid option.
now, since everybody seems to agree that it is fine to use FDs for type
variable
instantiation in some contexts, i don't understand why we don't do the
same in
all contexts, if only for consistency.
back to my three interpretations of "instance F Int b":
1 the instance says b is polymorphic. the FD says b is uniquely
determined.
so b is uniquely determined to be fully polymorphic. similar to GHC's
rigid type variables, it cannot be instantiated to anything but a fully
polymorphic type forall a. a.
2 the instance is polymorphic in b. the FD says b is uniquely determined.
so any constraints involving this instance have to involve mutually
consistent
instantiations of b, b_i, and the ultimate interpretation of the instance
is
instance F Int mgu(b_i). only if no mgu exists is there a conflict to
report.
3 the instance is polymorphic in b, so could be instantiated to any
specific type.
the FD says b is uniquely determined, so it cannot have differing
instantiations.
so the instance is in conflict with the FD.
GHC seems to tend towards 2, Hugs towards 3. i've listed 1 for
completeness
(although there might be other interpretations?). it would be difficult to
argue in
favour of 1, as it would amount to implicit existential quantification,
when the
general preference is towards explicit quantification. as i mentioned, i
can't think
of 3 as a consequent interpretation - the point of using a constraint
logic is to
find things that fulfill all given constraints, not to complain about
things that do not.
{{{
> class F a b | a -> b where f :: (a,b)
> instance F Int b
}}}
this would be a valid instance in 2 - there is a unique b such that F Int
b, but
we do not yet know what that is.
{{{
> x :: (Int,a)
> x = f
}}}
this is the devious part of the example. there is no doubt about the
interpretation
of the first line - if the definition type-checks, x may be used
polymorphically.
at first look, it might look as if that could be squared with
interpretation 2 of f:
the instance definition sets a bound on b on one side, x's type sets a
bound on
b on the other side, so b ends up fixed as a rigid type variable.
but this means trouble: first, it would once again smuggle in implicit
existentials,
which we don't want. second, the FD says that b is uniquely determined,
and
this right-hand side type-checks only if b is fully polymorphic, to match
x's rigid
type, but in order to switch from the rhs to the lhs, x's type goes from
rigid to
fully polymorphic itself, but since the FD fixes f's type, f has really
become
rigid, not polymorphic. (it hurts to think about this, and i'm not sure i
got it right;-)
{{{
> y :: (Int,Bool)
> y = f
}}}
valid in 2, as long as there are no conflicting instantiations of f.
incompatible
with either of x or z.
{{{
> z :: (Int,Char)
> z = x -- works, but 'z = f' does not
}}}
i don't think z=x should work, for the reasons given above. z=f would work
on its own in 2, but is incompatible with either x or y.
to sum up, while the program as a whole makes no sense, i think there is a
consistent interpretation, close to GHC's current one, in which the
instance itself
is valid, as well as use of f at one specific type. but i don't think GHC
gets this
quite right: after type-checking the rhs of x, f's type gets rigid, so
type-checking
the whole definition/declaration of x ought to fail. (i think:-)
note that i haven't even referred to the coverage condition here.
{{{
> However, with the definition `z = x` no constraint is genreated (since
`x`
> does not have an overloaded type) and all is well.
}}}
at this point, it is already too late. x=f should have generated a
constraint,
one that is in fact incompatible with the type declaration for x.
{{{
> I'm not sure what the Right Answer here is. It looks like another
fundep
> brain-bender. I'm inclined to continue working on type inference for
> associated types!
}}}
while i can understand the sentiment, i doubt that this is a real choice.
starting
from type classes (reduction of type predicates):
- associated types add a kind of semantic unification (equating types by
instantiating variables, intermingled with reduction of type functions)
- functional dependencies add syntactic unification, but we still end up
with a kind of narrowing (reduction of type predicates intermingled
with equating types by instantiating variables)
whichever way you start out, you end up with both unification and
reduction,
so the problems should be very similar in both forms, i'd suspect.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1241>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
