История изменений
Исправление quasimoto, (текущая версия) :
Почему это неинтересно?
Потому что TI это техническое средство которое работает только в самоочевидных случаях, чем больше типы становятся действительно утверждениями, тем меньше смысла в TI, просто потому что по виду программ (доказательств) нельзя угадать какие именно типы они имеют (какие утверждения доказывают). Это проявляется даже в хаскеле при type/data driven разработке, когда инварианты энфорсятся сверху как GADTs типы или классы с зависимостями. Например, полагаться на вывод типов при работе с перегруженными массивами или регулярными выражениями нельзя, GHC что-то вывести там просто не может (by design). И тут просто ─ по абстрактному контексту нельзя выбрать конкретную реализацию массивов или результат сопоставления с данным образцом (который просто строка, а результат может быть сложным кортежем). В случае зависимых типов ─ сложнее и тем более меньше толка от TI.
А НМ это что?
Wells' result implies that type inference for System F is impossible. A restriction of System F known as «Hindley–Milner», or simply «HM», does have an easy type inference algorithm and is used for many strongly typed functional programming languages such as Haskell 98 and ML.
(c) http://en.wikipedia.org/wiki/System_F.
HM это, с одной стороны, название определённого разрешимого алгоритма вывода типов, и, с другой, название _подмножества_ System F для которого этот алгоритм существует. Для полной System F вывод типов невозможен (неразрешим). То есть, HM как язык это, фактически, как раз тот кусок System F для которой возможен вывод типов (как одноимённый алгоритм).
Ну грамматика полностью совпадает, значит общий же?
Выписываю грамматику ещё раз.
ULC (противоречивая теория первого порядка):
Term variables i, j, ...
Terms t, u, ... ∷= i | λ i . t | t u
STLC (строго-нормализованная теория первого порядка):
Term variables i, j, ...
Type variables α, β, ...
Types A, B, ... ∷= α | A → B
Terms t, u, ... ∷= i | λ i : A . t | t u
System F (строго-нормализованная теория второго порядка):
Term variables i, j, ...
Type variables α, β, ...
Types A, B, ... ∷= α | A → B | ∀ α . A
Terms t, u, ... ∷= i | λ i : A . t | t u | Λ α . t | t A
Синтаксисы разные, теории разные, модели разные (с отсылкой к Дане Скотту), интернализации разные (CCC over domain / CCC / CCC+pullbacks). В ULC есть нетерминируемые программы, парадоксы (вроде Kleene-Rosser) и она противоречива, тогда как STLC и System F строго-нормализированы. STLC и System F при этом отличаются порядком. Как, например в ULC/STLC написать (Λ typeVar . typeDependentTerm[typeVar])? То есть second-order квантификацию из System F, при том, что ULC/STLC это first-order теории.
Стираются.
Смотря что понимать под стиранием. Компиляцию с устранением type level? Так я не про то. Вот в STLC типы реально стираются, то есть есть тотальное соответствие STLC → ULC (просто как (λ var : SomeType . someTerm[var]) → (λ var . someTerm[var])), потому что это теории одного (первого) порядка и ULC, кхм, «шире», а как ты собрался стирать вычисления с использованием абстракции по типам Λ и аппликацией термов зависимых от типов к типам? Во что превращать терм (Λ typeVar . typeDependentTerm[typeVar])? То есть как построить тотальное соответствие SystemF → STLC для теорий разных порядков (и при том, что тут SystemF шире)?
Ну напиши Y-комбинатор и попробуй типизировать этот терм в STLC
Как я его напишу, если я говорю «не пишется ни в одной из этих [лямбда куба] систем (STLC, System F, ...)»? Его типом в STLC _должно_ быть семейство (α → α) → α для каждого монотипа α теории, а в System F ─ полиморфный тип ∀ a . (a →a) → a. Это я имею ввиду, говоря «типизируется», то есть, нужный тип можно написать (в отличии от бесконечного типа комбинатора само-применения (тут ни тип, ни терм не написать)). Но соответствующий терм чисто физически не написать ─ ни в STLC, ни в System F.
В SystemF пишется. И типизируется.
Если ты сможешь написать fix в SystemF, то сможешь написать нетерминируемый терм (fix id). Fail.
В SystemF пишется.
В STLC пишется.
Напишешь?
fix ≡ λ f : [подставить нужное] . [подставить нужное]
Исходная версия quasimoto, :
Почему это неинтересно?
Потому что TI это техническое средство которое работает только в самоочевидных случаях, чем больше типы становятся действительно утверждениями, тем меньше смысла в TI, просто потому что по виду программ (доказательств) нельзя угадать какие именно типы они имеют (какие утверждения доказывают). Это проявляется даже в хаскеле при type/data driven разработке, когда инварианты энфорсятся сверху как GADTs типы или классы с зависимостями. Например, полагаться на вывод типов при работе с перегруженными массивами или регулярными выражениями нельзя, GHC что-то вывести там просто не может (by design). И тут просто ─ по абстрактному контексту нельзя выбрать конкретную реализацию массивов или библиотеку регулярных выражений. В случае зависимых типов ─ сложнее и тем более меньше толка от TI.
А НМ это что?
Wells' result implies that type inference for System F is impossible. A restriction of System F known as «Hindley–Milner», or simply «HM», does have an easy type inference algorithm and is used for many strongly typed functional programming languages such as Haskell 98 and ML.
(c) http://en.wikipedia.org/wiki/System_F.
HM это, с одной стороны, название определённого разрешимого алгоритма вывода типов, и, с другой, название _подмножества_ System F для которого этот алгоритм существует. Для полной System F вывод типов невозможен (неразрешим). То есть, HM как язык это, фактически, как раз тот кусок System F для которой возможен вывод типов (как одноимённый алгоритм).
Ну грамматика полностью совпадает, значит общий же?
Выписываю грамматику ещё раз.
ULC (противоречивая теория первого порядка):
Term variables i, j, ...
Terms t, u, ... ∷= i | λ i . t | t u
STLC (строго-нормализованная теория первого порядка):
Term variables i, j, ...
Type variables α, β, ...
Types A, B, ... ∷= α | A → B
Terms t, u, ... ∷= i | λ i : A . t | t u
System F (строго-нормализованная теория второго порядка):
Term variables i, j, ...
Type variables α, β, ...
Types A, B, ... ∷= α | A → B | ∀ α . A
Terms t, u, ... ∷= i | λ i : A . t | t u | Λ α . t | t A
Синтаксисы разные, теории разные, модели разные (с отсылкой к Дане Скотту), интернализации разные (CCC over domain / CCC / CCC+pullbacks). В ULC есть нетерминируемые программы, парадоксы (вроде Kleene-Rosser) и она противоречива, тогда как STLC и System F строго-нормализированы. STLC и System F при этом отличаются порядком. Как, например в ULC/STLC написать (Λ typeVar . typeDependentTerm[typeVar])? То есть second-order квантификацию из System F, при том, что ULC/STLC это first-order теории.
Стираются.
Смотря что понимать под стиранием. Компиляцию с устранением type level? Так я не про то. Вот в STLC типы реально стираются, то есть есть тотальное соответствие STLC → ULC (просто как (λ var : SomeType . someTerm[var]) → (λ var . someTerm[var])), потому что это теории одного (первого) порядка и ULC, кхм, «шире», а как ты собрался стирать вычисления с использованием абстракции по типам Λ и аппликацией термов зависимых от типов к типам? Во что превращать терм (Λ typeVar . typeDependentTerm[typeVar])? То есть как построить тотальное соответствие SystemF → STLC для теорий разных порядков (и при том, что тут SystemF шире)?
Ну напиши Y-комбинатор и попробуй типизировать этот терм в STLC
Как я его напишу, если я говорю «не пишется ни в одной из этих [лямбда куба] систем (STLC, System F, ...)»? Его типом в STLC _должно_ быть семейство (α → α) → α для каждого монотипа α теории, а в System F ─ полиморфный тип ∀ a . (a →a) → a. Это я имею ввиду, говоря «типизируется», то есть, нужный тип можно написать (в отличии от бесконечного типа комбинатора само-применения (тут ни тип, ни терм не написать)). Но соответствующий терм чисто физически не написать ─ ни в STLC, ни в System F.
В SystemF пишется. И типизируется.
Если ты сможешь написать fix в SystemF, то сможешь написать нетерминируемый терм (fix id). Fail.
В SystemF пишется.
В STLC пишется.
Напишешь?
fix ≡ λ f : [подставить нужное] . [подставить нужное]