Проверка типа "let" -привязки / определения функций эффективно в Системе F - PullRequest
Новая
       5

Проверка типа "let" -привязки / определения функций эффективно в Системе F

2 голосов
/ 03 апреля 2011

Рассмотрим следующий (псевдо-) код OCaml: 

let foo = <something> in
  begin
    foo a
    foo b
    foo c
    ...
    foo z
  end

(az - метавариабельные, ничего конкретного)

Я читаю [Pierce, TAPL, Ch.22.7], что в полиморфизме в стиле ML, проверка типа может быть выполнена эффективно путем вычисления основного типа для «foo», обобщения (таким образом вводя полиморфизм в стиле ML) и проверки на этот тип для каждого вхождения «foo» в теле (здесь будет 26 раз).

Теперь мой вопрос: что если мы находимся в Системе F?Что если вы не можете проверить тип функции с помощью алгоритма типизации ограничений?Конечно, правила для системы F существуют, но их реализация означает, что вам придется заменять каждый вхождения «foo» на «» и повторять проверку «» каждый раз, когда вы вызываете «foo».

1 Ответ

2 голосов
/ 05 апреля 2011

Система F обычно описывается в явно типизированном стиле: функции помечены типом их аргумента (λ(x:σ).t) и типом абстракции (Λα.t) и приложения (t[σ]) присутствуют в синтаксис.

В этой презентации легко вычислить тип термина в твой пример <something>. Этот тип уникален и, в частности, он является «наиболее общим типом»: путаница невозможна. foo будет иметь этот тип. Если это тип стрелки σ → τ, затем все параметры задаются foo (a, b ...) будет иметь тип σ. Если это полиморфный тип Λα₁Λα₂...σ→τ, затем перед использованием его в качестве функции необходимо инстанцировать значения переменных α₁, α₂ и т. д ... Вы не можете написать foo a, но вместо этого следует написать foo[τ₁][τ₂][..] a.

Это может обеспечить вам такое же количество полиморфизма, что и в ML: в ML, абстракции добавляются прозрачно (обобщение привязки) и устранены (экземпляры на сайтах использования). В явном виде Система F, вы делаете это вручную.

Например: 

let id = Λα.λ(x:α).x in
(id [int] 1, id [string] "foo", id [∀α. α → α] id)

Существуют и другие презентации Системы F с различной степенью неявность, где проблема вывода восстановления явного типы не всегда разрешимы. Вы можете увидеть ML как конкретный вывод процесс для неявной системы F, которая не является полной в том смысле, что он не примет все условия, которые можно было бы ввести в Системе F. Для попыток сделать вывод для полной Системы F, см. this Резюме (со времени написания (2004), работа над MLF Реми прогресс, и привел к работе HML / HMF Leijen, а FPH Vytionitis et al.).

...