termination for FDs and ATs
ross at soi.city.ac.uk
Fri May 5 04:27:59 EDT 2006
On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote:
> 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?
Actually a = Maybe Bool
> 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.
I think Martin is assuming the current Haskell algorithm: infer the type
of the function and then check that it's subsumed by the declared type,
while you're assuming a bidirectional algorithm. That makes a big
difference in this case, but you still do subsumption elsewhere, so
Martin's requirement for normal forms will still be present.
More information about the Haskell-prime