Функции Agda, соответствие функций по типам

Question

Я хочу создать вспомогательную функцию, которая возьмет термин из индексированного или параметризованного типа и вернет этот параметр типа.

showLen : {len : ℕ} {A : Set} -> Vec A len -> ℕ 
showLen ? = len 

showType : {len : ℕ} {A : Set} -> Vec A len -> Set 
showType ? = A 

Возможно ли это? (? Я могу видеть, как showType [] могут возникнуть проблемы, но то, что о том, когда тип индексируется)

Answer 1

Если вы избавитесь от неявных аргументов, вы можете осуществить это довольно легко:

showLen : (len : ℕ) (A : Set) → Vec A len → ℕ 
showLen len _ _ = len 

В самом деле, мы можем сделать оба сразу:

open import Data.Product 

showBoth : (len : ℕ) (A : Set) → Vec A len → ℕ × Set 
showBoth len A _ = len , A 

Теперь неявные аргументы как обычные аргументы за исключением того, что компилятор будет пытаться заполнить их самостоятельно. Мы всегда можем отменить это поведение, если захотим или понадобится.

Если вы хотите реализовать функцию, которая имеет скрытые аргументы и вы каким-то образом нужно получить доступ к ним, вы можете сделать это, упоминая их в фигурные скобки, например:

replicate : {n : ℕ} {A : Set} → A → Vec A n 
replicate {zero} _ = [] 
replicate {suc _} x = x ∷ replicate x 

Когда вы тогда хотите позвонить функция и нужно указать скрытый аргумент, процесс аналогичен:

vec : Vec ℕ 4 
vec = replicate {4} 0 

Теперь мы просто применить это showBoth приведенные выше:

showBoth : {len : ℕ} {A : Set} → Vec A len → ℕ × Set 
showBoth {len} {A} _ = len , A 

---

Теперь, если ваши аргументы оказались в неправильном порядке; Например, вы хотели бы, чтобы явно дать A аргумент, но не n аргумента, вы должны были бы сделать это:

vec₂ : Vec ℕ 4 
vec₂ = replicate {_} {ℕ} 0 

Теперь, если вам необходимо заполнить п -м неявного аргумента, это будет очень утомительно. Таким образом, Agda дает нам возможность обратиться к ним по имени:

vec₃ : Vec ℕ 4 
vec₃ = replicate {A = ℕ} 0 

Это использует имя, данное в сигнатуре типа. Вы также можете использовать это при определении функции:

showType : {len : ℕ} {A : Set} → Vec A len → Set 
showType {A = Type} _ = Type