[Prev][Next][Index][Thread]

Polymorphic Type Inference

The paper "Partial Polymorphic Type Inference and Higher-Order
Unification" (to appear at the upcoming Conference on Lisp and
Functional Programming) may be of interest to typophiles.  If you
would like a copy, please send mail to my secretary, Michelle Jackson
<michelle@h.gp.cs.cmu.edu>, since I will be out of town for extended
periods this summer.  The paper is available as Ergo Report 88-048.

Since it has lead to misunderstandings in the past, I would like to
emphasize, that even though the paper is entitled "Partial Polymorphic
Type Inference and Higher-Order Unification", the problem solved is no
more or less complete than the traditional type inference problem, but
reflects a "Church view" of the polymorphically typed lambda-calculus
rather than a "Curry view".  In the case of implicitly polymorphic
languages (like ML), the same algorithm solves both problems, but this
is no longer the case when one generalizes to the second-order
polymorphic lambda-calculus.

   - Frank Pfenning
------------------------------------------
Frank Pfenning
Department of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3890

Telephone: (412) 268-6343
ArpaNet: fp@cs.cmu.edu
------------------------------------------
   Partial Polymorphic Type Inference and Higher-Order Unification
			    Frank Pfenning
		     Carnegie Mellon University

Abstract

We show that the problem of partial type inference in the nth-order
polymorphic lambda-calculus is equivalent to nth-order unification.
On the one hand, this means that partial type inference in polymorphic
lambda-calculi-of order 2 or higher is undecidable.  On the other
hand, higher-order unification is often tractable in practice, and our
translation entails a very useful algorithm for partial type inference
in the omega-order polymorphic lambda-calculus.  We present an
implementation in Lambda-Prolog in full.

>From the introduction:

In explicitly polymorphic languages, at least two different type
inference problems arise which we call "full" and "partial" type
inference (following Boehm).  These different problems reflect
different views of the underlying lambda-calculus, either as
type-assignments to untyped terms (the "Curry" view) or as filling in
information omitted from typed terms (the "Church" view).  The former
leads to full type inference, the latter to partial type inference.

Full type inference means that arbitrary type abstractions and
applications may be inserted into the untyped term in order to find a
valid typing.  Aspects of full type inference for the second-order
polymorphic lambda-calculus have been examined by Leivant ('83)
McCracken ('84), and Mitchell ('84), but the decidability question is
still open.

Partial polymorphic type inference, on the other hand, does not
attempt to arbitrarily insert type abstractions and applications, but
requires placeholders to be supplied by the user.  Thus "\x.xx" would
not type-check, but "\x.x[]x" would, since there is an explicit
indication that "x" was intended to be a type abstraction.  This is
perhaps a little more verbose than the completely untyped term, but
still much shorter than its fully typed counterpart.  Partial type
inference has been investigated by Mitchell ('84) and Boehm ('85).