Additional Exercises

Many common functions on lists can be implemented in terms of Fold. For example, here's an alternative definition of length:

Fold_length <x> (xs: List x) : Nat
Fold_length xs = Fold (x => y Nat.succ y) xs 0n

Test_fold_length1 : Equal (Fold_length [4, 7, 0]) 3n
Test_fold_length1 = Equal.refl

Prove the validity of Fold_length:

Fold_length_correct <x> (xs: List x) : Equal (Fold_length xs) (List.length xs)
Fold_length_correct xs = ?

We can also define Map in terms of Fold. Complete the function:

Fold_map <x> <y> (f: x -> y) (xs: List x) : List y
Fold_map f xs = ?

Write a theorem fold_map_correct in Kind stating that Fold_map is correct and prove it:

Fold_map_correct : ?

In Kind, a function f: a -> b -> c actually has type a -> (b -> c). That is, if you give f a value of type a, it will provide the function g: b -> c. If you give g a value of type b, it will return a value of type c. This allows for partial application, as in Plus3. Processing a list of arguments with functions that return functions is called currying, in honor of the logician Haskell Curry.

On the other hand, we can reinterpret the function f: a -> b -> c as (Pair a b) -> c. This is called uncurrying. With a binary uncurry function, both arguments must be provided at the same time as a pair; there is no partial application.

We can define curry as follows:

Pair_curry <x> <y> <z> (f: (Pair x y) -> z) (x_val: x) (y_val: y) : z 
Pair_curry f x_val y_val = ?

As an exercise, define its inverse, Pair_uncurry. Then prove the theorems below to show that the two are inverses.

Pair_uncurry <x> <y> <z> (f: x -> y -> z) (p: Pair x y) : z
Pair_uncurry f p = ?

As a (trivial) example of the usefulness of curry, we can use it to shorten one of the examples we saw above:

Test_map2 : Equal (Map (x => Plus 3n x) [2n,0n,2n]) [5n,3n,5n]
Test_map2 = Equal.refl

Reflection exercise: before executing the following commands, can you calculate the types of Pair_curry and Pair_uncurry?

Uncurry_curry <x> <y> <z> (f: x -> y -> z) (x_val: x) (y_val: y) : 
   Equal z (Pair_curry (p => Pair_uncurry f p) x_val y_val) (f x_val y_val)
Uncurry_curry f x_val y_val = ?

Curry_uncurry <x> <y> <z> (f:(Pair x y) -> z) (p: Pair x y) : 
   Equal z (Pair_uncurry (x => y => Pair_curry f x y) p) (f p)
Curry_uncurry f p = ?

Remember the definition of the function Nth_error(Nth_error_informal):

Nth_error_informal <x> (l: List x) (n: Nat) : Maybe x
Nth_error_informal List.nil n = Maybe.none 
Nth_error_informal (List.cons head tail) Nat.zero = Maybe.some head 
Nth_error_informal (List.cons head tail) (Nat.succ n) = Nth_error tail n

Write an informal proof of the following theorem:

Nat -> List -> (Equal (Length List) Nat) : Equal (Nth_error_informal List Nat) Maybe.none

We can explore an alternative way of defining natural numbers, using Church numerals, named after the mathematician Alonzo Church. We can represent a natural number n as a function that takes a function s as a parameter and returns s iterated n times.

Num <x> : Type
Num x = (x -> x) -> x -> x

Let's see how to write some numbers with this notation. Iterating a function once should be the same as just applying it. In this way:

One : Num
One = s => z => s z 

Note that the function applies an s to a z, if we read the s as successor and the z as zero, we have that One is equal to the successor of zero.

Similarly, Two applies the function s twice to z:

Two : Num
Two = s => z => s (s z)

Defining zero is a bit more complicated: how can we "apply a function zero times"? The answer is actually simple: just return the argument untouched.

Zero : Num
Zero = s => z => z

More generally, a number n can be written as s => z => s (s ... (s z) ...), with n occurrences of s. Note in particular how the function doit3times that we defined earlier is actually just the Church representation of 3.

Three : Num
Three = s => z => Doit3times s z

Complete the definitions of the following functions. Make sure the corresponding unit tests pass, proving them with Equal.refl.

Successor

Successor of a natural number:

Succ (n: Num) : Num
Succ n = ?

Succ_1 : Equal (Succ Zero) (One)
Succ_1 = ?

Succ_2 : Equal (Succ One) (Two)
Succ_2 = ?

Succ_3 : Equal (Succ Two) (Three)
Succ_3 = ?

Addition

Addition of two natural numbers:

Plus (n: Num) (n: Num) : Num
Plus n m = ?

Plus_1 : Equal (Plus One Zero) (One)
Plus_1 = ?

Plus_2 : Equal (Plus Two One) (Plus One Two)
Plus_2 = ?

Plus_3 : Equal (Plus (Plus Two Two) Three) (Plus One (Plus Three Three))
Plus_3 = ?

Multiplication

Mult (n: Num) (m: Num) : Num
Mult n m = ?

Mult_1 : Equal (Mult One One) One
Mult_1 = ?

Mult_2 : Equal (Mult Zero (Plus Three Three)) Zero
Mult_2 = ?

Mult_3 : Equal (Mult Two Three) (Plus Three Three)
Mult_3 = ?

Exponentiation

It is not possible to make it work with Exp (n: Num) (m: Num) : Num. Polymorphism plays a crucial role here. However, choosing the right type to iterate over can be tricky. If you encounter an "inconsistency" error, try iterating over a different type: Num itself is usually problematic.

Exp (n: Num) (m: Num -> Num) : Num
Exp n m = ?

Exp_1 : Equal (Exp Two Two) (Plus Two Two)
Exp_1 = ?

Exp_2 : Equal (Exp Three Two) (Plus (Mult Two (Mult Two Two)) One)
Exp_2 = ?

Exp_3 : Equal (Exp Three Zero) One
Exp_3 = ?

Predecessor

Pred (n: Num -> Num) : Num
Pred n = ?

Pred_1 : Equal (Pred Zero) (Zero)
Pred_1 = ?

Pred_2 : Equal (Pred Two) (One)
Pred_2 = ?

Pred_3 : Equal (Pred Three) (Two)
Pred_3 = ?

Subtraction

Sub (n: Num) (m: Num) : Num
Sub n m = ?

Sub_1 : Equal (Sub One Zero) (One)
Sub_1 = ?

Sub_2 : Equal (Sub Two Two) (Sub One One)
Sub_2 = ?

Sub_3 : Equal (Sub Three One) Two
Sub_3 = ?