Системное имя типа PureScript

Question

Какое уместное академическое имя для системы типов, используемой в PureScript? Я ищу документы об этом и доказательства того, что это звучит.

В частности, поскольку система типов позволяет разрешить исключение как проблему скрытого канала связи, когда вы хотите бросить экземпляр частного типа исключения и передать его через эффективные вычисления обработчику catch без необходимости раскрывать тип вычисление и возможность поймать его там, было бы неплохо подтвердить, что это звучит.

Answer 1

Проверка PureScript не основана на какой-либо одной системе типов в частности. Я черпал вдохновение из нескольких работ, как я реализовал его, в том числе:

• «Полные и Easy двунаправленной проверка типов для более высокого ранга полиморфизма» Джошуа Dunfield и Нилакантан Р. Кришнасва
• «HMF: Простой типа Inference для первый класс Полиморфизм»от Даан Leijen
• "Koka: Программирование с Им-полиморфными типами эффектов" от Daan Leijen

Там нет доказательств нормативов безопасных. В какой-то момент мне было бы интересно вернуться и переопределить проверку типов на основе некоторой системы с гарантией надежности, но первоначальная цель состояла в том, чтобы создать практическую систему типов с теми функциями, которые я хотел: полиморфизм строк, типы классов и ранг N типы.