Vectors in different dependently typed programming lanugages

Vector.agda

-- Based on the built in Agda implementation

module Vec where
  -- The unit. A null of sorts.
  data One : Set where
    unit : One
    
  -- A tuple.
  data _*_ (A B : Set) : Set where
    pair : A -> B -> A * B
    
  -- A natural number is either zero or a successor of another natural number. One is suc zero, two is suc suc zero, etc.
  data Nat : Set where
    zero : Nat 
    suc  : Nat -> Nat
  
  -- A vector is parametrized by a natural number and some type.
  -- A zero length vector is a unit.
  -- A vector of any other length is a pair - an element and a vector of length one less than this one
  Vec : Nat -> Set -> Set
    Vec  zero   X = One
    Vec (suc n) X = X * Vec n X

Vectors.coq

(* Based on the built in Coq implementation *)

(* All sorts of imports, like natural numbers *)
Require Import Arith_base.
Require Vectors.Fin.
Import EqNotations.
Local Open Scope nat_scope.

(* A vector is parametrized by some type A (its contents) and a natural number (its length) *)
Inductive t A : nat -> Type :=
  |nil : t A 0 (* An empty vector is of length 0 *)
  |cons : forall (h:A) (n:nat), t A n -> t A (S n). (* Concating an element to a vector increases its size by one (S n) *)