6.S050 Problem Set 6: State, Data Representation, and Modularity

\[ \newcommand{\target}[2]{\class{mathjax-symbol mathjax-symbol-#1}{#2}} \newcommand{\type}[3]{#1 \target{type}{\vdash} #2 \target{type}{:} #3} \newcommand{\abs}[3]{\target{abs}{\lambda} #1 \target{abs}{:} #2\target{abs}{.} #3} \newcommand{\tabs}[2]{\target{tabs}{\Lambda} #1 \target{tabs}{.} #2} \newcommand{\arrow}{\target{arrowT}{\rightarrow}} \newcommand{\subt}{\target{subT}{<:}} \newcommand{\Int}{\mathsf{Int}} \newcommand{\Bool}{\mathsf{Bool}} \newcommand{\lett}[3]{\mathsf{let}\ \mathit{#1} : #2 = #3\ \mathsf{in}} \newcommand{\letu}[2]{\mathsf{let}\ \mathit{#1} = #2\ \mathsf{in}\ } \newcommand{\ite}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} \DeclareMathOperator{\proj}{.} \newcommand{\object}[1]{\mathsf{object}\ #1\ \mathsf{end}} \newcommand{\call}[2]{#1 \# \mathit{#2}} \newcommand{\method}[2]{\mathsf{method}\ \mathit{#1} = #2} \newcommand{\self}{\mathit{self}} \newcommand{\super}{\mathit{super}} \newcommand{\refc}{\mathsf{ref}\ } \newcommand{\inherit}[2]{\mathsf{inherit}\ #1\ \mathsf{as}\ \mathit{#2}} \newcommand{\pack}[3]{\mathsf{pack}\ (#1, #2)\ \mathsf{as}\ #3} \newcommand{\unpack}[4]{\mathsf{unpack}\ (#1, #2) = #3\ \mathsf{in}\ #4} \newcommand{\override}{\ \mathsf{override}\ } \newcommand{\loc}[1]{l_{#1}} \]

Typing relation. Usually written \(\type{\Gamma}{e}{\tau}\), where \(\Gamma\) is a map from identifiers to types, \(e\) is an expression, and \(\tau\) is a type.

\(\type{\mathrm{Type Context}}{\mathrm{Expression}}{\mathrm{Type}}\)

Anonymous function.

\(\abs{\mathrm{Parameter Name}}{\mathrm{Parameter Type}}{\mathrm{Body}}\)

Type abstraction.

\(\tabs{\mathrm{Type Variable}}{\mathrm{Body}}\)

Function type.

\(\mathrm{Parameter Type} \arrow \mathrm{Return Type}\)

Subtyping relation.

Read \(\tau \subt \tau'\) as: \(\tau\) is a subtype of \(\tau'\). If \(\tau\) and \(\tau'\) are records, \(\tau\) has a superset of the fields in \(\tau'\). Alternatively, anything that expects a \(\tau'\) can take a \(\tau\).

1. Peer Feedback on Problem Set 5 (20 points)

Respond to the following prompts about your peer's submission and post your response as a comment on Canvas. You can find your response to review on the right column of the assignment.

  1. Briefly explain what program properties the proposed type system is tracking.
  2. Pick one aspect of their formalism that you think is particularly clear or elegant, and explain why.
  3. Pick one aspect of their formalism that you found confusing or verbose, and suggest an improvement. Feel free to share what you chose to do in your formalism.

2. State (36 points)

2.1. Building Data Structures with Ref Cells (12 points)

The following program simulates ref cells in TypeScript. It tries to use ref cells and functions to implement arrays. (TypeScript already has arrays, but we want to show that a language that only has ref cells is still powerful enough to implement complex data structures.)

class Ref<T> {
    private value : T;
    constructor(value: T) { this.value = value; }
    get(): T { return this.value; }
    set(value: T): void { this.value = value; }
}

type FunArray = Ref<(i: number) => number>;

function mk_array() : FunArray {
    return new Ref(function (i : number) { return 0; });
}

function lookup(a : FunArray, i : number) : number {
    return a.get()(i);
}

function update(a : FunArray, i : number, v : number) : void {
    a.set((j : number) => { return j === i ? v : lookup(a, j); });
}

The functions follow this specification:

  • mk_array creates an array that is initialized to 0.
  • lookup a i returns the ith element of a.
  • update a i x sets the ith element of a to x.

Unfortunately, this implementation is incorrect. Your job is to fix it!

  1. Write a test that exercises all three functions.
  2. Explain why the current program is incorrect.
  3. Give a correct version of the program.

Turn in your code in a file called ref_array.ts. Include your explanation in a comment at the top of the file. When your code is executed, it should run your test function.

2.2. Purity & Reasoning about Side effects (24 points)

When writing a compiler (or other language processing system) we often want to transform programs in ways that preserve their behavior. Many transformations that are correct for pure programs (programs that do not use mutable state) are not correct for impure programs. For each of the following transformations, indicate whether it is (1) correct for pure programs and (2) correct for impure programs. For the incorrect transformations, give a program that changes behavior when the transformation is applied.

  1. (fun x -> x + e2) e1 to e1 + e2 (where x is not free in e1 or e2)
  2. (fun x -> e1 + x) e2 to e1 + e2 (where x is not free in e1 or e2)
  3. if true then e1 else e2 to e1
  4. if e1 then e2 else e2 to e2
  5. if (if e1 then e2 else e3) then e4 else e5 to if e1 then (if e2 then e4 else e5) else (if e3 then e4 else e5)
  6. e1 (if e2 then e3 else e4) to if e2 then e1 e3 else e1 e4

You can make the following assumptions:

  • Binary operators are evaluated from left to right.
  • We are using call-by-value, which means that an application e1 e2 evaluates e1 first, then evaluates e2, then performs the function call.
  • None of the expressions produce errors or fail to terminate.

3. Modularity (44 points)

3.1. Objects as Records of Functions with self (24 points)

  1. In lecture, we modeled objects as a record of functions where each function takes a self parameter. This model is sufficient to describe classes, inheritance, and open recursion. In class, we introduced objects on their own; in this problem, we'll be mixing objects and references.

    The syntax of references is as follows:

    • Creation: \(\refc e\)
    • Read: \(!e\)
    • Write: \(e := e\)

    Here's an example of a counter class (i.e. it's a function that creates counter objects):

    \begin{align*} &\mathit{Counter} = \lambda c. \\ &\quad\letu{ctr}{\refc c} \\ &\quad\object{\\ &\quad\quad\method{value}{ctr} \\ &\quad\quad\method{get}{\lambda \self. !(\self \proj \mathit{value})} \\ &\quad\quad\method{incr}{\lambda \self. (\self \proj \mathit{value}) := \call{\self}{get} + 1} \\ &\quad} \end{align*}

    The following class inherits from Counter and adds a set method:

    \begin{align*} &\mathit{SetCounter} = \lambda c. \\ &\quad\object{\\ &\quad\quad\inherit{\mathit{Counter}\ c}{super} \\ &\quad\quad\method{set}{\lambda \self. \lambda v. (\self \proj \mathit{value}) := v} \\ &\quad} \end{align*}

    Write a class AuditCounter that inherits from SetCounter and adds a new method accesses that returns the number of times that the get method has been called. This count should include any calls to get made by incr. Your new class should not redefine any methods other than get (i.e. you should not add a new implementation of incr).

  2. This model of objects lacks some of the encapsulation features that real object systems provide. Show that our Counter object is not encapsulated by writing a program that accesses the count without calling get.
  3. Write a new class HiddenCounter that only allows the count to be accessed by calling get.
  4. Can you write a HiddenSetCounter class that inherits from HiddenCounter without modifying HiddenCounter? Why or why not?

3.2. Existential Types (20 points)

The following function constructs a set implementation given an equality function. It works for any type, and it hides the implementation of the set from its consumers.

\begin{align*} \mathit{mkSet} : \forall \alpha. (\alpha \rightarrow \alpha \rightarrow \Bool) \rightarrow \exists \sigma. \{ \mathit{empty} : \sigma, \mathit{add} : \sigma \rightarrow \alpha \rightarrow \sigma, \mathit{contains} : \sigma \rightarrow \alpha \rightarrow \Bool \} \end{align*}
  1. Give an implementation of this type using the notation we defined in lecture. Your implementation should be correct (i.e. the methods should correspond to a mathematical set), not just match the type.

    Hint: Look at problem 2.2 for inspiration. You don't need ref cells, but the use of functions in 2.2 should be instructive.

  2. Write a program that exercises the three set methods.

Last updated: 2023-05-09 Tue 20:05