对于对类型系统和类型理论感兴趣的人来说，他们第一次接触文献时会看到一些复杂的语法，但实际上相当简单。基本思想来自形式逻辑，整个表达式是一个蕴涵，上半部分是假设，下半部分是结果。了解这些符号后，可以理解如何使用规则来计算表达式的类型。规则包括应用、函数、let语句、子类型和类型泛化。通过递归应用规则，可以得到表达式类型的证明。这些规则精确地说明了如何找出表达式的类型。