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