[Prev][Next][Index][Thread]
Undecidable Second-order Type-Scheme Problem
Date: Mon Oct 23 14:28:50 GMT+0100 1989
Assuming the undecidability of the semiunification problem for a language
without constants (as stated in a previous message on the Type Net) we can
prove that:
it is undecidable if a (closed) lambda-term M has a second order type
that is a (substitution) instance of the type (scheme) t. I.e.,
there is a simple substitution S such that |- M:St.
Type schemes and simple substitutions are defined in our paper [1].
Type schemes are description of second order types in which we only fix
the first order structure (arrows and repeated patterns) of the type. Simple
substitutions map type schemes in second order types.
To prove the result we define a lambda-term M and a type scheme t such that
|-M:St for some S, if and only if a given semiunification problem
{(t1,u1),...,(tn,un)} has a solution. (The hypothesis that M is closed is
just for simplicity.)
Of course the result does not imply the undecidability of the inference
problem for the second order lambda-calculus.
Paola Giannini, Simona Ronchi.
[1] Paola Giannini, Simona Ronchi, "Characterization of typings in polymorphic
type discipline" LICS 88