here are fixed-length vectors defined in terms of naturals 

Vec: Type → ℕ → Type
Vec A 0 = ⊤
Vec A (S n) = A × Vec A n

nil: (A: Type) → Vec A 0
nil A = ()

cons: (A: Type) → (n: ℕ) → (a: A) → Vec A n → Vec A (S n)
cons A n a as = (a, as) as A × Vec A (S n)

match: (A: Type)
→ (P: (n: ℕ) → Vec A n → Type)
→ P 0 (nil A)
→ ((n: ℕ) → (a: A) → (as: Vec A n)
→ P (S n) (cons A n a as))
→ (n: ℕ) → (Vec A n)
match A P Pn Pc 0 () = Pn
match A P Pn Pc (S n) (a, as) = Pc n a as

I've always thought that vectors are more "complex" than lists because they have a length index but I don't think I can define parametrized, non-indexed lists with only the power of naturals (and maybe equality)

@ionchy Are sigma types allowed? Then it's Sigma n : N . Vec n a

@ionchy With the power of container types 💪 (or polynomial functors, whatever you prefer)

Sign in to participate in the conversation

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.