В этом документе x⃗ означает «Последовательность x , разделенных соответствующими разделителями» .
Несколько примеров:
Если x - переменная, λ x⃗ . e - это сокращение от λ x 1 . λ x 2 . … Λ x n e . Другими словами, много вложенных лямбд с одним аргументом или лямбда с множеством аргументов.
Если σ и τ являются типами, σ⃗ → τ - сокращение для σ 1 → σ 2 →… → σ n → τ . Другими словами, тип функции с множеством типов параметров.
Если a - это переменная типа, а σ - это тип, ∀ a⃗ . σ - это сокращение от ∀ a 1 . ∀ а 2 . … ∀ a n . σ . Другими словами, многие вложенные функции polymorphi c или функция polymorphi c с множеством параметров типа.
На рисунке 1 в документе синтаксис выражения перехода определяется как:
e , u , v ⩴… | прыжок j ϕ⃗ e⃗ τ
Если это объявление было переведено на a Haskell тип данных, это может выглядеть так:
data Term
-- | A jump expression has a label that it jumps to, a list of type argument
-- applications, a list of term argument applications, and the return type
-- of the overall `jump`-expression.
= Jump LabelVar [Type] [Term] Type
| ... -- Other syntactic forms.
То есть конструктор данных, который принимает переменную-метку j , последовательность аргументов типа ϕ⃗ , последовательность аргументов термина e⃗ и тип возвращаемого значения τ .
«Объединение» вещей:
Иногда несколько Использование верхней стрелки накладывает неявное ограничение на то, что их последовательности имеют одинаковую длину. Одно из мест, где это происходит, - это замены.
{ ϕ / ⃗ a } означает «заменить a 1 с ϕ 1 , заменить a 2 на ϕ 2 ,…, заменить a n с ϕ n ”, неявно утверждая, что и a⃗ и ϕ⃗ имеют одинаковую длину, n .
Рабочий пример: правило JUMP:
Правило JUMP интересно тем, что оно обеспечивает несколько вариантов использования секвенирования и даже последовательность из помещений . Вот опять правило:
( j : ∀ a⃗ . σ⃗ → ∀ r . r ) ∈ Δ
(Γ; ε ⊢⃗ u : σ { ϕ / ⃗ а })
Γ; Δ ⊢ прыжок j ϕ⃗ u⃗ τ : τ
Первая посылка должна быть довольно простой, теперь: найдите j в контексте метки Δ и убедитесь, что тип j начинается с набора ∀, за которым следует набором типов функций, заканчивающихся на ∀ r . r .
Вторая «посылка» на самом деле представляет собой последовательность посылок. Что это зацикливается? Пока что последовательности, которые мы имеем в области видимости: ϕ⃗ , σ⃗ , a⃗ и u⃗ .
ϕ⃗ и a⃗ используются во вложенной последовательности, поэтому, вероятно, не эти два.
С другой стороны, u⃗ и σ⃗ кажутся вполне правдоподобными, если учесть, что они означают.
σ⃗ - это список типов аргументов, ожидаемых меткой j и u⃗ - это список терминов аргументов, предоставленный метке j , и имеет смысл, что вы можете захотеть перебирать типы аргументов и термины аргументов вместе.
Итак, эта «предпосылка» на самом деле означает что-то вроде этого:
для каждой пары σ и u :
Γ; ε ⊢ u : σ { ϕ / ⃗ a }
Псевдо- Haskell реализация
Наконец, вот отчасти полный пример кода, иллюстрирующий, как это правило ввода может выглядеть в реальной реализации. x⃗ реализован как список x значений, а некоторая монада M используется для сигнализации отказа, когда предпосылка не выполняется.
data LabelVar
data Type
= ...
data Term
= Jump LabelVar [Type] [Term] Type
| ...
typecheck :: TermContext -> LabelContext -> Term -> M Type
typecheck gamma delta (Jump j phis us tau) = do
-- Look up `j` in the label context. If it's not there, throw an error.
typeOfJ <- lookupLabel j delta
-- Check that the type of `j` has the right shape: a bunch of `foralls`,
-- followed by a bunch of function types, ending with `forall r.r`. If it
-- has the correct shape, split it into a list of `a`s, a list of `\sigma`s
-- and the return type, `forall r.r`.
(as, sigmas, ret) <- splitLabelType typeOfJ
-- exactZip is a helper function that "zips" two sequences together.
-- If the sequences have the same length, it produces a list of pairs of
-- corresponding elements. If not, it raises an error.
for each (u, sigma) in exactZip (us, sigmas):
-- Type-check the argument `u` in a context without any tail calls,
-- and assert that its type has the correct form.
sigma' <- typecheck gamma emptyLabelContext u
-- let subst = { \sequence{\phi / a} }
subst <- exactZip as phis
assert (applySubst subst sigma == sigma')
-- After all the premises have been satisfied, the type of the `jump`
-- expression is just its return type.
return tau
-- Other syntactic forms
typecheck gamma delta u = ...
-- Auxiliary definitions
type M = ...
instance Monad M
lookupLabel :: LabelVar -> LabelContext -> M Type
splitLabelType :: Type -> M ([TypeVar], [Type], Type)
exactZip :: [a] -> [b] -> M [(a, b)]
applySubst :: [(TypeVar, Type)] -> Type -> Type