Summary
Our treatment of type inference, based on constraints collected by the inference algorithm, is based on Pierce (cited below).
Terms and concepts
- abstract syntax
- abstract syntax tree
- associativity
- back end
- Backus-Naur Form (BNF)
- big step
- bytecode
- call by name
- call by value
- capture-avoiding substitution
- closure
- compiler
- concrete syntax
- constraint
- context-free grammar
- context-free language
- desugaring
- dynamic environment
- dynamic scope
- environment model
- evaluation
- fresh
- front end
- generalization
- Hindley–Milner (HM) type inference algorithm
- implicit typing
- instantiation
- intermediate representation
- interpreter
- lambda calculus
- let polymorphism
- lexer
- machine configuration
- metavariable
- nonterminal
- operational semantics
- optimizing compiler
- parser
- precedence
- preliminary type variable
- preservation
- primitive operatiohn
- progress
- pushdown automata
- regular expression
- regular language
- relation
- semantic analysis
- short circuit
- small step
- source program
- static scope
- static typing
- stuck
- substitution
- substitution model
- symbol
- symbol table
- target program
- terminal
- token
- type annotation
- type checking
- type inference
- type reconstruction
- type safety
- type scheme
- type system
- type variable
- typing context
- unification
- unifier
- value
- value restriction
- virtual machine
- weak type variable
- well typed
Further reading
- Types and Programming Languages by Benjamin C. Pierce, chapters 1-14, 22.
- Modern Compiler Implementation (in Java or ML) by Andrew W. Appel, chapters 1-5.
- Automata and Computability by Dexter C. Kozen, chapters 1-27.
- Real World OCaml has a chapter on the OCaml frontend.
- This webpage documents how some of the internals of the OCaml type checker and inferencer.
- The OCaml VM aka the Zinc Machine is described in these papers: 1, 2.