Фазовое различие
Фазовое различие — это свойство языков программирования, которые соблюдают строгое разделение между типами и терминами . Краткое правило для определения того, сохраняется ли фазовое различие в языке или нет, было предложено Лукой Карделли : если 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 г.