Lecture 16: Polymorphism II🔗

1 Purpose🔗

More detail / practice with polymorphism

2 Outline🔗

Last time we went over how All worked. Today we want to talk about how Exists works.

3 Existentials🔗

That covers LSL’s All construct, which allows you to write contracts that ensure that functions use arguments opaquely: this ensures that code can be used for many different purposes, as it won’t (inadvertantly) depend on specific details of particular types. There is a deep connection between All (and the analog in typed languages, parametric polymorphism a.k.a. generics) and forall from first-order logic.

Next we’ll explore another form of polymorphism: existentials. Again, there is a deep connection between this progamming language concept and the exists operator from first order logic. Here, the main idea is information hiding: taking concrete details and hiding them so that clients can use them without knowing the details.

The operator in LSL is Exists, and the simplest example is, indeed, very simple:

(: x (Exists (A) A))

(define x 10)

What this states, precisely, is that x has some type (there exists a type A), but what exact type it is, we are not allowed to know. Why this ensures information hiding is that if we try to use x in any way, we get a similar error to when we try to use arguments to functions that use All to abstract the values:

(equal? x 10)

equal?: contract violation

expected: non-parametric?

given: ∃A₀

in: the 1st argument of

(-> non-parametric? non-parametric? any)

contract from:

<pkgs>/lsl-lib/private/library/equal.rkt

blaming: program

(assuming the contract is correct)

at: <pkgs>/lsl-lib/private/library/equal.rkt:16:3

Now, this use of Exists is pointless: we’ve made x abstract, such that it can never be used again. Rather than just hiding a value, however, how this mechanism is actually used is to have an abstract value and some limited operations that you can do to it. i.e., to "package" a value up with operations, such that those operations are the only way to interact with it: any previous knowledge of what type the value was, and correspondingly how to interact with it, is hidden.

For example, if we paired x above with a way of converting to a String, it is no longer useless:

(: x1 (Exists (A) (Tuple A (-> A String))))

(define x1 (list 10 number->string))

As we can now do:

> ((second x1) (first x1))

"10"

Now why might we want to do this? Well, if we look at the type of x1, we note that we can give that exact same type to an existential package (how these values + operations are often called) that uses a different value, and indeed, a different type:

(: x2 (Exists (A) (Tuple A (-> A String))))

(define x2 (list "blah" identity))

> ((second x2) (first x2))

"blah"

Or:

(: x3 (Exists (A) (Tuple A (-> A String))))

(define x3 (list #t (lambda (b) (if b "#t" "#f"))))

> ((second x3) (first x3))

"#t"

If you are familiar with languages like Java, this hopefully starts to ring bells: what we have is the technique that underlies interfaces (one of the most important, if not the most important, ideas when programming in Java). Our contract (Exists (A) (Tuple A (-> A String))) is an interface for values that can be turned into strings. They may or may not currently be strings, but that doesn’t matter: they all essentially have a toString method.

We don’t actually have to include a value: we can include one (or more) functions that create the value (like a constructor), and others that work on it. For example:

(: counter-pkg (Exists (A) (Tuple (-> A) (-> A A) (-> A Integer))))

(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 (make-counter)))

1

Here we define a package that has three "fields" (we’re using fixed size lists here, for ease, but structs would work equally and would make pulling the fields out easier). One makes a new counter (of abstract type A), one increments it by 1, and one turns it into an integer. In this case, we implement the counter using integers, but we could equally do it with lists:

(: counter-pkg1 (Exists (A) (Tuple (-> A) (-> A A) (-> A Integer))))

(define counter-pkg1     (list (λ () empty)           (λ (x) (cons 0 x))           (λ (x) (length x))))

(define make-counter (first counter-pkg1))

(define counter-incr (second counter-pkg1))

(define counter-get (third counter-pkg1))

(counter-get (counter-incr (make-counter)))

1

As with our toString example above, the type hasn’t changed: just the values used to implement it. What this means is that any code that used the counter does not know how it is implemented, which has really important software engineering consequences. It means that if you decided to change how to implement the internals, provided you don’t change the interface, you are guaranteed that no code that uses the interface will break. This is because there is no way for code using the interface to have depended on the internals.

Concretely, this means that if you were using the first counter and switched to the second, you know there is no code that could have "cheated" by using the fact that the counters were actually integers and circumvented the increment operation.

Why would this be useful? Well, rather than swapping out for a list (which is a bit silly), what if you wanted to make it so that the increment operation logged every time it was called? You could easy change the implementation from (λ (x) (+ x 1)) to (λ (x) (begin (log-increment x) (+ x 1))); since the counter is abstract, the only way it gets incremented is via calling this function, so you know your log is complete. If instead you just exposed that it was an integer, some clients might just decide to add themselves, and never call your function, so your log would be incomplete.

How does this all work? Well, it turns out that Exists work identically, but in reverse order, to All. If you remember we talked about polarity: how positions within the All are either negative (inputs to functions) or positive (outputs) and how that gets reversed for function arguments, it turns out that Exists starts reversed. So the outputs of functions inside of an Exists (which have positive polarity) get wrapped, and the inputs (which have negative polarity) get unwrapped.

We didn’t talk about arguments not in a function at all for All, because it’s not actually helpful, but if you extrapolate backwards: functions reverse polarity, so if the function inside All has negative inputs and positive outputs, then the entire function should be in a positive position, which would mean that it gets unwrapped. That’s not useful, i.e., writing:

(: not-useful (All (X) X)) (define not-useful 10) not-useful

not-useful: contract violation

expected: ∀X₆

given: 10

blaming: program (as server)

Just fails, because it tries to unwrap 10, but nothing ever wrapped it.

Since Exists is opposite, at the top level, which is positive, it wraps, which is what we saw with our very first example.

Just like All, the direction of wrapping and unwrapping flips when going into functions. So in our toString example, the input is negative, which for Exists, means it unwraps.

This also explains how our counter works: the constructor (the first field) return type is in a positive position, so for an Exists, it wraps its argument with A. The increment field unwraps on negative input, wraps on positive output, and get unwraps on its negative input.