[TYPES] System F type inference: summary of responses
Michael Hicks
mwh at cs.umd.edu
Tue Jul 27 17:46:25 EDT 2004
Here is a summary of the results I received to my query (quoted below).
The bottom line seems to be that there isn't a well-known intuition as
to how, or whether, a System F type inference problem can be encoded as
a semi-unification problem.
Thanks to all who sent me a response.
Mike
> I'm trying to better understand the difficulty with System F type
> inference. I realize that in general Wells has shown System F
> typability is undecidable due to the undecidability of
> semi-unification. However, I have yet to arrive at an intuition as to
> the sort of programs that are problematic. Wells' reduction is from
> semi-unification to System F, but I'd like to better understand the
> reverse: how would a System F inference problem translate to an
> undecidable semi-unification problem? Henglein presented a
> semi-unification algorithm that seems to work in "natural" cases of
> type inference for ML with polymorphic recursion, so I'm wondering
> when (or whether) this algorithm would be sufficient for System F
> terms.
* Deepak Kapur (kapur at cs.unm.edu) wrote:
I will be very interested in knowing this. When you do literature
search on semi-unification, you will notice that we were the first-ones
to develop a polynomial time semi-unification algorithm for a single
inequality. For many years, I have been interested in finding class of
interesting type inference problems for which undecidability result has
implications.
* François Pottier (Francois.Pottier at inria.fr) wrote:
You might want to have a look at the following two papers by Christophe
Raffalli:
Type checking in system ${F}^\eta$,
ftp://www.lama.univ-savoie.fr/pub/users/RAFFALLI/Papers/Feta-partial.ps
An optimized complete semi-algorithm for system ${F}^\eta$
ftp://www.lama.univ-savoie.fr/pub/users/RAFFALLI/Papers/Feta-total.ps
* David Walker (dpw at cs.princeton.edu) wrote:
Didier Remy (and Didier Le Botlan) recently had a paper about system F
type inference at ICFP 03. Also, do you need complete inference?
Bi-directional type inference is quite elegant and scales to many
complex type systems.
(I read this paper closely and it does provide a very nice intuition
that a difficulty of System F type inference lies in the lack of
principal types. The interesting result of the paper is that
Hindley-Milner-style inference can be used for System F as long as
lambda-bound variables that require System F types (i.e. polytypes) are
annotated with them whenever these variables will be instantiated in
the body of the function. This provides the inference algorithm with
the necessary 'structure' of the type to automatically construct the
instantiations. This is my understanding anyway.)
* Didier Le Botlan (didier.lb at melix.net) wrote:
You might be interested in << On the undecidability of Partial Type
Reconstruction >> (Frank Pfenning, JFI 1993)
A very interesting example is in Boehm's << Partial Polymorphic Type
Inference in Undecidable >> (FOCS 1985).
He gives a term which can only be typed with a type of the form i ->
... -> i where the number of arrows is any multiple of a given number
k. You can then build a more complex term which encodes any
diophantian equation...and solving such equations is known to be
undecidable (tenth Hilbert's problem).
Looking at this example may help you understand what is difficult in
type inference.
* Christian Maeder (maeder at tzi.de) wrote:
"Practical type inference for arbitrary-rank types"
http://research.microsoft.com/Users/simonpj/papers/putting/index.htm
They mention at least Kfoury and Wells's work 94 in the introduction.
* Fritz Henglein (henglein at diku.dk) wrote:
I guess you are asking for a lambda-expression or program (System F
inference problem instance) that translates via Well's reduction to a
semi-unification instance where Algorithm A from my thesis or Hans
Leiss's algorithm, which is at the heart of an SML/NJ variant that
implements an extension of Standard ML with polymorphic recursion (see
Hans Leiss's home page at U. Muenchen) doesn't terminate. I'd be
interested in seeing such an example, too. It is bound to exist, but I
don't know if anybody has actually constructed such examples. For
System F a maybe more basic problem (vis a vis semi-unification) is
that the reduction is only one direction: from System F typability to
semi-unificability, whereas for polymorphic recursion there are
log-space reductions in both directions. This means that
semi-unification can be used to perform type inference for polymorphic
recursion, but not (to my knowledge) for System F.
I still have no solid intuition of why Algorithm A for semi-unification
doesn't terminate (nor, for that matter, why it should terminate). As
for System F, the lack of a principal typing property is, from a
programming perspective (*), rather serious: it disables modular
reasoning (typing) and, beyond that, makes System F type inference so
'interesting' that it is a gem for theoreticians and a nightmare for
language designers, systems builders and, not least, programmers. More
plainly: if somebody builds a component/library, how do you specify its
interface (typing description) in a 'complete' fashion? (The essence
of principal typing being that if there is a type T for a component f
such that for _all_ C[], if C[f] is typable then C[x:T] is also
typable.) This suggests that one should find a 'minimal extension'
(whatever that means) of simple typing that has a principal type or
principal typing (**) property and offers some form of higher-rank
polymorphism. ML is one such extension, ML plus polyrec is, and Rank-2
System F. But is there a way of pushing this to higher ranks (where it
is 'allowed' to add type functions, constraints, etc., whatever seems
defensible).
(*) Makes sense from a logical perspective, but that is dual to the
programming perspective. In logic the types have preeminence and the
terms are subsidiary to them as encodings of proofs, whereas in
programming it is the terms that are there "first" and the types
function as properties/interface descriptions.
(**) Damas had a rank 2 principal typing property in his 1984 thesis,
which was rediscovered and developed independently by Jim (POPL 96).
More information about the Types-list
mailing list