В библиотечных эффектах Idris Effects представлены как
||| This type is parameterised by:
||| + The return type of the computation.
||| + The input resource.
||| + The computation to run on the resource given the return value.
Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type
Если мы позволяем ресурсам быть значениями и свопим первые два аргумента, мы получаем (остальная часть кода находится в Agda)
Effect : Set -> Set
Effect R = R -> (A : Set) -> (A -> R) -> Set
Имея некоторый базовый тип-компонент-членский механизм
data Type : Set where
nat : Type
_⇒_ : Type -> Type -> Type
data Con : Set where
ε : Con
_▻_ : Con -> Type -> Con
data _∈_ σ : Con -> Set where
vz : ∀ {Γ} -> σ ∈ Γ ▻ σ
vs_ : ∀ {Γ τ} -> σ ∈ Γ -> σ ∈ Γ ▻ τ
мы можем кодировать конструкторы лямбда-терминов следующим образом:
app-arg : Bool -> Type -> Type -> Type
app-arg b σ τ = if b then σ ⇒ τ else σ
data TermE : Effect (Con × Type) where
Var : ∀ {Γ σ } -> σ ∈ Γ -> TermE (Γ , σ ) ⊥ λ()
Lam : ∀ {Γ σ τ} -> TermE (Γ , σ ⇒ τ ) ⊤ (λ _ -> Γ ▻ σ , τ )
App : ∀ {Γ σ τ} -> TermE (Γ , τ ) Bool (λ b -> Γ , app-arg b σ τ)
In TermE i r i′ i - это индекс вывода (например, lambda abstractions (Lam)), (для удобства описания я проигнорирую, что индексы также содержат контексты помимо типов)), r представляет собой ряд индуктивных положений (Var не принимает (⊥) любой TermE, Lam получает один (⊤), App получает два (Bool) - a функция и ее аргумент) и i′ вычисляет индекс в каждом индуктивном положении (например, индекс в первом индуктивном положении App равен σ ⇒ τ, а индекс во втором - σ, т.е. мы можем применить функцию к значению, только если тип первого аргумента функции равен типу значения).
Чтобы построить реальный лямбда-член, мы должны связать узел, используя что-то вроде типа данных W. Вот определение:
data Wer {R} (Ψ : Effect R) : Effect R where
call : ∀ {r A r′ B r′′} -> Ψ r A r′ -> (∀ x -> Wer Ψ (r′ x) B r′′) -> Wer Ψ r B r′′
Это индексированный вариант монады Олега Киселева Freer, но без return. Используя это, мы можем восстановить обычные конструкторы:
_<∨>_ : ∀ {B : Bool -> Set} -> B true -> B false -> ∀ b -> B b
(x <∨> y) true = x
(x <∨> y) false = y
_⊢_ : Con -> Type -> Set
Γ ⊢ σ = Wer TermE (Γ , σ) ⊥ λ()
var : ∀ {Γ σ} -> σ ∈ Γ -> Γ ⊢ σ
var v = call (Var v) λ()
ƛ_ : ∀ {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ ⇒ τ
ƛ b = call Lam (const b)
_·_ : ∀ {Γ σ τ} -> Γ ⊢ σ ⇒ τ -> Γ ⊢ σ -> Γ ⊢ τ
f · x = call App (f <∨> x)
Вся кодировка очень похожа на соответствующую кодировку в терминах индексированные контейнеры: Effect соответствует IContainer, а Wer соответствует ITree (тип деревьев Петерссона-Синека). Однако приведенная выше кодировка выглядит мне проще, потому что вам не нужно думать о вещах, которые вы должны вводить в формы, чтобы иметь возможность восстанавливать индексы на индуктивных позициях. Вместо этого у вас есть все в одном месте, и процесс кодирования действительно прост.
Так что я здесь делаю? Существует ли какое-то реальное отношение к подходу с индексированными контейнерами (помимо того факта, что эта кодировка имеет те же проблемы с расширением)? Можем ли мы сделать что-то полезное таким образом? Одна естественная мысль состоит в том, чтобы создать эффективный лямбда-исчисление, так как мы можем свободно смешивать лямбда-члены с эффектами, поскольку сам лямбда-член сам по себе является эффектом, но он является внешним эффектом, и мы также нуждаемся в том, чтобы другие эффекты были внешними (что означает, что мы не можем сказать что-то вроде tell (var vz), потому что var vz не является значением - это вычисление), или нам нужно каким-то образом интернализировать этот эффект и весь механизм эффектов (что означает, что я не знаю, что).
