Фазовое различие

Фазовое различие — это свойство языков программирования, которые соблюдают строгое разделение между типами и терминами . Краткое правило для определения того, сохраняется ли фазовое различие в языке или нет, было предложено Лукой Карделли : если A является термином времени компиляции, а B является подтермом A, то B также должен быть термином времени компиляции. ^[1]

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

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

Теория

Фазовое различие используется в сочетании со статической проверкой. ^[2] Используя систему, основанную на исчислении, различение фаз устраняет необходимость применения линейной логики между различными типами и терминами программирования. ^[3]

Введение

Phase Distinction различает обработку, выполняемую во время компиляции, и обработку, выполняемую во время выполнения.

Рассмотрим простой язык, ^[3] с условиями:

   t ::= true | false | x | λx : T . t | t t | if t then t else t

и типы:

   T ::= Bool | T -> T

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

Ссылки

^ Карделли, Лука (3 января 1988 г.). «Различия фаз в теории типов» (PDF) . Корпорация цифрового оборудования .
^ Карделли, Лука (3 января 1988 г.). «Различия фаз в теории типов» (PDF) . Корпорация цифрового оборудования .
^ Jump up to: ^а ^б «CMSC 336: Системы типов для языков программирования; Лекция 7: Изоморфизм Карри-Ховарда и производные формы» (PDF) . 31 января 2008 г.

[1] Карделли, Лука (3 января 1988 г.). «Различия фаз в теории типов» (PDF) . Корпорация цифрового оборудования .

[2] Карделли, Лука (3 января 1988 г.). «Различия фаз в теории типов» (PDF) . Корпорация цифрового оборудования .

[uchic-3] Jump up to: ^а ^б «CMSC 336: Системы типов для языков программирования; Лекция 7: Изоморфизм Карри-Ховарда и производные формы» (PDF) . 31 января 2008 г.

[1]

[2]

[3]