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 a 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.

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 (Leaf) (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) (Sop Set                                      (-> Elt Set)                                      (-> Set Set Set)                                      (-> Set Set Set)                                      (-> Elt Set Boolean)))

The idea is that we collect all the set operaitons (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 to 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 list

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 an example tree) (define T1-KEYS (list ... its keys))   (define (t1-prop sop) ... define a prop that ensures tree-keys returns elements in T1-KEYS)

I’ve written what we’ll run as a unit test as a function that takes a set implementation computes with it, so we can easily run the same tests with different implementations. The first one we’ll run is:

(check-satisfied SOP-LIST t1-prop)

Exercise 3: Implementing tree-keys, using 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)    ...)

(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, come up with a third implementation – maybe a tree?