Если что-то простое, то это должно быть полностью объяснимо несколькими словами. Это можно сделать для λ-исчисления:

Λ-исчисление - это синтаксическая грамматика (в основном, структура) с правилом редукции (что означает, что процедура поиска / замены неоднократно применяется к каждому вхождению определенного шаблона, пока такой шаблон не существует).

Грамматика:

Term = (Term Term) | (λ Var . Term) | Var

Правило сокращения:

((λ var body) term) -> SUBS(body,var,term)
    where `SUBS` replaces all occurrences of `var`
    by `term` in `body`, avoiding name capture.

Примеры:

(λ a . a)                             -> (λ a a)
((λ a . (λ b . (b a))) (λ x . x))     -> (λ b . (b (λ x x)))
((λ a . (a a)) (λ x . x))             -> (λ x . x)
((λ a . (λ b . ((b a) a))) (λ x . x)) -> (λ b . ((b (λ x . x)) (λ x . x)))
((λ x . (x x)) (λ x . (x x)))         -> never halts

Хотя это и несколько неформально, можно утверждать, что это достаточно информативно для обычного человека, чтобы понять λ-исчисление в целом - и требуется 22 строки уценки. Я пытаюсь понять системы чистого / зависимого типа, используемые Idris / Agda и подобными проектами, но я могу найти более краткое объяснение: « Просто легко» - отличная статья, но, похоже, она предполагает много предыдущих знаний (Хаскель, индуктивный определения), что у меня нет. Я думаю, что что-то более короткое, менее богатое может устранить некоторые из этих барьеров. Таким образом,

Можно ли дать краткое, полное объяснение систем чистого / зависимого типа в том же формате, который я представил выше для λ-исчисления?

отказ

Это очень неформально, как вы и просили.

Грамматика

В языке с зависимой типизацией у нас есть связующее на уровне типов, а также на уровне значений:

Term = * | (∀ (Var : Term). Term) | (Term Term) | (λ Var. Term) | Var

Хорошо введенный термин - это термин с прикрепленным типом, мы напишем t ∈ σили

σ
t

чтобы указать, что термин tимеет тип σ.

Правила печатания

Для простоты мы требуем, чтобы λ v. t ∈ ∀ (v : σ). τоба λи ∀связывали одну и ту же переменную ( vв данном случае).

Правила:

t ∈ σ is well-formed if σ ∈ * and t is in normal form (0)

*            ∈ *                                                 (1)
∀ (v : σ). τ ∈ *             -: σ ∈ *, τ ∈ *                     (2)
λ v. t       ∈ ∀ (v : σ). τ  -: t ∈ τ                            (3)
f x          ∈ SUBS(τ, v, x) -: f ∈ ∀ (v : σ). τ, x ∈ σ          (4)
v            ∈ σ             -: v was introduced by ∀ (v : σ). τ (5)

Таким образом, *это «тип всех типов» (1), ∀образует типы из типов (2), лямбда-абстракции имеют pi-типы (3) и, если они vпредставлены ∀ (v : σ). τ, то vимеют тип σ(5).

«в нормальной форме» означает, что мы выполняем как можно больше сокращений, используя правило сокращения:

Правило сокращения

(λ v. b ∈ ∀ (v : σ). τ) (t ∈ σ) ~> SUBS(b, v, t) ∈ SUBS(τ, v, t)
    where `SUBS` replaces all occurrences of `v`
    by `t` in `τ` and `b`, avoiding name capture.

Или в двумерном синтаксисе, где

σ
t

означает t ∈ σ:

(∀ (v : σ). τ) σ    SUBS(τ, v, t)
                 ~>
(λ  v     . b) t    SUBS(b, v, t)

Лямбда-абстракцию можно применять только к термину, если термин имеет тот же тип, что и переменная в связанном квантификаторе поиска. Затем мы уменьшаем как лямбда-абстракцию, так и квантификатор Форалла таким же образом, как в чистом лямбда-исчислении ранее. После вычитания части уровня значения мы получаем (4) правило набора текста.

Пример

Вот оператор приложения функции:

∀ (A : *) (B : A -> *) (f : ∀ (y : A). B y) (x : A). B x
λ  A       B            f                    x     . f x

(мы сокращаем , ∀ (x : σ). τчтобы σ -> τесли τне упоминать x)

fвозвращает B yдля любого предоставленного yтипа A. Применим fк x, что правильный тип A, и заменить yна xв ∀AFTER ., таким образом , f x ∈ SUBS(B y, y, x)~> f x ∈ B x.

Давайте теперь сокращаем оператор приложения функции как appи применяем его к себе:

∀ (A : *) (B : A -> *). ?
λ  A       B          . app ? ? (app A B)

Я ставлю ?на условия, которые мы должны предоставить. Сначала мы явно представляем и создаем экземпляр Aи B:

∀ (f : ∀ (y : A). B y) (x : A). B x
app A B

Теперь нам нужно объединить то, что мы имеем

∀ (f : ∀ (y : A). B y) (x : A). B x

который так же, как

(∀ (y : A). B y) -> ∀ (x : A). B x

и что app ? ?получает

∀ (x : A'). B' x

Это приводит к

A' ~ ∀ (y : A). B y
B' ~ λ _. ∀ (x : A). B x -- B' ignores its argument

(см. также Что такое предсказуемость? )

Наше выражение (после некоторого переименования) становится

∀ (A : *) (B : A -> *). ?
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

Так как для любого A, Bи f(где f ∈ ∀ (y : A). B y)

∀ (y : A). B y
app A B f

мы можем создать экземпляр Aи Bполучить (для любого fс соответствующим типом)

∀ (y : ∀ (x : A). B x). ∀ (x : A). B x
app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) f

и сигнатура типа эквивалентна (∀ (x : A). B x) -> ∀ (x : A). B x.

Все выражение

∀ (A : *) (B : A -> *). (∀ (x : A). B x) -> ∀ (x : A). B x
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

Т.е.

∀ (A : *) (B : A -> *) (f : ∀ (x : A). B x) (x : A). B x
λ  A       B            f                    x     .
    app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B) f x

который после всех сокращений на уровне значения возвращает то же самое app.

Таким образом , в то время как он требует всего несколько шагов в чистом лямбда - исчислении , чтобы получить appот app app, в типизированной настройки (и особенно в зависимости напечатал) мы также должны заботиться об объединении и вещи становятся все более сложными , даже с некоторым inconsitent удобства ( * ∈ *).

Проверка типа

• Если tесть *то t ∈ *(1)
• Если tесть ∀ (x : σ) τ, σ ∈? *, τ ∈? *(смотрите примечание о ∈?ниже) , то в t ∈ *силу (2)
• Если tесть f x, f ∈ ∀ (v : σ) τдля некоторых σи τ, x ∈? σто t ∈ SUBS(τ, v, x)(4)
• Если tявляется переменной v, vбыла введена к тому ∀ (v : σ). τвремени t ∈ σ(5)

Все это правила вывода, но мы не можем сделать то же самое для лямбд (вывод типов неразрешим для зависимых типов). Поэтому для лямбд мы проверяем ( t ∈? σ), а не выводим:

• Если tесть λ v. bи проверено ∀ (v : σ) τ, b ∈? τтоt ∈ ∀ (v : σ) τ
• Если tэто что-то еще и проверено, σто определите тип tиспользования функции выше и проверьте, является ли этоσ

Проверка на равенство типов требует, чтобы они были в нормальных формах, поэтому, чтобы решить, tимеет ли тип, σмы сначала проверяем, σимеет ли тип *. Если это так, то σэто нормализуемо (по парадоксу по модулю Жирара), и оно нормализуется (следовательно, σстановится хорошо сформированным (0)). SUBSтакже нормализует выражения для сохранения (0).

Это называется двунаправленной проверкой типов. При этом нам не нужно аннотировать каждую лямбду с типом: если f xтип fизвестен, то xпроверяется на соответствие типу fполучаемого аргумента, а не выводится и сравнивается на равенство (что также менее эффективно). Но если fэто лямбда, это требует явной аннотации типа (аннотации опущены в грамматике, и везде вы можете добавлять Ann Term Termили λ' (σ : Term) (v : Var)к конструкторам).

Кроме того, посмотрите на проще, проще! Сообщение блога.

Пойдем. Я не буду беспокоиться о парадоксе Жирара, потому что он отвлекает от центральных идей. Мне нужно будет представить некоторые механизмы представления о суждениях и выводах и тому подобное.

грамматика

Срок :: = (Элим) | * | (Вар: Срок) → Срок | λVar↦Term

Elim :: = Срок: Срок | Вар | Элим Терм

Грамматика имеет две взаимно определенные формы, «термины», которые являются общим понятием вещи (типы - вещи, значения - вещи), включая * (тип типов), зависимые типы функций и лямбда-абстракции, но также встраивание » Исключения »(т.е.« использует », а не« конструкции »), которые являются вложенными приложениями, в которых в конечном итоге в позиции функции находится либо переменная, либо термин, помеченный ее типом.

Правила сокращения

(λy↦t: (x: S) → T) s ↝ t [s: S / y]: T [s: S / x]

(т: т) ↝ т

Операция подстановки t [e / x] заменяет каждое вхождение переменной x на исключение e, избегая захвата имени. Чтобы сформировать приложение, которое может быть сокращено, лямбда- термин должен быть аннотирован по его типу для исключения . Аннотация типа дает лямбда-абстракции своего рода «реактивность», позволяющую приложению продолжить работу. Как только мы достигнем точки, в которой больше не будет приложений, и активное t: T встраивается обратно в синтаксис термина, мы можем отбросить аннотацию типа.

Давайте расширим отношение сокращения by структурным замыканием: правила применяются везде внутри терминов и исключений, чтобы вы могли найти что-то соответствующее левой части. Напишите ↝ * для рефлексивно-транзитивного (0-или-более-шагового) замыкания ↝. В результате система восстановления в этом смысле сливается:

Если s ↝ * p и s ↝ * q, то существует такой r, что p ↝ * r и q ↝ * r.

Контексты

Контекст :: = | Context, Var: Term

Контексты - это последовательности, которые присваивают переменным типы, растущие справа, которые мы считаем «локальным» концом, говорящим нам о самых последних связанных переменных. Важным свойством контекстов является то, что всегда можно выбрать переменную, еще не использованную в контексте. Мы поддерживаем инвариант, что переменные, приписываемые типам в контексте, различны.

Суждения

Суждение :: = Контекст ⊢ Термин есть Термин | Контекст ⊢ Элим - это термин

Это грамматика суждений, но как их читать? Для начала, ⊢ является традиционным символом «турникета», отделяющим предположения от выводов: вы можете прочитать его неформально, как «говорит».

G ⊢ T имеет т

означает, что в данном контексте G тип T допускает термин t;

G ⊢ e это S

означает, что с учетом контекста G исключение e имеет тип S.

Суждения имеют интересную структуру: ноль или более входов , один или несколько предметов , ноль или более выходов .

INPUTS                   SUBJECT        OUTPUTS
Context |- Term   has    Term
Context |-               Elim      is   Term

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

Правила печатания

Я представляю их в смутном стиле Пролог, написав J -: P1; ...; Pn, чтобы указать, что суждение J выполняется, если также выполняются посылки P1-Pn. Предпосылкой будет другое решение или требование о сокращении.

условия

G ⊢ T имеет t -: T ↝ R; G ⊢ R имеет т

G ⊢ * имеет *

G ⊢ * имеет (x: S) → T -: G ⊢ * имеет S; G, z: S! - * имеет T [z / x]

G ⊢ (x: S) → T имеет λy↦t -: G, z: S ⊢ T [z / x] имеет t [z / y]

G ⊢ T имеет (е) -: G ⊢ е является Т

Исключения

G R e является R -: G ⊢ e является S; S ↝ R

G, x: S, G '⊢ x является S

G ⊢ fs есть T [s: S / x] -: G ⊢ f есть (x: S) → T; G ⊢ S имеет с

Вот и все!

Только два правила не направлены на синтаксис: правило, которое гласит «вы можете уменьшить тип, прежде чем использовать его для проверки термина» и правило, которое гласит «вы можете уменьшить тип после того, как вы синтезировали его из исключения». Одной из жизнеспособных стратегий является сокращение типов до тех пор, пока вы не откроете самый верхний конструктор.

Эта система не сильно нормализуется (из-за Парадокса Жирара, который является парадоксом самообращения в стиле лжеца), но ее можно сильно нормализовать, разбивая * на «уровни вселенной», где любые значения, которые включают типы на более низких уровнях сами иметь типы на более высоких уровнях, предотвращая самоотдачу.

Эта система, однако, обладает свойством сохранения типа, в этом смысле.

Если G ⊢ T имеет t и G ↝ * D и T ↝ * R и t ↝ r, то D ⊢ R имеет r.

Если G ⊢ e является S и G ↝ * D и e ↝ f, то существует R такое, что S ↝ * R и D ⊢ f есть R.

Контексты могут вычисляться, позволяя вычислять содержащиеся в них термины. То есть, если суждение является действительным сейчас, вы можете вычислить его входные данные столько, сколько хотите, и его предмет за один шаг, и тогда можно будет каким-то образом вычислить его выходные данные, чтобы убедиться, что полученное суждение остается действительным. Доказательство является простой индукцией при выводе производных, учитывая слияние -> *.

Конечно, я представил здесь только функциональное ядро, но расширения могут быть весьма модульными. Вот пары.

Срок :: = ... | (x: S) * T | S, T

Элим :: = ... | e.head | e.tail

(s, t: (x: S) * T) .head ↝ s: S

(s, t: (x: S) * T) .tail ↝ t: T [s: S / x]

G ⊢ * имеет (x: S) * T -: G ⊢ * имеет S; G, z: S has * имеет T [z / x]

G ⊢ (x: S) * T имеет s, t -: G ⊢ S имеет s; G ⊢ T [s: S / x] имеет t

G head e.head является S -: G ⊢ e является (x: S) * T

G ⊢ e.tail является T [e.head / x] -: G ⊢ e является (x: S) * T

Корреспонденция Карри-Говард говорит , что существует систематическая соответствие между системами типов и системами доказательств в логике. С точки зрения программиста, вы можете изменить это следующим образом:

• Системы логической защиты являются языками программирования.
• Эти языки статически типизированы.
• Обязанность системы типов в таком языке - запрещать программы, которые создают несостоятельные доказательства.

Видно с этой точки зрения:

• Нетипизированное лямбда-исчисление, которое вы суммируете, не имеет существенной системы типов, поэтому построенная на ней система доказательств была бы несостоятельной.
• Простое типизированное лямбда-исчисление - это язык программирования, который имеет все типы, необходимые для построения звуковых доказательств в предложенной логике («если / то», «и», «или», «не»). Но его типы недостаточно хороши для проверки доказательств, которые включают квантификаторы («для всех x, ...»; «существует такой x, что ...»).
• Лямбда-исчисление с независимой типизацией имеет типы и правила, которые поддерживают логические предложения и квантификаторы первого порядка (количественное определение по значениям).

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

Обратите внимание, что в правилах есть лямбда-термины. Они могут быть прочитаны как программы, которые создают доказательства предложений, представленных их типами (или, более кратко, мы просто говорим, что программы являются доказательствами ). Аналогичные правила сокращения, которые вы даете, могут применяться к этим лямбда-терминам.

Почему мы заботимся об этом? Ну, во-первых, потому что доказательства вполне могут оказаться полезным инструментом в программировании, и наличие языка, который может работать с доказательствами как первоклассными объектами, открывает много возможностей. Например, если у вашей функции есть предварительное условие, вместо того, чтобы записать это как комментарий, вы можете потребовать доказательства этого в качестве аргумента.

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

Чтобы дать очень простое применение этого, я все время пишу код, который должен читать файлы Avro, которые состоят из записей с одинаковой структурой - все имеют одинаковый набор имен и типов полей. Это требует от меня либо:

1. Жесткий код структуры записей в программе как тип записи.
   • Преимущества: код проще, и компилятор может отлавливать ошибки в моем коде
   • Недостаток: программа жестко запрограммирована для чтения файлов, соответствующих типу записи.
2. Чтение схемы данных во время выполнения, общее представление ее в виде структуры данных и использование ее для общей обработки записей
   • Преимущества: моя программа не жестко запрограммирована только на один тип файла
   • Недостатки: компилятор не может поймать столько ошибок.

Как вы можете видеть на странице учебника Avro Java , они показывают вам, как использовать библиотеку в соответствии с обоими этими подходами.

С зависимыми типами функций вы можете получить свой торт и съесть его за счет более сложной системы типов. Вы можете написать функцию, которая читает файл Avro, извлекает схему и возвращает содержимое файла в виде потока записей , статический тип которых зависит от схемы, хранящейся в файле . Компилятор мог бы перехватывать ошибки, когда я, например, пытался получить доступ к именованному полю, которое может отсутствовать в записях файлов, которые он будет обрабатывать во время выполнения. Сладкий, а?