Фазовое различие
Различение фаз — это свойство языков программирования, которые соблюдают строгое разделение между типами и терминами . Краткое правило для определения того, сохраняется ли различие фаз в языке или нет, было предложено Лукой Карделли : если A — это термин времени компиляции, а B — подтерм A, то B также должен быть термином времени компиляции. [1]
Большинство статически типизированных языков соответствуют принципу фазового различения. Однако некоторые языки с особенно гибкими и выразительными системами типов (в частности, языки программирования с зависимой типизацией ) позволяют манипулировать типами так же, как и обычными терминами. Они могут передаваться функциям или возвращаться в качестве результатов.
Язык с фазовым различием может иметь отдельные пространства имен для типов и переменных времени выполнения. В оптимизирующем компиляторе фазовое различие отмечает границу между выражениями, которые можно безопасно стереть .
Теория
Фазовое различие используется совместно со статической проверкой. [2] Используя систему, основанную на исчислении, фазовое различие устраняет необходимость в применении линейной логики между различными типами и терминами программирования. [3]
Введение
Фазовое различие позволяет различать обработку, выполняемую во время компиляции, и обработку, выполняемую во время выполнения.
Рассмотрим простой язык [3] с терминами:
t ::= true | false | x | λx : T . t | tt | если t, то t, иначе t
и типы:
T ::= Бул | T -> T
Обратите внимание, как типы и термины различаются. Во время компиляции типы используются для проверки действительности терминов. Однако типы не играют никакой роли во время выполнения.
Ссылки
- ^ Карделли, Лука (3 января 1988 г.). "Фазовые различия в теории типов" (PDF) . Digital Equipment Corporation .
- ^ Карделли, Лука (3 января 1988 г.). "Фазовые различия в теории типов" (PDF) . Digital Equipment Corporation .
- ^ ab "CMSC 336: Системы типов для языков программирования; Лекция 7: Изоморфизм Карри-Ховарда и производные формы" (PDF) . 31 января 2008 г.
