Lecture 15: 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:.../syntax/compile.rkt:194:7> 100) name:       check-contract location:   eval:7:0 discovered a counterexample   counterexample: (my-filter-wrong #<procedure:generated> '(∀X₁ ∀X₁))   error:     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:16:3 -------------------- 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.