[Prev][Next][Index][Thread]
Re: Typing Power of F_omega
Kucan asked the following question:
>Is a theorem of the following kind known to hold for the type system
>F_omega?
>
> For any integer n, there is an untyped term M_n such that M_n
> is not typable in F_n, but it is typable in F_n+1.
>
>F_n is the fragment of F_omega that allows type constructors of
>order up to n.
>
>I know that F_3 can type more than F_2 (or sometimes denoted by F),
>but I couldn't find any results about higher order fragments.
I dont know the answer to this question, but, in the paper:
Giannini P., Honsell F., Ronchi Della Rocca S.,
"Type Inference: some results, some problems"
which will appear in a special issue of Fundamenta Informaticae,
we state the following CONJECTURE:
The class of terms typable in F_n, for n>3, coincides
with the class of terms typable in F_3.
The conjecture is motivated by the following PARTIAL RESULT:
Let D:A|-M:a be a derivation in F_n and let n>3. If the
occurrences of type variables of order >3 in D satisfy
some constraints, then there is an effective procedure
for transforming D into a derivation D':A'|-M:a' in F_3.
The specification of the constraints is too technical to be
completely written here.
The proof is given in the paper. Unfortunately it cannot be
generalized to all derivations.
Simona Ronchi Della Rocca