Type Reconstruction with First-Class Polymorphic Values

Abstract

We present the first type reconstruction system which combines the implicit typing of ML with the full power of the explicity typed second-order polymorphic lambda calculus. The system will accept ML-style programs, explicity typed programs, and programs that use explicit types for all first-class polymorphic values. We accomplish this flexibility by providing both generic and explicitly-quantified polymorphic types, as well as operators which convert between these two forms of polymorphism. This type reconstruction system is an integral part of the FX-89 programming language. We present a type reconstruction algorithm for the system. The type reconstruction algorithm is proven sound and complete with respect to the formal typing rules.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1989
Accession Number
ADA210833

Entities

People

  • David K. Gifford
  • James W. O'toole

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Automatic
  • Availability
  • Calculus
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Department Of Defense
  • Information Processing
  • Language
  • Massachusetts
  • Military Research
  • Programming Languages
  • Security
  • Side Effects
  • Specifications

Readers

  • Calculus or Mathematical Analysis
  • Computational Linguistics