Functions as data
Functions as data Like many other modern programming languages -- including all functional languages (ML, Haskell, Scheme, Scala, Clojure, etc.) -- Kind treats functions as first-class citizens, allowing them to be passed as arguments to other functions, returned as results, stored in data structures, etc.
Higher-Order Functions
Functions that manipulate other functions are often called higher-order functions (or "higher-order" for short). Here is a simple example:
Doit3times <x> (f: x -> x) (n: x) : x
Doit3times f x = (f (f (f x)))
Test_doit3times1 : Equal (Doit3times (x => MinusTwo x) 9n) 3n
Test_doit3times1 = Equal.refl
Test_doit3times2 : Equal (Doit3times (x => Notb x) Bool.true) (Bool.false)
Test_doit3times2 = Equal.reflFilter
Here is a more useful higher-order function, taking a list of xs and a predicate on x (a function from x to Bool) and "filtering" the list, returning a new list containing only those elements for which the predicate returns Bool.true.
Filter <x> (test: x -> Bool) (xs: List x) : List x
Filter test List.nil = []
Filter test (List.cons head tail) =
Bool.if (test head) (List.cons head (Filter test tail)) (Filter test tail)For example, if we apply the "is even" filter to a list of numbers, it will return another list with only the even numbers.
Test_filter1 : Equal (Filter (x => Evenb x) [1,2,3,4,5]) [2,4]
Test_filter1 = Equal.refl
Length_is_one <x> (xs: List x) : Bool
Length_is_one xs = Eql (Length xs) 1n
Test_filter2 : Equal (Filter (x => Length_is_one x) ([[1],[1,2],[3],[1,2,3],[21]])) ([[1],[3],[21]])
Test_filter2 = Equal.reflWe can use filter to provide a concise version of the Countoddmembers function from the Lists chapter.
CountOddMembers (xs: List Nat) : Nat
CountOddMembers xs = Length (Filter (x => Oddb x) xs)
Test_CountOddMembers1 : Equal (CountOddMembers [1n,0n,3n,1n,4n,5n]) 4n
Test_CountOddMembers1 = Equal.refl
Test_CountOddMembers2 : Equal (CountOddMembers [0n 2n,4n]) 0n
Test_CountOddMembers2 = Equal.refl
Test_CountOddMembers3 : Equal (CountOddMembers []) 0n
Test_CountOddMembers3 = Equal.reflAnonymous Functions
It is arguably a bit sad, in the example above, to be forced to define the function Length_is_one and give it a name just to be able to pass it as an argument to filter, since we will probably never use it again.
Furthermore, this is not an isolated example: when using higher-order functions, we often want to pass "unique" functions as arguments that we will never use again; having to name each of these functions would be tedious.
Fortunately, there is a better way. We can build a function "on the fly" without declaring it at the top level or giving it a name.
Test_anon_fun : Equal (Doit3times (x => (Mult x x)) 2n) 256n
Test_anon_fun = Equal.reflThe expression x => (Mult x x) can be read as "the function takes a number n and returns n * n".
Here is the example of Filter rewritten to use an anonymous function:
Test_filter2 : Equal (Filter (x => (Length_is_one x)) [[1],[1,2],[2],[1,2,3],[21]]) [[1],[2],[21]]
Test_filter2 = Equal.refl
Filter_even_gt7
Use Filter with anonymous functions (instead of function definitions) to write a function Filter_even_gt7 that takes a list of natural numbers as input and returns a list only of those that are even and greater than 7.
Filter_even_gt7 (xs: List Nat) : List Nat
Filter_even_gt7 xs = ?
Test_filter_even_gt7a: Equal (Filter_even_gt7 [1n,2n,3n,4n,5n,7n,8n,9n,10n,11n,12n]) [8n,10n,12n]
Test_filter_even_gt7a = ?
Test_filter_even_gt7b : Equal (Filter_even_gt7 [5n, 2n, 6n, 19n, 129n]) []
Test_filter_even_gt7b = ?A small observation, the attentive reader may have noticed that we used a new notation, the n after the numbers. This is a sugar syntax that Kind has. We can write natural numbers by simply adding an n to the number. However, this is a syntax that can end up weighing down Kind. Imagine that the user only wants to add the number 1 to 1000000, it's a simple calculation that Kind can easily handle, but it becomes a bit heavier when using the sugar syntax for natural numbers. The sum will be Plus 1n 1000000n, but Kind will need to check each Nat.succ up to one million and one, in other words, one million and one "Nat.succ" will be computed unnecessarily. This syntax is very useful, but we should use it with care. Ideally, for large numbers, U60.to_nat should be used, which is much lighter for Kind.
Partition
Use Filter to write a Partition function in Kind.
Partition <x> (test: x -> Bool) (xs: List x) : Pair (List x) (List x)
Partition test xs = ?Given a set x, a test function of type x -> Bool, and a List x, the Partition function should return a pair of lists. The first member of the pair is the sublist of the original list containing the elements that satisfy the test, and the second is the sublist containing those that fail the test. The order of the elements in the two sublists should be the same as the original list.
Test_partition1 : Equal (Partition (x => Oddb x) [1n,2n,3n,4n,5n]) (Pair.new [1n,3n,5n] [2n,4n])
Test_partition1 = ?
Test_partition2 : Equal (Partition (x => Bool.false) [5n, 9n, 0n]) (Pair.new [] [5n, 9n, 0n])
Map
Another very useful higher-order function is Map.
Map <x> <y> (f: x -> y) (xs: List x) : List y
Map f List.nil = List.nil
Map f (List.cons head tail) = List.cons (f head) (Map f tail)It takes a function f and a list xs = [n1, n2, n3, ...] and returns the list [f n1, f n2, f n3, ...], where f is applied to each element of xs. For example:
Test_map1 : Equal (Map (x => Plus 3n x) [2n, 0n, 2n]) [5n, 3n, 5n]
Test_map1 = Equal.reflThe types of the elements in the input and output list do not need to be the same, as Map accepts two type arguments, x and y; thus a function of numbers to booleans can be applied to produce a list of booleans:
Test_map2 : Equal (Map (x => Nat.is_odd x) [2n, 1n, 2n, 5n]) [Bool.false, Bool.true, Bool.false, Bool.true]
Test_map2 = Equal.reflIt can even be applied to a list of numbers and a function that returns a list of boolean lists:
Test_map3 = Equal (Map (x => [(Nat.is_even x), (Nat.is_odd x)]) [2n, 1n, 2n, 5n]) [[Bool.true, Bool.false], [Bool.false, Bool.true], [Bool.true, Bool.false], [Bool.false, Bool.true]]
Test_map3 = Equal.reflMap_rev
Let's make things a little more difficult. Show the commutativity of Rev and Map; you may need an auxiliary function:
Map_rev <x> <y> (f: x -> y) (xs: List x) : Equal (Map f (Rev xs)) (Rev (Map f xs))
Map_rev f xs = ?Flat_equal
The Map function maps a List x to a List y using a function of type x -> y. We can define a similar function, Flat_map, that maps a List x to a List y using a function f of type x -> List y. Its definition should work by "flattening" the results of f, like so:
Flat_equal : Equal (Flat_map ( x => ([x , (Plus x 1n), (Plus x 2n)])) [1n, 5n, 10n]) [1n, 2n, 3n, 5n, 6n, 7n, 10n, 11n, 12n]
Flat_equal = Equal.refl
Flat_map <x> <y> (f: x -> List y) (xs: List x) : List y
Flat_map f xs = ?
Test_flat_map1 : Equal (Flat_map (x => [x, x, x]) [1n, 5n, 4n]) [1n, 1n, 1n, 5n, 5n, 5n, 4n, 4n, 4n]
Test_flat_map1 = ?Lists are not the only inductive type for which we can write a Map function. Here's the definition of map for the Maybe type:
Maybe_map <x> <y> (f: x -> y) (a: Maybe x) : Maybe y
Maybe_map f Maybe.none = Maybe.none
Maybe_map f (Maybe.some x) = Maybe.some (f x)Fold
An even more powerful higher-order function is called Fold. This function is the inspiration for the "reduce" operation that is at the heart of Google's map/reduce distributed programming framework.
Fold <x> <y> (f: x -> y -> y) (xs: List x) (a: y) : y
Fold f List.nil a = a
Fold f (List.cons head tail) a = f head (Fold f tail a)
Test_fold1 : Equal (Fold (x => y => (Bool.and x y)) [Bool.true, Bool.true, Bool.false] Bool.false) Bool.false
Test_fold1 = ?
Test_fold2 : Equal (Fold (x => y => (* x y)) [1, 2, 3, 4] 1) 24
Test_fold2 = ?
Test_fold3 : Equal (Fold (x => y => (Concat x y)) [[1], [], [2, 3], [], [4]] [5, 6, 7]) [1, 2, 3, 4, 5, 6, 7]
Test_fold3 = ?Fold_types_different
Note that the type Fold is parameterized by two type variables, x and y, and the parameter f is a binary operator that takes an x and a y and returns a y. Can you think of a situation where it would be useful for x and y to be different?
Functions that build functions
Most of the higher-order functions we've talked about so far use functions as arguments. Let's look at some examples that involve returning functions as results of other functions. To start, here's a function that takes a value x (extracted from some type x) and returns a Nat to x function that returns x every time it's called, ignoring its Nat argument.
Constfun <y> (x: y) : Nat -> y
Constfun x = y => xFtrue : Nat -> Bool
Ftrue = Constfun Bool.trueConstfun_example1 : Equal ((Ftrue) 0n) Bool.true
Constfun_example1 = Equal.reflConstfun_example2 : Equal ((Constfun 5n) 99n) 5n
Constfun_example2 = Equal.reflPlus3 : Nat -> Nat
Plus3 = n => Plus 3n nTest_plus3_1 : Equal ((Plus3) 4n) 7n
Test_plus3_1 = Equal.reflTest_plus3_2 : Equal (Doit3times (Plus3) 0n) 9n
Test_plus3_2 = Equal.reflTest_plus3_3 : Equal (Doit3times (x => Plus 3n x) 0n) 9n
Test_plus3_3 = Equal.refl