PureScript類型系統名稱

Question

PureScript中使用的類型系統的正確學術名稱是什麼？我正在尋找有關這方面的文件，並證明它是正確的。

特別是，當類型系統允許將異常解決爲隱藏通信通道問題時，當想要拋出一個私有異常類型的實例，並將其通過有效的計算傳遞給catch處理程序而不需要將該類型暴露給計算和在那裏捕捉它的可能性，這將很高興確認這是正確的。

Answer 1

PureScript類型檢查器並不特別基於任何一種類型的系統。我把靈感來自於數篇論文，我實現了它，包括：

• 「完整而簡單的雙向類型檢查 爲較高等級多態性」約書亞Dunfield和Neelakantan R.瓦米
• 「HMF：簡單類型推斷一流的多態性」的 大安Leijen
• ‘科卡：具有行多態性影響類型的節目’，由大安Leijen

有沒有合理性的證明。在某些時候，我會有興趣回到並重新實現類型檢查器，它基於一些有保證的系統，但最初的目標是生成一個具有我想要的特性的實用類型系統：行多態，類型類和等級N類型。