В библиотеке эффектов 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 σ τ)
В TermE i r i′ i - это выходной индекс (например, лямбда-абстракции (Lam) создают типы функций (σ ⇒ τ) (для простоты описания я проигнорирую, что индексы также содержат контексты помимо типов)), r представляет собой количество индуктивных позиций (Var не ' t (⊥) принимает любое TermE, Lam получает один (⊤), App получает два (Bool) - функцию и ее аргумент) и 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 не значение - это вычисление) или нам нужно как-то усвоить этот эффект и весь механизм эффектов (что означает, что я не знаю что).
