MLF for everyone (users, implementers, and designers)

ABSTRACT

ML^F is an alternative to ML that permits second-order polymorphism as in System F but retains (partial) type inference a la ML. Type annotations are requested only on parameters of functions that are used polymorphically. Type abstractions and type applications are entirely alleviated. Inpractice, very few type annotations are actually needed. Moreover, small program transformations such as commutation of arguments, η-expansion, etc. never require extra type annotations. ML^F is a conservative extension of ML that allows to type all of System-F terms-and a few more.

Types of ML^F extend those of System-F with instance-bounded polymorphism so that more expressions have principal types and also abstraction-bounded polymorphism so that first-class types may always be treated abstractly during type inference. However, types may be more concisely described as the superposition of a standard term-dag representation of first-order types and a binding tree, with well-formedness conditions relating the two. This allows for a simple definition of type instance and leads to an efficient unification algorithm on types.

This graphical presentation of types may also be extended to represent type schemes and unification and instantiation constraints as additional edges. Typing rules, type inference, and type soundness can then all be described using type constraints. Type inference for ML^F is performed much as for ML and is about as efficient.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

General Terms:
Algorithms, Design, Languages, Theory

Keywords:
ML, ML^F, System F, binders, graphs, type constraints, type inference, types, unification