Lecture 17: Polymorphism II
1 Purpose
More detail / practice with polymorphism
2 Outline
Last time we went over how All and Exists work. Today we want to talk a little more about how existentials show up in programming languages.
In particular, we want to contrast the difference between the mechanism of data abstraction typically used in object oriented languages with that presented with existential types. Since we are trying to confront this logically, we are using idealized versions of these: real languages actually mix both of these (i.e., the object oriented languages you have used feature both object oriented features and features explainable with existential types). Understanding them well, however, benefits from teasing apart the details.
If we think about how an object works, ignoring classes, inheritance, etc, we are left with the idea of methods being fundamental. In particular, it’s very important for methods to be able to access data internal to the object that is not accessible from outside (as an idealized model, we will assume all data has to go through methods). This is the core idea of object oriented programming, which originated with languages like Smalltalk, as far back as the early 1970s. And a method, really, really just needs to be a function that can close over private data: this is true of functions in nearly all languages (often these are called "closures", if one is being proecise).
We can represent a the idea of objects with methods in LSL as a struct full of functions, where the functions may include, in data they close over, private data.
As an example, here’s an object with a single method: add, that takes an integer and adds it to a private integer it has:
(define-struct adder (add))
(define (make n) (make-adder (lambda (x) (+ n x)))) (define A1 (make 10)) (define A2 (make 20)) ((adder-add A1) 1) 11
((adder-add A2) 3) 23
To make calling the methods easier, I’ll define a few helper functions:
(define (call0 o m) ((m o)))
(define (call1 o m a) ((m o) a))
So I can rewrite the above as:
(call1 A1 adder-add 1) 11
(call1 A2 adder-add 3) 23
Exercise: define an object that contains two methods, add and mul: which add and multiply by a private field, respectively.
(define-struct addmuler (add mul))
(define (make2 n) (make-addmuler (lambda (x) (+ n x)) (lambda (x) (* n x))))
Note how both methods use n, which is not exposed publically. Once you create one of these objects, you can only interact with it via the methods: this is the fundamental idea of object oriented programming.
In particular, if we create:
(define A3 (make2 10))
There is no way of distinguishing A1 and A3.
As a more complicated example, which also lets us start talking about interfaces (a key idea!), we could define a square object that had an area and tostring method as follows:
(define-struct shape (area tostring))
Let’s define the signature for a Shape~:
(define-contract Shape~ (Shape (-> Real) (-> String)))
So now we can define our first Shape~ constructor:
(: square (-> Real Shape~))
(define (square sidelen) (local ((define (square-area) (* sidelen sidelen)) (define (square-tostring) (string-append "square(" (number->string sidelen) ")"))) (make-shape square-area square-tostring)))
Note what we have done: defined a struct to hold the methods area and tostring, and then defined a constructor square as an ordinary function that returns an instance of that struct (a Shape~). The idea of having a struct with a common set of methods is based on the idea that "types", in a pure OO world, arise as the set of methods that an object will respond to.
We can then construct and use their shape methods as follows:
(define SQ1 (square 10)) (define SQ2 (square 20)) (call0 SQ1 shape-area) 100
(call0 SQ2 shape-tostring) "square(20)"
Whats interesting, of course, and this is the fundamental idea with object oriented programming, is that we can define different shapes that still have the same set of methods:
(: circle (-> Real Shape~))
(define (circle radius) (local ((define (circle-area) (* (* radius radius) 3.14)) (define (circle-tostring) (string-append "circle(" (number->string radius) ")"))) (make-shape circle-area circle-tostring)))
Exercise: define a rectangle that takes a width and height.
(: rectangle (-> Real Real Shape~))
(define (rectangle width height) (local ((define (rect-area) (* width height)) (define (rect-tostring) (string-append "rectangle(" (number->string width) ", " (number->string height) ")"))) (make-shape rect-area rect-tostring)))
Now we can construct squares, circles, and rectangles: they all have exactly the same methods, and so we can program against them uniformly.
This therefore provides a form of information hiding, and allows us to treat different types abstractly.
And it works quite well – e.g., I can construct a list of Shape~s, put squares, circles, rectangles in them, and then compute the total area:
(: my-shapes (List Shape~)) (define my-shapes (list (square 10) (circle 5) (square 15) (rectangle 3 4))) (apply + (map (lambda (s) ((shape-area s))) my-shapes)) 415.5
So what does this have to do with existential types? We just managed to do some of what we said our goal was, with not a single Exists in sight.
Well, what if we wanted to add a method equal. We can try to rewrite our code:
(define-struct shape (area tostring equal))
(define (square sidelen) (local ((define (square-area) (* sidelen sidelen)) (define (square-tostring) (string-append "square(" (number->string sidelen) ")")) (define (square-equals other-square) ...)) (make-shape square-area square-tostring square-equals)))
But there is an immediate problem. How do we compare another Shape~? A square should be equal to another square with the same sidelen, but given a Shape~, the only things we have access to are methods, so we can’t get the sidelen, nevermind know if it was make with the square constructor: that information was (deliberately) lost.
Now, we could try to sidestep this, by maybe using the tostring method and comparing that, but now we aren’t comparing against the actual object, we are just comparing the result of calling a single method. Indeed, there is no guarantee that a Shape~ that returns "square(10)" was indeed constructed by calling (square 10) – as it could easily have been the object:
(define bad-obj (make-shape (lambda () 0) (lambda () "square(10)")))
So what do we do? Well, if a pure method based world, the only option is to add more methods that somehow expose enough to make equality work. You can carry this out via a form of double dispatch, but this requires fixing, ahead of time, all the types of shapes that you’ll deal with. e.g., you can have the equal method take, as its input, a set of methods to call, one per type, and then the receiver can decide what to do.
Counters
We’ll come back to how to do this, but let’s first look at another example – our counters from yesterday. We defined them using existentials:
(define-contract (Counter~ A) (Tuple (-> A) (-> A A) (-> A Integer))) (: counter-pkg (Exists (A) (Counter~ A)))
(define counter-pkg (list (λ () 0) (λ (x) (+ x 1)) (λ (x) x))) (define make-counter (first counter-pkg)) (define counter-incr (second counter-pkg)) (define counter-get (third counter-pkg)) (counter-get (counter-incr (counter-incr (make-counter)))) 2
With mutable state (a preview: we’ll come back to this), we can define this with the pure method approach as well:
(define-struct counter (incr get)) (define-contract Counter~ (Counter (-> True) (-> Integer)))
(define (make-c) (let ([n 0]) (make-counter (lambda () (begin (set! n (add1 n)) #t)) (lambda () n))))
But I might want to add a merge operation: combine the counts of two separate counters. Like equal, this similarly requires us to poke at the internals of the counter. How could we do it with the pure method approach? What would we have to do? As an exercise, do that! Add a merge method.
Probably the easiest is to use get on the other object:
(define (call0 o m) ((m o)))
(define (call1 o m a) ((m o) a)) (define-struct counter (incr get merge)) (define-contract Counter~ (Counter (-> True) (-> Integer) (-> Counter~ True)))
(define (make-c) (let ([n 0]) (make-counter (lambda () (begin (set! n (add1 n)) #t)) (lambda () n) (lambda (m) (let ([o (call0 m counter-get)]) (begin (set! n (+ n o)) #t))))))
We can then use this as follows:
(define C1 (make-c)) (define C2 (make-c)) (call0 C1 counter-incr) #t
(call0 C1 counter-incr) #t
(call0 C2 counter-incr) #t
(call1 C1 counter-merge C2) #t
(call0 C1 counter-get) 3
But there is an issue with that – if our internal representation were not an integer, it might make this merge operation very expensive. Indeed, if we switched to lists:
(define (call0 o m) ((m o)))
(define (call1 o m a) ((m o) a)) (define-struct counter (incr get merge)) (define-contract Counter~ (Counter (-> True) (-> Integer) (-> Counter~ True)))
(define (make-c) (let ([l empty]) (make-counter (lambda () (begin (set! l (cons l n)) #t)) (lambda () (length l)) (lambda (m) (let ([o (call0 m counter-get)]) (begin (set! l (append l (build-list o (lambda (x) 1)))) #t))))))
Then we not only have to call length to get, but we then have to reconstruct a whole new list.
With the existential implementation, on the other hand, we can just directly combine them, since the private data is exposed within the implementations:
(define-contract (Counter~ A) (Tuple (-> A) (-> A A) (-> A A A) (-> A Integer))) (: counter-pkg (Exists (A) (Counter~ A)))
(define counter-pkg (list (λ () empty) (λ (x) (cons 1 x)) (λ (x y) (append x y)) (λ (x) (length x)))) (define make-counter (first counter-pkg)) (define counter-incr (second counter-pkg)) (define counter-merge (third counter-pkg)) (define counter-get (fourth counter-pkg)) (define C1 (counter-incr (counter-incr (make-counter)))) (define C2 (counter-incr (make-counter))) (counter-get (counter-merge C1 C2)) 3
There is a downside to this, of course: we cannot merge incompatible counters. If we needed to do this, we essentially need the flexibility that the method approach enforces.
If we return to the question of equality, we can see that comparing the same objects is quite easy with existentials:
(define-struct shape (v area tostring equal))
(define-contract (Shape~ A) (Shape A (-> Real) (-> String) (-> A Boolean))) (: square (Exists (A) (-> Real (Shape~ A))))
(define (square sidelen) (local ((define (square-area) (* sidelen sidelen)) (define (square-tostring) (string-append "square(" (number->string sidelen) ")")) (define (square-equal? s) (= s sidelen))) (make-shape sidelen square-area square-tostring square-equal?))) (: rectangle (Exists (A) (-> Real Real (Shape~ A))))
(define (rectangle width height) (local ((define (rect-area) (* width height)) (define (rect-tostring) (string-append "rectangle(" (number->string width) ", " (number->string height) ")")) (define (rect-equal? s) (and (= (first s) width) (= (second s) height)))) (make-shape (list width height) rect-area rect-tostring rect-equal?)))
Here we’ve changed one thing: we now have an actual field for the "fields" (or private data) of the object, which in the previous version, we didn’t have. This doesn’t actually expose anything, since it will be wrapped up, but it means that we can specify that what is passed to the equal method should be private data of the same type. In particular, it had to have been created by the same constructor (square,rectangle, etc).
Now note that we can compare squares for equality:
(define SQ1 (square 10)) (define SQ2 (square 20)) (define SQ3 (square 10)) ((shape-equal SQ1) (shape-v SQ2)) #f
((shape-equal SQ1) (shape-v SQ3)) #t
But if we try to compare a square to a rectangle, we get an error!
(define R1 (rectangle 10 20)) ((shape-equal SQ1) (shape-v R1)) square: contract violation
expected: ∃A₀
given: ∃A₁
blaming: program (as client)
On the other hand, to define equality at all with pure methods, we need to do quite a bit of work. e.g., aside from relying on hacks like tostring, the best option is probably some amount of double dispatch:
(define (call0 o m) ((m o)))
(define (call1 o m a) ((m o) a)) (define-struct shape (area tostring equal compare)) (define-struct equal (square circle rectangle)) (define-contract Equal~ (Equal (-> Real Boolean) (-> Real Boolean) (-> Real Real Boolean)))
(define-contract Shape~ (Shape (-> Real) (-> String) Equal~ (-> Equal~ Boolean)))
(define (square sidelen) (local ((define (square-area) (* sidelen sidelen)) (define (square-tostring) (string-append "square(" (number->string sidelen) ")")) (define square-equal (make-equal (lambda (s) (= s sidelen)) (lambda (r) #f) (lambda (w h) #f))) (define (square-compare other-equals) ((equal-square other-equals) sidelen))) (make-shape square-area square-tostring square-equal square-compare)))
(define (circle radius) (local ((define (circle-area) (* (* radius radius) 3.14)) (define (circle-tostring) (string-append "circle(" (number->string radius) ")")) (define circle-equal (make-equal (lambda (s) #f) (lambda (r) (= r radius)) (lambda (w h) #f))) (define (circle-compare) ((equal-circle) radius))) (make-shape circle-area circle-tostring circle-equal circle-compare)))
(define (rectangle width height) (local ((define (rect-area) (* width height)) (define (rect-tostring) (string-append "rectangle(" (number->string width) ", " (number->string height) ")")) (define rect-equal (make-equal (lambda (s) #f) (lambda (r) #f) (lambda (w h) (and (= w width) (= h height))))) (define (rect-compare) ((equal-rectangle) width height))) (make-shape rect-area rect-tostring rect-equal rect-compare)))
And we can use that to perform comparisons:
(define SQ1 (square 10)) (define SQ2 (square 20)) (define SQ3 (square 10)) (call1 SQ1 shape-compare (shape-equal SQ2)) #f
(call1 SQ1 shape-compare (shape-equal SQ3)) #t
But this is a lot of indirection and overhead, and more importantly, the idea that we have to know all of the shapes we’ll deal with up front is tedious (though, performing some amount of this is what notions like classes, inheritance, etc does behind the scenes).
Exercise Define another implementation of Counter~, not using a number or a list internally, that provides all the methods above.
Exercise Write a function that uses a counter count the number of elements of a list. Now switch which counter you had it use: notice how the code that used the counter did not change.
For a much more thorough presentation of the ideas from todays lecture, see https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf