Lecture 15: Specifications with Functions
1 Purpose
Functions as Data
2 Outline
Up until now, all the functions we’ve written have had non-function values as arguments. But we’ve seen the syntax for defining function contracts countless times! It’s the contract that we give to functions, and can be used for arguments, not just top-level functions. As a simple example:
(: myfun (-> (-> Integer Integer) Integer Integer)) (define (myfun f x) (f (f x))) (: myfun-prop (-> (-> Integer Integer) True)) (define (myfun-prop f) (equal? (myfun f 0) (f (f 0)))) (check-contract myfun-prop 1) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
Here we aren’t going anything particularly interesting, but myfun-prop takes an arbitrary (-> Integer Integer) function as an argument, and checks that passing it (and 0) to myfun is the same as calling it twice on 0 (which happens to be exactly what myfun does).
Now, that is a simple example, but what it points to is being able to specify, from the outside, the behavior of code that takes functions as input. Especially in more complex examples, such functions are quite common. Indeed, even pretty simple list abstractions like map and filter have exactly this phenomena. If we want to be able to specify the behavior of map, we need to be able to talk about arbitrary functions.
What is an arbitrary function? How could we possibly generate it? Well, there are interesting research questions related to this (see a recent paper with a Khoury alum as a co-author: https://dl.acm.org/doi/10.1145/3632919), but a simple answer can be arrived at by using our normal random generation on the output of the functions. e.g., if my goal is an (-> Integer Integer), I could create something like that with:
(lambda (x) (contract-generate Integer)) #<procedure:...te/library/core.rkt:106:2>
Now, this alone isn’t ideal, because it means our functions, when called multiple times on the same input, produce different output. Maybe we want that, but most likely, if we are trying to create arbitrary functions, we want them to be have as functions: i.e., the same input produces the same output, even if that output is arbitrary. We can do that by remembering which output we generated for which input, and always returning the same value when called again (this is actually a general optimization technique called memoization, related to dynamic programming you may have heard of!).
This is how our generator for functions works.
Let’s practice by creating properties that capture how map should work:
(: map-prop1 (-> (List Integer) (-> Integer Integer) True)) (define (map-prop1 l f) (equal? (length l) (length (map f l)))) (check-contract map-prop1) (: map-prop2 (-> (List Integer) (-> Integer Integer) True)) (define (map-prop2 l f) (if (empty? l) #t (equal? (f (first l)) (first (map f l))))) (check-contract map-prop2) (: map-prop3 (-> Integer (List Integer) (-> Integer Integer) True)) (define (map-prop3 n l f) (equal? (map f (cons n l)) (cons (f n) (map f l)))) (check-contract map-prop3) (: map-prop4 (-> (List Integer) True)) (define (map-prop4 l) (equal? (map (lambda (_) 0) l) (build-list (length l) (lambda (_) 0)))) (check-contract map-prop4) (: map-prop5 (-> (List Integer) (List Integer) (-> Integer Integer) True)) (define (map-prop5 l1 l2 f) (equal? (map f (append l1 l2)) (append (map f l1) (map f l2)))) (check-contract map-prop5) (: map-prop6 (-> (List Integer) (-> Integer Integer) (-> Integer Integer) True)) (define (map-prop6 l f g) (equal? (map g (map f l)) (map (lambda (x) (g (f x))) l))) (check-contract map-prop6) 6 success(es) 0 failure(s) 0 error(s) 6 test(s) run
Question: are there some properties that imply others? Are there a subset that completely define map?
We can write similar properties about filter:
(: filter-prop1 (-> Integer (List Integer) (-> Integer Boolean) True)) (define (filter-prop1 n l f) (if (f n) (equal? (filter f (cons n l)) (cons n (filter f l))) (equal? (filter f (cons n l)) (filter f l)))) (check-contract filter-prop1) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
(: filter-prop2 (-> (List Integer) (-> Integer Boolean) True)) (define (filter-prop2 l f) (>= (length l) (length (filter f l)))) (check-contract filter-prop2) 1 success(es) 0 failure(s) 0 error(s) 1 test(s) run
Exercise: come up with more!
Parametric Signatures
Up until now, all signatures we’ve written have involved concrete types. We have a mechanism in LSL to allow you to write parametric signatures, analogously to how you write parametric contracts, using the keyword All.
The name is suggestive: it is analogous to forall from first order logic. The idea is that a function should work for All contracts that could be substituted in for the given contract variable.
For example, one of the simplest such parametric (or polymorphic) functions we can write is:
(: id (All (X) (-> X X))) (define (id x) x)
This says that the function id, given any types X, should take in an X and produce an X. This is actually a very strong statement: since it is stated for any X, it means, in particular, that id cannot do anything that depends on particularities of the value, since it won’t know what type of value it will get. e.g., it cannot add, compare, etc, because it may be passed a struct, or a string, or a function.
We can see what happens if we try to write such a function:
(: id-fail (All (X) (-> X X))) (define (id-fail x) (+ 1 x)) (id-fail 1) [assert] $+: expected real? arguments
arguments: (∀X₁)
Despite the fact that we call id-fail on a number, attemping to add 1 to the argument in its body fails, since the signature we gave it said that id-fail would treat its argument abstractly. The reason why this is important is we need the code to equally work if we pass such a function a String as an input.
This actually means that, aside from doing pointless computation, or running forever, the only thing that a function with signature (All (X) (-> X X)) can do is return its argument, unchanged. Because not only cannot it not modify its argument, it has no other way of creating an X aside from the one it was passed as an argument.