Arity-универсальное программирование в Agda
Как написать универсальные функции в Agda? Можно ли написать полностью зависимые и универсальные полиморфные функции общего типа?
1 ответ
Я возьму n-арную композиционную функцию в качестве примера.
Самая простая версия
open import Data.Vec.N-ary
comp : ∀ n {α β γ} {X : Set α} {Y : Set β} {Z : Set γ}
-> (Y -> Z) -> N-ary n X Y -> N-ary n X Z
comp 0 g y = {!!}
comp (suc n) g f = {!!}
Вот как N-ary определяется в Data.Vec.N-ary модуль:
N-ary : ∀ {ℓ₁ ℓ₂} (n : ℕ) → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
N-ary zero A B = B
N-ary (suc n) A B = A → N-ary n A B
Т.е. comp получает номер n, функция g : Y -> Z и функция f, который имеет arity n и результирующий тип Y,
в comp 0 g y = {!!} случай у нас есть
Goal : Z
y : Y
g : Y -> Z
следовательно, отверстие может быть легко заполнено g y,
в comp (suc n) g f = {!!} дело, N-ary (suc n) X Y сводится к X -> N-ary n X Y а также N-ary (suc n) X Z сводится к X -> N-ary n X Z, Итак, мы имеем
Goal : X -> N-ary n X Z
f : X -> N-ary n X Y
g : Y -> Z
Cc Cr уменьшает отверстие до λ x -> {!!}, и сейчас Goal : N-ary n X Z, который может быть заполнен comp n g (f x), Таким образом, все определение
comp : ∀ n {α β γ} {X : Set α} {Y : Set β} {Z : Set γ}
-> (Y -> Z) -> N-ary n X Y -> N-ary n X Z
comp 0 g y = g y
comp (suc n) g f = λ x -> comp n g (f x)
Т.е. comp получает n аргументы типа X, применяется f к ним, а затем относится g к результату.
Простейшая версия с зависимой g
когда g имеет тип (y : Y) -> Z y
comp : ∀ n {α β γ} {X : Set α} {Y : Set β} {Z : Y -> Set γ}
-> ((y : Y) -> Z y) -> (f : N-ary n X Y) -> {!!}
comp 0 g y = g y
comp (suc n) g f = λ x -> comp n g (f x)
что там должно быть в дыре? Мы не можем использовать N-ary n X Z как и раньше, потому что Z теперь это функция. Если Z это функция, мы должны применить ее к чему-то, что имеет тип Y, Но единственный способ получить что-то типа Y это применить f в n аргументы типа X, Который так же, как наш comp но только на уровне типа:
Comp : ∀ n {α β γ} {X : Set α} {Y : Set β}
-> (Y -> Set γ) -> N-ary n X Y -> Set (N-ary-level α γ n)
Comp 0 Z y = Z y
Comp (suc n) Z f = ∀ x -> Comp n Z (f x)
А также comp тогда это
comp : ∀ n {α β γ} {X : Set α} {Y : Set β} {Z : Y -> Set γ}
-> ((y : Y) -> Z y) -> (f : N-ary n X Y) -> Comp n Z f
comp 0 g y = g y
comp (suc n) g f = λ x -> comp n g (f x)
Версия с аргументами разных типов
Существует статья " Arity-generic datatype-generic Программирование ", в которой, помимо прочего, описывается, как писать функции arity-generic, которые получают аргументы разных типов. Идея состоит в том, чтобы передать вектор типов в качестве параметра и сложить его в значительной степени в стиле N-ary:
arrTy : {n : N} → Vec Set (suc n) → Set
arrTy {0} (A :: []) = A
arrTy {suc n} (A :: As) = A → arrTy As
Однако Агда не может вывести этот вектор, даже если мы предоставим его длину. Следовательно, документ также предоставляет оператор для каррирования, который делает из функции, которая явно получает вектор типов, функцию, которая получает n неявные аргументы.
Этот подход работает, но он не масштабируется до полностью универсальных полиморфных функций. Мы можем избежать всех этих проблем, заменив Vec тип данных с _^_ оператор:
_^_ : ∀ {α} -> Set α -> ℕ -> Set α
A ^ 0 = Lift ⊤
A ^ suc n = A × A ^ n
A ^ n изоморфен Vec A n, Тогда наш новый N-ary является
_->ⁿ_ : ∀ {n} -> Set ^ n -> Set -> Set
_->ⁿ_ {0} _ B = B
_->ⁿ_ {suc _} (A , R) B = A -> R ->ⁿ B
Все типы лежат в Set для простоты. comp сейчас
comp : ∀ n {Xs : Set ^ n} {Y Z : Set}
-> (Y -> Z) -> (Xs ->ⁿ Y) -> Xs ->ⁿ Z
comp 0 g y = g y
comp (suc n) g f = λ x -> comp n g (f x)
И версия с зависимой g:
Comp : ∀ n {Xs : Set ^ n} {Y : Set}
-> (Y -> Set) -> (Xs ->ⁿ Y) -> Set
Comp 0 Z y = Z y
Comp (suc n) Z f = ∀ x -> Comp n Z (f x)
comp : ∀ n {Xs : Set ^ n} {Y : Set} {Z : Y -> Set}
-> ((y : Y) -> Z y) -> (f : Xs ->ⁿ Y) -> Comp n Z f
comp 0 g y = g y
comp (suc n) g f = λ x -> comp n g (f x)
Полностью зависимый и универсальный полиморфный comp
Основная идея состоит в том, чтобы представлять вектор типов как вложенные зависимые пары:
Sets : ∀ {n} -> (αs : Level ^ n) -> ∀ β -> Set (mono-^ (map lsuc) αs ⊔ⁿ lsuc β)
Sets {0} _ β = Set β
Sets {suc _} (α , αs) β = Σ (Set α) λ X -> X -> Sets αs β
Второй случай читается как "есть тип X так что все другие типы зависят от элемента X ". Наш новый N-ary тривиально:
Fold : ∀ {n} {αs : Level ^ n} {β} -> Sets αs β -> Set (αs ⊔ⁿ β)
Fold {0} Y = Y
Fold {suc _} (X , F) = (x : X) -> Fold (F x)
Пример:
postulate
explicit-replicate : (A : Set) -> (n : ℕ) -> A -> Vec A n
test : Fold (Set , λ A -> ℕ , λ n -> A , λ _ -> Vec A n)
test = explicit-replicate
Но каковы типы Z а также g сейчас?
comp : ∀ n {β γ} {αs : Level ^ n} {Xs : Sets αs β} {Z : {!!}}
-> {!!} -> (f : Fold Xs) -> Comp n Z f
comp 0 g y = g y
comp (suc n) g f = λ x -> comp n g (f x)
Напомним, что f ранее имел тип Xs ->ⁿ Y, но Y теперь скрыто в конце этих вложенных зависимых пар и может зависеть от элемента любого X от Xs, Z ранее имел тип Y -> Set γ следовательно, теперь нам нужно добавить Set γ в Xs, делая все x с неявным:
_⋯>ⁿ_ : ∀ {n} {αs : Level ^ n} {β γ}
-> Sets αs β -> Set γ -> Set (αs ⊔ⁿ β ⊔ γ)
_⋯>ⁿ_ {0} Y Z = Y -> Z
_⋯>ⁿ_ {suc _} (_ , F) Z = ∀ {x} -> F x ⋯>ⁿ Z
в порядке, Z : Xs ⋯>ⁿ Set γ какой тип имеет g? Ранее это было (y : Y) -> Z y, Снова нам нужно добавить что-то к вложенным зависимым парам, так как Y снова скрыт, только теперь зависимым образом:
Πⁿ : ∀ {n} {αs : Level ^ n} {β γ}
-> (Xs : Sets αs β) -> (Xs ⋯>ⁿ Set γ) -> Set (αs ⊔ⁿ β ⊔ γ)
Πⁿ {0} Y Z = (y : Y) -> Z y
Πⁿ {suc _} (_ , F) Z = ∀ {x} -> Πⁿ (F x) Z
И наконец
Comp : ∀ n {αs : Level ^ n} {β γ} {Xs : Sets αs β}
-> (Xs ⋯>ⁿ Set γ) -> Fold Xs -> Set (αs ⊔ⁿ γ)
Comp 0 Z y = Z y
Comp (suc n) Z f = ∀ x -> Comp n Z (f x)
comp : ∀ n {β γ} {αs : Level ^ n} {Xs : Sets αs β} {Z : Xs ⋯>ⁿ Set γ}
-> Πⁿ Xs Z -> (f : Fold Xs) -> Comp n Z f
comp 0 g y = g y
comp (suc n) g f = λ x -> comp n g (f x)
Тест:
length : ∀ {α} {A : Set α} {n} -> Vec A n -> ℕ
length {n = n} _ = n
explicit-replicate : (A : Set) -> (n : ℕ) -> A -> Vec A n
explicit-replicate _ _ x = replicate x
foo : (A : Set) -> ℕ -> A -> ℕ
foo = comp 3 length explicit-replicate
test : foo Bool 5 true ≡ 5
test = refl
Обратите внимание на зависимость в аргументах и результирующий тип explicit-replicate, Кроме того, Set заключается в Set₁, в то время как ℕ а также A роды Set - это иллюстрирует полиморфизм вселенной.
замечания
AFAIK, нет понятной теории для неявных аргументов, поэтому я не знаю, как все это будет работать, когда вторая функция (т.е. f) получает неявные аргументы. Этот тест:
foo' : ∀ {α} {A : Set α} -> ℕ -> A -> ℕ
foo' = comp 2 length (λ n -> replicate {n = n})
test' : foo' 5 true ≡ 5
test' = refl
передается по крайней мере.
comp не может обрабатывать функции, если от значения зависит юниверс, в котором находится некоторый тип. Например
explicit-replicate' : ∀ α -> (A : Set α) -> (n : ℕ) -> A -> Vec A n
explicit-replicate' _ _ _ x = replicate x
... because this would result in an invalid use of Setω ...
error : ∀ α -> (A : Set α) -> ℕ -> A -> ℕ
error = comp 4 length explicit-replicate'
Но для Агды это характерно, например, вы не можете применить явное id к себе:
idₑ : ∀ α -> (A : Set α) -> A -> A
idₑ _ _ x = x
-- ... because this would result in an invalid use of Setω ...
error = idₑ _ _ idₑ
Код.