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

paper available: Finite-Rank Polymorphic Lambda Calculus


[This message being sent to the "types" and "sml-list" mailing lists.]

This note is the announcement of the availability of a paper entitled:

  A Direct Algorithm for Type Inference in the
  Rank 2 Fragment of the Second-Order Lambda-Calculus

by myself and A. J. Kfoury.  Here is the abstract:

  We study the problem of type inference for a family of polymorphic type
  disciplines containing the power of Core-ML.  This family comprises all
  levels of the stratification of the second-order lambda-calculus by
  ``rank'' of types.  We show that typability is an undecidable problem at
  every rank k >= 3 of this stratification.  While it was already known
  that typability is decidable at rank <= 2, no direct and
  easy-to-implement algorithm was available.  To design such an algorithm,
  we develop a new notion of reduction and show how to use it to reduce
  the problem of typability at rank 2 to the problem of acyclic
  semi-unification.  A by-product of our analysis is the publication of a
  simple solution procedure for acyclic semi-unification.

This is a report prepared for conference submission, so it leaves out the
fine details of justifying why the algorithm is correct.

It is Boston Univ. Comp. Sci. Dept. Tech. Rep. 93-011 and it is available
via anonymous FTP from the host CS.BU.EDU in the directory "techreports"
as the file "93-017-finite-rank.ps.gz" (67K).

-- 
Enjoy,

Joe Wells <jbw@cs.bu.edu>
Member of the League for Programming Freedom --- send e-mail for details