termination for FDs and ATs
Simon Peyton-Jones
simonpj at microsoft.com
Fri May 5 03:42:12 EDT 2006
| The important question is whether this will retain *complete* type
| inference? For example, in case of type annotations we need to
| test for equivalence among constraints.
An excellent question. Here's an example, adapted from Ross:
class C a where
type Result a
method :: a -> Result a
instance C (Maybe a) where
type Result (Maybe a) = Bool
g :: (a->a) -> Int
g f = 3
w ::Int
w = g (\b x -> if b then Just (method x) else x)
Now, as Ross pointed out, the (\b x->...) expression has inferred type
(a = Maybe (Result a), C a) => Bool -> a -> a
Alas, g simply discards its argument, so there are no further
constraints on 'a'. I think Martin would argue that type inference
should succeed with a=Bool, since there is exactly one solution. Is
this an example of what you mean?
However, as a programmer I would not be in the least upset if inference
failed, and I was required to add a type signature. I don't expect type
inference algorithms to "guess", or to solve recursive equations, and
that's what is happening here. (Notice that it's quite hard to set up
this problem. First you need a program whose equality constraints become
recursive. Then you need to arrange that the type variables in the
recursion are not mentioned elsewhere -- if they were, they'd be
instantiated there, and everything would be ok.)
What I am less sure of is how to *specify* the type system so that it
describes these hard-to-infer programs as illegal. Presumably it's a
question of setting up the entailment system so that it has limited
rules of deduction -- more limited than first order logic.
Simon
More information about the Haskell-prime
mailing list