Lecture 18: Programming Against Interfaces🔗

1 Purpose🔗

Revisit All

2 Outline🔗

The last few days we’ve been learning about All and Exists, two features in LSL that allow us to express information hiding invariants.

Generally, a contract (: some-function (All (X) ...)) will prevent some-function from knowing anything about the X that it is passed, and a contract (: some-value (Exists (X) ...)) will prevent any users of some-value from knowing anything about X. The mechanism is the same, it is the direction of protection that differs.

One of the most compelling uses of these features is they allow you to enforce the software engineering pattern of programming against an interface. While this can certainly be followed without any enforcement mechanism, it is such an important idea that many languages have built in support for enforcing it at the language level.

Lecture today is going to be pretty different: we’re going to run it as effectively one big lab: you follow the exercises described here, getting help from me or other TAs who are in the room.

The task is to design an interface for a Set, program against it, and then see how we can provide multiple implementations that have very different performance characteristics.

A template file is available here:

l18.rkt

3 Lecture Lab🔗

The task that we want to do is to collect a set of all keys from a tree where each node has a key, value, and two descendents:

(define-struct leaf [])

(define-struct node [k v l r])

(define-contract (Tree K V)   (OneOf (Struct leaf [])          (Struct node [K V (Tree K V) (Tree K V)])))

We’ll define the operations that a set should have as follows:

(define-struct sop [empty singleton union intersect member?])

(define-contract (Sop Set Elt)   (Struct sop [Set                (-> Elt Set)                (-> Set Set Set)                (-> Set Set Set)                (-> Elt Set Boolean)]))

The idea is that we collect all the set operations (Sop) into a struct, so its easy to carry them around.

We then want to implement a function that has this signature:

(: tree-keys (All (Set V)                   (-> (Sop Set String)                       (Tree String V)                       Set)))

i.e., for any type of Set, and any values in the tree, we take the interface for working with that set and the tree, and we will return a set.

In order to be able to write tests for code that uses these, we need to define an instance of Sop.

Exercise 1: Implementing sets as lists

Your first task is to define an instance of Sop where the set is represented as a list of strings, i.e., (Sop (List String) String):

(define SOP-LIST ...)

Answer:

(define SOP-LIST (make-sop empty                            (lambda (e) (list e))                            append                            (lambda (l1 l2)                              (filter (lambda (e1) (member? e1 l2)) l1))                            member?))

Exercise 2: Writing a test

Now you can write a unit test for tree-keys that passes our SOP-LIST as the concrete implementation; tree-keys won’t know this is the implementation, and we’ll later test it on others, but let’s start here.

(define T1 ...)   (define T1-KEYS (list ...))     (define (t1-prop sop) ...)

t1-prop can be thought of as a unit test that is parametric in the particular set implementation that it will use; since it is a function that takes in a set implementation that it then uses, we can easily run the same test with different implementations. We will see how we can use it to test a particular implementation in Exercise 3.

Exercise 3: Implementing tree-keys, using the set interface

Now let’s go and implement tree-keys. The key here, of course, is that despite the fact that our only set implementation, so far, is a list, we cannot use that fact within tree-keys: our signature rules that out. We must only use the operations provided by Sop.

(define (tree-keys sop t)    ...)

Now we can use t1-prop to test tree-keys on our SOP-LIST set implementation:

(check-satisfied SOP-LIST t1-prop)

And see that our code works.

Exercise 4: Implementing sets as characteristic functions

Now, let’s define a different set implementation; this time, using the idea of characteristic functions: that is, a set of T for some T is a function (-> T Boolean) that return #t for all elements in the set and #f otherwise.

(define SOP-FUN ...)

Now we can again run our same test against this new implementation:

(check-satisfied SOP-FUN t1-prop)

Challenge: If you finished early, come up with a third implementation – maybe a tree?