数理逻辑是基础工具，研究PLT必备。类型论是PLT的一个重要方面。范畴论是类型论的抽象工具。编程语言有无类型都是图灵等价的。类型只是标注，擦除掉也不影响解释执行。类型标志就像xx编程规范，可以增强可读性正确性，减少bug。但也不仅于此，类型是对编程语言的抽象，类型表达一类变量或函数的共同行为特征。