module Homework1 where
-- You get access to the data type definitions below by downloading the lecture files and writing
--
-- open import Bool
-- open import Nat
-- open import Product
-- open import List
-- open import Vector
--
-- Alternatively, if you have installed the standard library you can import from there by writing
--
-- open import Data.Bool
-- open import Data.Nat
-- open import Data.Product
-- open import Data.List
-- open import Data.Vec
--
-- For your submission, you can either cut out the definitions and import the
-- lecture files or leave them as is.
{- -- >8 -- -}
data Bool : Set where
true false : Bool
data Nat : Set where
zero : Nat
succ : Nat → Nat
_+_ : Nat → Nat → Nat
n + zero = n
n + succ m = succ (n + m)
infixl 30 _*_
infixl 20 _+_
_*_ : Nat → Nat → Nat
n * zero = zero
n * succ m = n + n * m
data _×_ (A B : Set) : Set where
<_,_> : A → B → A × B
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
data Vect (A : Set) : Nat → Set where
[] : Vect A zero
_::_ : {n : Nat} → A → Vect A n → Vect A (succ n)
{- -- 8< -- -}
{-
Problem 1:
----------
Define logical or and logical equivalence
_||_ : Bool → Bool → Bool
_<=>_ : Bool → Bool → Bool
by pattern matching and refinement, using ^C^C, ^C^R, and ^C^SPC.
Compute some instances using ^C^N!
-}
{-
Problem 2:
----------
(a) Define the factorial function
factorial : Nat → Nat
Compute the result of factorial for some instances by normalizing with ^C^N. How large factorials can Agda compute?
(b) Define the power function
power : Nat → Nat → Nat
such that power m n = n^m. Compute the result of power for some instances of m by normalizing with ^C^N.
Agda's normalization is more general than the usual evaluator of a functional language. You can do "partial evaluation" or "program specialization" by running power only on its first argument. Compute in this way power zero, power one, power two, etc! What are the results? Could you achieve the same effect if you swapped the order of arguments to power?
-}
{-
Problem 3:
----------
Define the Maybe type in Agda and the function
data Maybe (A : Set) : Set
head : {A : Set} → List A -> Maybe A
-}
{-
Problem 4:
----------
(a) 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)
Note that you need to decide what to do when you zip lists of unequal length. (What does Haskell do?)
(b) 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:
vzip : {A B : Set} → {n : Nat} → Vect A n → Vect B n → Vect (A × B) n
-}