Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Glossary - Functional programming and type systems

Principal typings

The process of type inference is the fact of guessing, given an user-written program, what the type of this program is. In general, there may be several correct types for a given program. For example, the program fun x -> x can be given the types int -> int and bool -> bool.

Given a program, a type for this program is principal if it is the most general type that can be given to this program, in the sense that all other psosible types are specialization (instances) of this type. With my fun x -> x example, the polymorphic 'a -> 'a is a principal type.

A type system has the property of principal typing if for every term in the system, there's a principal type that subsumes (is a more general version, or a "supertype") all the other possible typings of the term.

Type systems with principal typing: ML, System F Type systems without principal typing: ML + overloaded operators, ML + polymorphic recursion (it can make the inference of the principal type undecidable) , Haskell's typesystem

Type passing vs Type erasing semantics

What are the differences between ML and System F?

Simpler terms

Typing environment: (Sigma) a relation that associates for every term a type

Lemmas, theorems and properties:

  • Soundness
  • Inversion
  • Subject reduction: informally a type system has the subject reduction property if evaluation doesn't change the types of terms
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment