Могут ли зависимые типы абстрагироваться от функций с n аргументами?

Зависимые типы (pis) в основном представляют собой «усиленные» формы функциональных пространств (стрелки).

Если ты видишь:

Pi x : T. T(x)

Тогда это тип, который в основном говорит: «дайте мне x типа T, я дам вам что-то типа T(x)».

В вырожденном случае, когда T не имеет экземпляров x в своем теле, это эквивалентно T1 -> T2 в других языках (заменив T1 на вещь в x выше). Простой ответ на ваш вопрос заключается в том, что нет, вы не можете увеличить «количество стрелок» в типе, но вы можете сделать что-то в этом роде, если у вас есть это.

Pi x : nat. listoflength(x)

где listoflength — это то, что генерирует список (некоторого типа, возможно, с другим параметром) длиной x. Вы могли бы, например, реализовать его, используя тип сигмы (например, список с длиной в качестве аргумента свойства аля этот метод). Проблема в том, что аргументы должны быть однородного типа. Альтернативой является создание функции, которая, учитывая аргумент, возвращает вам кортеж из n вещей, каждая из которых имеет определенный тип.

Основная проблема заключается в том, что если вы задаете конкретное n, то вам нужно иметь возможность сказать: «Я принимаю n аргументов, вот их типы», чтобы выполнить всю арифметику типов.

Таким образом, хотя вы не можете создать любое количество стрелок, вы можете создать что-то, что генерирует функцию, которая принимает кортеж в качестве входных данных (и я полагаю, что если бы вы знали n, вы могли бы удалить его в тех местах, где он использовался).

В практическом программировании с зависимым типом я не знаю, насколько это было бы полезно (у меня нет доказательств того, что это было бы бесполезно), но я мог видеть случай для функций, которые принимали списки определенного размера, где размер должен иметь некоторые статические вычисления, чтобы доказать, что они «совпадают». В тех случаях, когда вы хотите принимать разнородные типы ввода, рассуждать об этом на практике может быть сложно, и я обычно стараюсь избегать этого с точки зрения практики кодирования. В динамических языках, где у вас может быть переменное количество аргументов, кажется, что вариант использования, вероятно, заключается в том, что он позволяет вам морально «перегружать» функцию легко, но в языках с зависимой типизацией просто кажется, что любое удобство записи, которое вы получили от этого, будет потеряно потому что вам нужно будет доказать, что вы правильно используете экземпляры.

Легко написать разнородные универсальные функции арности, если вы знаете прием, который описан в документе Arity-Generic Datatype-Generic Programming. Во-первых, вы делаете функцию, которая получает вектор типов, а во-вторых, вы "каррируете" эту функцию, чтобы она получала неявные типы вместо явного вектора.

Сначала немного импорта:

open import Data.Nat
open import Data.Vec
open import Data.Vec.N-ary

Вот два комбинатора из статьи:

∀⇒ : ∀ {n α β} {A : Set α} 
   -> (Vec A n -> Set β) 
   -> Set (N-ary-level α β n)
∀⇒ {0}     B = B []
∀⇒ {suc n} B = ∀ {x} -> ∀⇒ (λ xs -> B (x ∷ xs))

λ⇒ : ∀ {n α β} {A : Set α} {B : Vec A n -> Set β} 
   -> ((xs : Vec A n) -> B xs) 
   -> ∀⇒ B
λ⇒ {0}     f = f []
λ⇒ {suc n} f = λ {x} -> λ⇒ (λ xs -> f (x ∷ xs))

И зависимая полиморфная арно-общая функция композиции, которая получает явный вектор типов.

Vec-ary : ∀ {α γ l} -> Vec (Set α) l -> Set γ -> Set (N-ary-level α γ l)
Vec-ary  []      Z = Z
Vec-ary (X ∷ Xs) Z = X -> Vec-ary Xs Z

compT : ∀ {α β γ l} {Y : Set β} 
         -> (Xs : Vec (Set α) l)
         -> Vec-ary Xs Y
         -> (Y -> Set γ)
         -> Set (N-ary-level α γ l)
compT  []      y Z = Z y
compT (X ∷ Xs) g Z = (x : X) -> compT Xs (g x) Z

comp' : ∀ {α β γ l} {Y : Set β} {Z : Y -> Set γ}
      -> (Xs : Vec (Set α) l)
      -> (f : (y : Y) -> Z y)
      -> (g : Vec-ary Xs Y)
      -> compT Xs g Z
comp'  []      f y = f y
comp' (X ∷ Xs) f g = λ (x : X) -> comp' Xs f (g x)

Теперь легко сделать типы неявными:

comp : ∀ {α β γ} {Y : Set β} {Z : Y -> Set γ}
     -> (n : ℕ)
     -> ∀⇒ (λ (Xs : Vec (Set α) n)
           -> (f : (y : Y) -> Z y)
           -> (g : Vec-ary Xs Y)
           -> compT Xs g Z)
comp n = λ⇒ {n} comp'

И тест:

zeros : (n : ℕ) -> Vec ℕ n
zeros  0      = []
zeros (suc n) = 0 ∷ zeros n

comp-test-func-1 : ℕ -> Vec ℕ 0 -> Vec (Vec ℕ 1) 2 -> ℕ
comp-test-func-1 _ _ _ = 3

test-comp-1 : ℕ -> Vec ℕ 0 -> Vec (Vec ℕ 1) 2 -> Vec ℕ 3
test-comp-1 = comp 3 zeros comp-test-func-1

Однако есть один недостаток: все типы должны находиться в одном юниверсе, поэтому этот тест не пройден:

comp-test-func-2 : Set -> Vec ℕ 0 -> Vec (Vec ℕ 1) 2 -> ℕ
comp-test-func-2 _ _ _ = 3

test-comp-2 : Set -> Vec ℕ 0 -> Vec (Vec ℕ 1) 2 -> Vec ℕ 3
test-comp-2 = comp 3 zeros comp-test-func-2

Потому что Set и Vec ℕ 0 лежат в разных вселенных.

Однако можно сделать полностью полиморфную композиционную функцию, но только с полуявными аргументами. Итак, comp 3 становится comp (_ ∷ _ ∷ _ ∷ []), что некрасиво.