Lecture 16: Polymorphism

1 Purpose

Learn about parametric polymorphic contracts

2 Outline

While we’ve been able to write contracts for parametric data, e.g.,

(define-struct leaf [value])

(define-struct node [left right])

(define-contract (Tree X) (OneOf (Leaf X) (Node (Tree X) (Tree X))))

Up until last time, when we’ve used these contracts in function signatures, we’ve had to make them concrete. e.g., (Tree Integer) or (Tree String).

Last time, we introduced the mechanism by LSL to allow you to write parametric signatures using the keyword All.

This allows us to give accurate signatures to functions that process data structures that are themselves parametric.

For example, since Lists can have any type inside, when we go to write a generic function that works on any list, we would rather not write the signature saying it only works for, e.g. (List Integer) or (List String).

Can you think of some list functions like that?

For example, if you want to give a signature to length, it would have signature:

(: length (All (X) (-> (List X) Natural)))

Or, the list abstractions that we use.

Now note what happens if we write my-filter with a bug. Maybe we forget to use pred?, and think we are dealing with numbers, and try to just compare against 0:

(: my-filter-wrong (All (X) (-> (-> X Boolean) (List X) (List X)))) (define (my-filter-wrong pred? lst)   (cond [(empty? lst) lst]         [(cons? lst) (if (equal? (first lst) 0)                          (cons (first lst) (my-filter-wrong pred? (rest lst)))                          (my-filter-wrong pred? (rest lst)))])) (check-contract my-filter-wrong)

-------------------- interaction-area tests > Unnamed test FAILURE params:     '(#<procedure:...yntax/interface.rkt:83:7> 100) name:       check-contract location:   eval:7:0 discovered a counterexample   counterexample: (my-filter-wrong #<procedure:generated> '(∀X₁))   error:     [assert] equal?: contract violation       expected: non-parametric?       given: ∀X₁       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:18:10 -------------------- 0 success(es) 1 failure(s) 0 error(s) 1 test(s) run

Note how equal? fails because we try to call it on an abstract value.

How would we write map? Unlike with previous examples, to write the signature for map, we should use two variables:

(: map (All (X Y) (-> (-> X Y) (List X) (List Y))))

This is actually quite important. We could give map a signature with only one variable:

(: mymap (All (X) (-> (-> X X) (List X) (List X))))

(define (mymap f l)   (cond [(empty? l) empty]         [(cons? l) (cons (f (first l)) (mymap f (rest l)))]))

But, while this doesn’t error if the code is correct (due to how the abstract contracts work: more on this in a minute), it doesn’t rule out an implementation that doesn’t call the function at all:

(: mymap-buggy (All (X) (-> (-> X X) (List X) (List X))))

(define (mymap-buggy f l)   (cond [(empty? l) empty]         [(cons? l) (cons (first l) (mymap-buggy f (rest l)))]))

Note that:

> (mymap number->string '(1 2 3))

'("1" "2" "3")

Why? Well, technically, the way that All works involves the idea of negative and positive positions of arguments. This same idea appears in subtyping in languages like Java. The idea is that a negative position is an input, and so All (X) will wrap a seal around arguments that involve the polymorphic variable X. In this case, the two negative positions are (-> X X) and (List X). For (List X), this means that all elements of the list get wrapped up; this is why in errors you don’t see normal values, but instead special sealed ones: the actual value has been wrapped up.

(-> X X) is special – we’ll come back to that in a second.

In a positive position, which are essentially outputs, All (X) will unwrap the values. So in this case, the (List X) in the output means that all elements of the list will have the X seal removed from them. If they don’t have an X seal, you will get an error.

This is why the following function causes an error:

(: id-error (All (X) (-> X X))) (define (id-error x) 1) (id-error 1)

id-error: contract violation

expected: ∀X₄

given: 1

blaming: program (as server)

Now: why do we bother with this negative/positive stuff when we could just say inputs and outputs? Well, for function arguments (a.k.a. higher order arguments), we switch the polarity: negative becomes positive and positive becomes negative.

What that means is that for the argument (-> X X) that is in a negative position, its input has positive polarity, so it unwraps, and its output has negative polarity, so it wraps (this is also often how subtyping works!).

This turns out to be exactly what we want: if we go back to our example:

> (mymap number->string '(1 2 3))

'("1" "2" "3")

We can see what happens: '(1 2 3) is in a negative position, so each element is wrapped in an X seal. Then when number->string is called, the input is unwrapped: the X seal is removed (since its a positive position), so number->string can run as normal, and then on the output (e.g., "1" etc), the X seal is added back (since it is a negative position). Now the entire resulting list '("1" "2" "3") (but all wrapped in X seals) is returned, and since the return type is (List X), in a positive position, all the seals are removed and we get back the expected output.

Now, if we do the same thing with:

> (map number->string '(1 2 3))

'("1" "2" "3")

Which has the right signature, with All (X Y), the only difference is that when number->string returns, values are wrapped with Y, and the entire resulting list '("1" "2" "3") then has the Y seals removed: all works out.

If we instead investigate:

(: mymap-catch-bug (All (X Y) (-> (-> X Y) (List X) (List Y))))

(define (mymap-catch-bug f l)   (cond [(empty? l) empty]         [(cons? l) (cons (first l) (mymap-catch-bug f (rest l)))]))

(mymap-catch-bug number->string '(1 2 3))

mymap-catch-bug: contract violation

expected: ∀Y₆

given: ∀X₅

blaming: program (as server)

What happens is that the input list '(1 2 3) is wrapped with X; the function is never called, which means we try to return a list where all the elements are wrapped with X. Since the output is (List Y), we try to remove Y seals from the elements: but we don’t have elements that are wrapped with Y, so an error occurs. This is why we should give this more accurate signature to the function.

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:18:10

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)

eval:44:0: begin (possibly implicit): the last form is not

an expression

at: (define not-useful 10)

in: (begin (: not-useful (All (X) X)) (define not-useful

10))

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.