What is Type Inference?

• Type-checking (checking the types of values in a program before it is run) can reject a program before it runs to prevent type errors from emerging.

  • This is a feature of statically-typed languages (SML is one such language).
  • In statically-typed languages, every binding must be given a type at compile time.
  • In dynamically-typed language (e.g. Python, Racket, Ruby, JS), not much of such checking is done, hence errors usually appear at runtime.

• Implicit typing

  • In implicitly-typed languages, the programmer rarely needs to specify the type of a binding.

  • Instead, the compiler will infer the type of a binding at compile time.

    • The following code snippet depicts such an inference.

      fun f x = (* infer val f: int -> int *)
      	if x > 3
      	then 42
      	else x * 2
      

  • However, if the compiler is unable to infer a type, it will throw an error. (If the compiler can’t infer a type, it’s not its fault — you probably made a mistake somewhere in your code)

    • In the example below, the compiler won’t be able to infer a return type for the function g as it returns a bool in some situations and an int in others

      fun g x = (* report type error *)
      	if x > 3
      	then true
      	else x * 2
      

• What is type inference?

  • The act of taking a program and try to infer a type for every variable, binding, and expression in the program such that the program type-checks and is able to run.
  • If a type cannot be inferred (as with the example of function g earlier), it’s type inference’s job to fail and throw an error.
  • In principle, you could have a type inferencer infer the types of all the bindings in a program before a type checker checks if those types are correct.
    • In SML, the type inferencer and type checker are the same entity.

• There are 3 types of type inference

  • Easy (i.e. accept/reject all types)
  • Difficult
  • Impossible (i.e. the types of bindings in a program cannot be inferred)

• The greater the difficulty of type inference, the stricter the type inferencer is with deciding on types.

ML Type Inference

• In SML, the type inference procedure is as follows:

  1. Determine type of bindings in order

     • This applies in all cases except for mutual recursion (covered later) since mutual recursion works through 2 functions that are defined in terms of each other.
     • If you use bindings before they are defined, they won’t type-check.

  2. For every val or fun binding,

     • Analyse its definition for any elements that could constrain the type of the input(s)/output.
     • For instance, if x > 0 appears in code, x will be constrained to the type int since > only operates on 2 values of type int.
     • Likewise, if x/3.0 appears in code, x will be constrained to the type real since / only operates on 2 values of type real.
     • If the type of the input(s)/output is over-constrained (i.e. if there are constraints that contradict one another and disallow the type of the input(s)/output to be inferred), a type error will be thrown.

  3. For any types that remain unconstrained (i.e. polymorphic), assign type variables (e.g. 'a, 'b).

     • For example, the type of any argument that remained unused in the function body must be unconstrained.
       • There is no way a type inferencer can assign unused arguments any specific type as they were never operated on.

  4. Lastly, enforce the value restriction.