Lecture 25: More Pointer Equality

1 Purpose

More on eq?; go over solution to HW8A.

2 Outline

We mentioned last time that these issues of aliasing show up in the same way in any language that supports mutation. For example, here we have translated, essentially word-for-word, all of the examples into Python. While Python supports lambda, since it is a little less common to use it in the way we use it in LSL, we instead define & return local functions, which is more idiomatic.

If you don’t know Python, that’s okay; the point is not to teach you it, the point is just to reinforce that this is not an "LSL problem" or a "Racket problem".

# Example 1
# (define Y 10)
# (define (mk-fn1 Y)
#   (lambda (x) (+ x Y)))
# (define fn1 (mk-fn1 Y))
# (set! Y 20)
# (fn1 0)
Y = 10
def mk_fn1(Y):
  def f(x):
      return x + Y
  return f

fn1 = mk_fn1(Y)

Y = 20
print(fn1(0))

# Example 2
# (define-struct container (val))
# (define Z (make-container 10))
# (define (mk-fn2 Y)
#   (lambda (x) (+ x (container-val Y))))
# (define fn2 (mk-fn2 Z))
# (set-container-val! Z 20)
# (fn2 0)
Z = [10]
def mk_fn2(Y):
  def f(x):
      return x + Y[0]
  return f

fn2 = mk_fn2(Z)

Z[0] = 20
print(fn2(0))


# Example 3
# (define Q (make-container 10))
# (define (mk-fn3 Z)
#   (local [(define P (make-container (container-val Z)))]
#     (lambda (x) (+ x (container-val P)))))
# (define fn3 (mk-fn3 Q))
# (set-container-val! Q 20)
# (fn3 0)
Q = [10]
def mk_fn3(Z):
    P = Z.copy()
    def f(x):
        return x + P[0]
    return f

fn3 = mk_fn3(Q)
Q[0] = 20
print(fn3(0))


# Example 4
# (define Q1 (make-container 10))
# (define (mk-fn4 Z)
#   (lambda (x)
#     (local [(define P (make-container (container-val Z)))]
#       (+ x (container-val P)))))
# (define fn4 (mk-fn4 Q1))
# (set-container-val! Q1 20)
# (fn4 0)
Q1 = [10]
def mk_fn4(Z):
    def f(x):
        P = Z.copy()
        return x + P[0]
    return f
fn4 = mk_fn4(Q1)
Q1[0] = 20
print(fn4(0))

# Example 5
# (define Q2 (make-container 10))
# (define (mk-fn5 Z)
#   (local [(define P Z)]
#      (lambda (x)
#        (+ x (container-val P)))))
# (define fn5 (mk-fn5 Q2))
# (set-container-val! Q2 20)
# (fn5 0)
Q2 = [10]
def mk_fn5(Z):
    P = Z
    def f(x):
        return x + P[0]
    return f
fn5 = mk_fn5(Q2)
Q2[0] = 20
print(fn5(0))

A reference solution to HW8A

In class, we showed how to solve HW8A, reviewing the lessons it provided.

Using eq? to specify behavior

One of the key logical forms of reasoning about programs involving mutable state relies upon the notion of exclusive ownership or separation. There is a system of reasoning called Separation Logic that is used to prove properties of programs that use mutable state, and the simpler notion of exclusive ownership is built into the type system of the language Rust. We can capture some aspects of these kind of reasoning systems using contracts that involve eq?.

For example, consider the following program, which swaps the contents of two cells, returning nothing (here, by convention, we’ll return #f if there is no value we want to return).

(define-struct cell [value])

(: swap (-> (Tuple (Cell Any) (Cell Any)) False))

(define (swap cs)   (let* ([c1 (first cs)]          [c2 (second cs)]          [v1 (cell-value c1)])     (begin (set-cell-value! c1 (cell-value c2))            (set-cell-value! c2 v1)            #f)))

One thing we should wonder about is: what happens if both of the arguments are the same Cell? Does the code still work? Should we allow that?

If we wanted to rule that out, we could easily do that by creating a contract that ensured that only different Cells were passed in, using eq? to distinguish:

(: disjoint? (-> (List Cell~) Boolean))

(define (disjoint? loc)   (cond [(empty? loc) #t]         [(cons? loc) (and (andmap (lambda (oc) (not (eq? oc (first loc)))) (rest loc))                           (disjoint? (rest loc)))]))

Then we could modify the contract of swap to be:

(: swap (-> (AllOf (Tuple Cell~ Cell~) disjoint?) False))

In this case, if they overlap the code will still work; it will do two pointless mutations of the same value. But in other cases, aliasing can cause correct code to become wrong.

For example, consider the following function, which is supposed to run in a loop, incrementing the first value until it is greater than the second:

(: f (-> (Cell Natural) (Cell Natural) False))

(define (f x y)   (if (<= (cell-value x) (cell-value y))       (begin (set-cell-value! x (add1 (cell-value x)))              (f x y))       #f))

This works fine most of the time:

> (define x (make-cell 0))

> (define y (make-cell 4))

> (f x (make-cell 10))

#f

> x

(make-cell 11)

> (f y (make-cell 10))

#f

> y

(make-cell 11)

But what happens if we call it as (f x x)?

Exercise: fix the contract for f so that such a call is ruled out.

(define-contract (NotEq v)   (lambda (x) (not (eq? x v))))

(: f (Function (arguments [a (Cell Natural)]                           [b (AllOf (Cell Natural)                                     (NotEq a))])                (result False)))

(define (f x y)   (if (<= (cell-value x) (cell-value y))       (begin (set-cell-value! x (add1 (cell-value x)))              (f x y))       #f))