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