module X2 where ---------------------------------------------------------------------- -- Exercise 2 : Vectors -- ---------------------------------------------------------------------- -- LIBRARY data Nat : Set where zero : Nat suc : Nat -> Nat data _^_ (X : Set) : Nat -> Set where [] : X ^ zero _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n _+_ : Nat -> Nat -> Nat zero + y = y suc x + y = suc (x + y) data Maybe (X : Set) : Set where just : X -> Maybe X nothing : Maybe X vec : {n : Nat}{X : Set} -> X -> X ^ n vec {zero} x = [] vec {suc n} x = x :: vec {n} x _\$s_ : {n : Nat}{S T : Set} -> (S -> T) ^ n -> S ^ n -> T ^ n [] \$s [] = [] (f :: fs) \$s (s :: ss) = f s :: (fs \$s ss) infixl 90 _\$s_ -- EXERCISES (usual hints apply) -- Vector basics {- (2.1) Implement vector concatenation. (Guess the length!) -} _++_ : {m n : Nat}{X : Set} -> X ^ m -> X ^ n -> X ^ {! !} xs ++ ys = {! !} {- (2.2) Show how to compute the sum a vector of numbers. -} sum : {n : Nat} -> Nat ^ n -> Nat sum xs = {! !} {- (2.3) Compute the scalar product of two vectors (the sum of the products of corresponding elements). You'll need to define multiplication, of course. -} _times_ : Nat -> Nat -> Nat m times n = {! !} _dot_ : {n : Nat} -> Nat ^ n -> Nat ^ n -> Nat xs dot ys = {! !} {- (2.4) Define Maybe-application, returning a value where possible. -} _\$m_ : {S T : Set} -> Maybe (S -> T) -> Maybe S -> Maybe T fm \$m sm = {! !} {- Compare (vec, _\$s_) with (just, _\$m_). Do you see a pattern? -} {- (2.5) Show how to construct a vector of values from a vector of maybe-values, provided they are all "just". -} allJust : {n : Nat}{X : Set} -> Maybe X ^ n -> Maybe (X ^ n) allJust xms = {! !} -- Matrices: rows of columns Matrix : Set -> Nat -> Nat -> Set Matrix X m n = (X ^ m) ^ n {- (2.6) Define the identity matrix of a given size (one on the diagonal, zero off) -} identity : {n : Nat} -> Matrix Nat n n identity {n} = {! !} {- (2.7*) Define matrix transposition. -} transpose : {m n : Nat}{X : Set} -> Matrix X m n -> Matrix X n m transpose xmn = {! !} {- (2.8) Define matrix multiplication. -} _mmult_ : {l m n : Nat} -> Matrix Nat l m -> Matrix Nat m n -> Matrix Nat l n xlm mmult xmn = {! !}