Agda functions, function matching on types

Question

I want to create a helper function, that will take a term from a an indexed or parametrized type and return that type parameter.

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

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

Is this possible? (I can see how showType [] might have issues, but what about when the Type is indexed?)

Answer 1

If you get rid of the implicit arguments, you can implement this quite easily:

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

In fact, we can do both at once:

open import Data.Product

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

Now, implicit arguments are just like normal arguments save for the fact that compiler will try to fill them on its own. We can always override this behaviour if we want or need to.

If you want to implement a function that has hidden arguments and you somehow need to access them, you can do so by mentioning them inside curly braces, like this:

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

When you then want to call a function and need to specify a hidden argument, the process is similar:

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

Now, we just apply this to showBoth given above:

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

---

Now, if your arguments happen to be in wrong order; for example you'd like to explicitly give the A argument but not the n argument, you'd have to do this:

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

Now, if you needed to fill in n-th implicit argument, this would get tedious very quickly. So, Agda gives us the option to refer to them by a name:

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

This uses the name given in the type signature. You can also use this when defining a function:

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