Является ли система типов Haskell стилем Карри или стилем Чёрча?
Является ли система типов Haskell стилем Карри или стилем Чёрча?
Исследуя систему типов Haskell, я наткнулся на термины «стиль Карри» и «стиль Чёрча». Я хотел бы понять разницу между ними.
- Стиль Карри — это система, в которой информация о типе является внешней по отношению к программе, и проверка типа не является обязательной для выполнения программы. Компилятор автоматически выводит типы без необходимости явных аннотаций типов.
- Церковный стиль — это система, в которой типы интегрированы в семантику языка. Аннотации типов являются обязательными, также выполняется вывод типа. Учитывая, что система типов Haskell включает вывод типов и аннотации типов не являются обязательными, я изначально думал, что ее можно отнести к стилю Карри. Однако в некоторой литературе предполагается, что он также имеет характеристики церковного стиля.
Следует ли считать систему типов Haskell стилем Карри или стилем Чёрча? Кроме того, не могли бы вы объяснить причины вашего мнения?
Ответы 2
Система типов Haskell выполнена в стиле Haskell. Оказывается, возможностей больше двух!
Вообще говоря, я склонен взаимодействовать с ней, как если бы это была система в стиле карри. Но есть несколько заметных отличий:
- Во многих случаях можно вывести всю необходимую информацию о типе программы. Но существует множество ситуаций, когда аннотации типов необходимы для управления механизмом вывода; примеры включают полиморфную рекурсию, неоднозначное использование классов типов, типы более высокого ранга, махинации с семействами типов и GADT.
- Проверка типов обязательна для выполнения программы в большинстве ситуаций. Часть оценки программы включает в себя выбор экземпляров класса типов, что невозможно сделать без проверки типов.
- Существует много причин прикреплять объявления типов к определениям верхнего уровня, поэтому почти все делают это, даже для типов, выведенный тип которых совпадает с объявленным типом.
+1. Если это различие в системах типов типа Черча и Карри в первую очередь связано с тем, являются ли типы явно обязательными, я не думаю, что это очень полезная ось для классификации Haskell. В случае классов типов выбранный тип даже влияет на то, что на самом деле делает программа! Вы можете создать две программы, которые успешно компилируются и выполняются, различаются только типами и выполняют разные действия. Записывать типы очень часто необязательно (по крайней мере, в «ванильном» Haskell), поэтому они могут быть совершенно невидимыми, но концепция типов прочно является частью семантики языка, IMO.
Спасибо за ваш ответ и объяснение. Я ценю ваше понимание. Мне стало ясно, что Haskell обладает элементами обеих систем типов, что приводит к его уникальному стилю. Ваш ответ был очень информативным. Спасибо.
Первоначальный смысл типизации в стиле Чёрча, примененный к лямбда-исчислению, действительно включал в себя явные аннотации типов на связующих. Но в настоящее время «черч-стиль» в первую очередь относится к внутренней типизации, и это то, что есть в Haskell. Каждый термин и переменная имеют единственный внутренний тип, а неправильно типизированный код не имеет определенного значения как программа.
Добавление вывода типа не обязательно меняет систему типов, оно просто реконструирует для вас некоторые аннотации типов.
Аналогично, типизация в стиле Карри теперь традиционно означает внешнюю типизацию, при которой программа имеет значение, не зависящее от проверки типов. У данного термина может быть несколько допустимых типов, ни один из которых не является наиболее общим, и выбор типа не меняет семантику. Вот почему в исходном контексте лямбда-исчисления не требовались аннотации типов.
Отчет Haskell определяет язык, допускающий внутренние типы. Здесь не только говорится, когда «происходит статическая ошибка», но и семантика некоторых функций языка, таких как сопоставление с образцом и классы типов, определяется в терминах внутренних типов.
Ошибки отложенного типа GHC (-fdefer-type-errors) могут показаться позволяющими запустить частично определенную программу. Но если в выражении есть ошибка типа, оно все равно не вернет значения, поэтому это не меняет природу типов — оно просто заменяет некоторые нетипизируемые части кода правильно типизированными терминами, такими как throw (TypeError "…"), чтобы сделать хорошо -типизированная программа.
Благодарю за ваш ответ. Я понимаю, что Haskell в первую очередь считается стилем Чёрча из-за его внутренней типизации, что соответствует моему пониманию. Хотя последние достижения в теории типов могут сделать простые классификации менее подходящими, я считаю, что это различие остается важным для концептуальной ясности. Ваш ответ был очень полезен. Спасибо.
Я думаю, что эти термины в основном используются для описания различных подходов к изучению языка с теоретической точки зрения. Приведем пример: если вы говорите о свойствах языка программирования в помощнике по проверке доказательств (например, Coq или Agda), вы можете настроить его так, чтобы каждый термин, о котором вы можете говорить, был правильно напечатан. Это своего рода «внутренняя типизация». Но вы также можете настроить его так, чтобы были разрешены неправильно напечатанные термины, а позже вы ограничивали их только правильно напечатанными терминами. Это своего рода «внешняя типизация». Но учтите, что язык, который мы изучаем, не изменился.