數理邏輯是基礎工具，研究PLT必備。類型論是PLT的一個重要方面。范疇論是類型論的抽象工具。編程語言有無類型都是圖靈等價的。類型只是標注，擦除掉也不影響解釋執行。類型標志就像xx編程規范，可以增強可讀性正確性，減少bug。但也不僅于此，類型是對編程語言的抽象，類型表達一類變量或函數的共同行為特征。