[Haskell-cafe] Limits of deduction

[Matthew Brecknell]

Roberto Zunino:
> Yes, you are right, I didn't want to involve type classes and assumed 
> 3::Int. A better example would be:
> 
> polyf :: Int -> a -> Int
> polyf x y = if x==0 then 0
>              else if x==1 then polyf (x-1) (\z->z)
>              else polyf (x-2) ()
> 
> Here, passing both () and (\z->z) _does_ make inference fail.

Alternatively, type inference succeeds in rejecting an illegal program
[1,2]. :-)

So I think we need to be a little more precise about exactly what is
undecideable in this example. Yes, the explicit type signature you've
given is valid, and the Hindley-Milner type inference algorithm is not
able to assign that type without an explicit signature. But that doesn't
make Hindley-Milner type inference undecideable. On the contrary,
Hindley-Milner type inference is deliberately designed to be decideable.
To achieve that, it assumes monomorphic types in certain identifiable
contexts, and therefore rejects some functions for which valid types
exist.

So I think the point you were making is that the problem of inferring
the types of all functions for which valid types exist is, in general,
undecideable. Hindley-Milner inference ensures decideability by choosing
a somewhat less general (but still useful) problem.

For what it's worth (not much), it might be possible to invent a
decideable type inference which could infer types for a slightly larger
set of functions (including polyf), by automatically generalising the
types of arguments which are not inspected. Of course, doing so would
presuppose the decideability of the subproblem of identifying unused
arguments, and achieving that would undoubtedly require certain
restrictions on the subproblem definition, analogous to the ones
employed by Hindley-Milner.

[1] http://haskell.org/onlinereport/decls.html#sect4.1.4
[2] http://haskell.org/onlinereport/decls.html#sect4.5