Inference Videos for CS 3520/6520

• Inference 1 — introduction (1:10)

  Introduction to type inference.

• Inference 2 — type inference (2:52)

  Basic type inference in action.

• Inference 3 — function calls (2:05)

  Type inference for function calls.

• Inference 4 — occurs check (1:43)

  Type inference needs to avoid creating cyclic type equivalences, which could otherwise happen for expressions that have no type.

• Inference 5 — unify and resolve (2:22)

  The unify function will replace any use of == in the type checker, and it needs a resolve helper function.

• Inference 6 — representing type variables (1:21)

  Representing type variables in our new, inferencing type checker.

• Inference 7 — unify examples (4:34)

  Examples for the unify function.

• Inference 8 — unification (4:02)

  Unification is the algorithm for assigning types to type variables. The unify function will need to implement this algorithm.

• Inference 9 — unify (4:25)

  Implementing unify.

• Inference 10 — typecheck (1:50)

  Updating typecheck to use unify. See infer-lambda.rkt.

• Inference 11 — reporting errors (1:14)

  Type errors with unification can’t point to one wrong expression, but they can report a mismatch and one or more relevant expressions.