[TYPES] System F type inference: summary of responses

[Michael Hicks]

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).