A Tutorial on Polymorphic Type Derivations

This is a tutorial on how to produce typing derivation trees for a simplified version of ML’s type system. Rather than being incredibly precise about every detail, this tutorial will focus on building up an understanding of why the rules work as they do. This tutorial is based on the presentation of polymorphic typ-ing in Programming Language Concepts [Sestoft, 2012]. For your convenience, the grammar and type system of the small version of ML used in this tutorial are reproduced in Appendix A. Notational Conventions When looking at a formal definition of a type sys-tem, it can be difficult at first to distinguish the different categories of sym-bols from each other. Rather than sweep this issue under the rug, colors an