module Vector where {- Another use of dependent types is to make a type depend on a variable of another data type. For example, we can define the data type Vect A n of vectors (lists) of length n : Nat. Before we define this type we need to import the natural numbers file and open the module so that the names defined there are in scope. We write -} open import Nat {- Now we can declare data type of vectors as follows: -} data Vect (A : Set) : Nat → Set where [] : Vect A zero _::_ : {n : Nat} → A → Vect A n → Vect A (succ n) {- This means that we have declared the following constants Vect : Set → Nat → Set [] : {A : Set} → Vect A zero _::_ : {A : Set} → {n : Nat} → A → Vect A n → Vect A (succ n) which entail that Vect A n is a vector of length n, by declaring that the empty vector has length 0 and cons adds one to the length of a vector. One may ask why the type Set occurs to the left and the type Nat occurs to the right of the :-sign in the type declaration. This is because we want to make the constructors polymorphic in A : Set but not in n : Nat. Now we have a new way of writing the type of the head function, expressing that it is a total function of vectors of length at least 1: -} head : {A : Set} → {n : Nat} → Vect A (succ n) → A head (a :: as) = a {- Similarly, the type of the tail function is: -} tail : {A : Set} → {n : Nat} → Vect A (succ n) → Vect A n tail (a :: as) = as {- And we can now express that map preserves the length of the input vector: -} map : {A B : Set} → {n : Nat} → (A → B) → Vect A n → Vect B n map f [] = [] map f (a :: as) = f a :: map f as {- Exercise: Define the Haskell zip function which takes two lists as inputs and outputs the corresponding lists of pairs. The type of this function is zip : {A B : Set} -> List A -> List B -> List (A × B) where you get access to the product type A × B by writing open import Product Alternatively, if you have installed the standard library you can import products from there by writing open import Data.Product Note that you need to decide what to do when you zip lists of unequal length. (What does Haskell do?) Then define it instead as a function on vectors expressing that the two input vectors (and also the output vector) should have the same length: zip : {A B : Set} → {n : Nat} → Vect A n → Vect B n → Vect (A × B) n -}