Как написать общие функции арности в Agda? Можно ли написать полностью зависимые и полиморфные вселенную общие функции с арностью?
Универсальное программирование Arity в 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
, которая имеет арность 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
C-c C-r уменьшает дыру до λ 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 Programming", который описывает, среди прочего, как писать общие функции арности, которые получают аргументы разных типов. Идея состоит в том, чтобы передать вектор типов в качестве параметра и свернуть его в стиле N-ary
:
arrTy : {n : N} → Vec Set (suc n) → Set
arrTy {0} (A :: []) = A
arrTy {suc n} (A :: As) = A → arrTy As
Однако Agda не может вывести этот вектор, даже если мы укажем его длину. Следовательно, в документе также представлен оператор каррирования, который делает из функции, которая явно получает вектор типов, функцию, которая получает 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
— это иллюстрирует полиморфизм вселенной.
Примечания
Насколько я знаю, для неявных аргументов нет понятной теории, поэтому я не знаю, как все это будет работать, когда вторая функция (т.е. 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'
Но это обычное дело для Agda, например. вы не можете применить явный id
к себе:
idₑ : ∀ α -> (A : Set α) -> A -> A
idₑ _ _ x = x
-- ... because this would result in an invalid use of Setω ...
error = idₑ _ _ idₑ
код.