Functional dependencies, principal types, and decidable
typechecking
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Apr 5 21:56:47 EDT 2005
Simon Peyton-Jones wrote:
> | > {-# OPTIONS -fglasgow-exts #-}
> | >
> | > class C a b c | a b -> c where
> | > foo :: (a, b) -> c
> | >
> | > instance C a a r => C a (b, c) r where
> | > foo (a, (b, c)) = foo (a, a)
>
> You are already on dodgy ground here, because the instance decl doesn't
> guarantee that the bit before the => is smaller than the bit after the
> =>. E.g. context reduction could go:
> C (Int,Int) (Bool, Bool) r
> --> C (Int,Int) (Int,Int) r
> --> C (Int,Int) (Int,Int) r
>
> So [Point 1]: GHC should require -fallow-undecidable-instances if you
> use repeated type variables before the =>.
Yes, I think that would be a good idea.
> | Now, in GHCi (version 6.4),
> |
> | > *FDs> let bar x = foo ((x, x), (x, x))
> | > *FDs> :t bar
> | > bar :: (C (a, a) (a, a) c) => a -> c
> |
> | but GHC is also happy to accept the more general type
> |
> | > bar :: a -> c
> | > bar x = foo ((x, x), (x, x))
>
> There are two separate things going on here
>
> [Point 2] GHC postpones context reduction until it's forced to do it
> (except if a single step will eliminate the dictionary altogether).
> Example:
>
> data T a = T a
> instance Eq (T a)
> bar x = [T x] == []
>
> GHC will *infer* bar :: Eq [T a] => a -> Bool, but it will happily
> *check*
> bar :: a -> Bool
> bar x = [T x] == []
>
> The reason for this lazy context reduction is overlapping instances; in
> principle there might be more instances for Eq [T a] at bar's call site.
>
> But now I look at it again, I think it would be OK to postpone context
> reduction only if there actually were overlapping instances (right here
> at bar's defn). That might be a good idea because it'd give less
> confusing types perhaps.
>
> However, note that the two types are indeed equivalent -- both are more
> general than the other. It's like saying (Eq Int => t) <= t,
> and vice versa.
Semantically, I understand that the constraint "C ((x, x), (x, x) a)"
does not constrain the two type variables "x" and "a" (and hence, the
two types are equivalent), but I don't see how you can derive that with
the constraint entailment rules
\theta \in P
------------
P ||- \theta
P ||- forall a.\theta
---------------------
P || [t/a]\theta
P || p => \phi P ||- p
------------------------
P ||- \phi
which I thought are those underlying GHC's type system.
> | Again, in GHCi,
> |
> | > *FDs> let bar x = foo ((x::Int, x), (x, x))
> | > *FDs> :t bar
> | > bar :: Int -> ()
> |
> | (which by itself is bizarre)
>
> This is the first time when the functional dependency plays a role.
> >From bar's right-hand-side we get the constraint (C (Int,Int) (Int,Int)
> c), and the type (Int -> c). Now GHC tries to decide what to quantify
> over. Shall we quantify over c? Well, no. GHC never quantifies over
> type variables that are free in the environment (of course) OR are fixed
> by functional dependencies from type variables free in the environment.
> In this case the functional dependencies tell us that since (Int,Int) is
> obviously completely fixed, then there's no point in quantifying over c.
>
>
> So bar is not quantified. The constraint (C (Int,Int) (Int,Int) c) is
> satisfied via the recursive dictionary thing, leaving 'c' completely
> unconstrained. So GHC chooses c to be (), because it doesn't like to
> leave programs with completely free type variables.
>
> | but it also accepts
> |
> | > bar :: Int -> c
> | > bar x = foo ((x::Int, x), (x, x))
>
> Here you are *telling* GHC what to quantify over, so the inference of
> what to quantify doesn't happen.
I accept that this is the process by which GHC computes these types, but
it does violate the principal types property, doesn't it? The relation
Int -> () <= forall c. Int -> c
does not hold.
Summary
~~~~~~~
So it seems to me that
* MPTCs with recursive dictionary construction seem to require a
semantic model of subsumption (as the normal constraint entailment rules
would lead to infinite trees).
* MPTCs with recursive dictionary construction and FDs break principal
types.
I guess that's all ok provided GHC enforces the use of
-fallow-undecidable-instances for any instances that need recursive
dictionaries.
Manuel
More information about the Glasgow-haskell-users
mailing list