29  Review: Higher-Order Functions and Static Checking

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferrule}[3][]{ \let\and\qquad \begin{array}{@{}l@{}} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Instructions

This assignment is a review exercise in preparation for a subsequent assessment activity.

This is a peer-quizzing activity with two students. Each section has an even number of exercises. Student A quizzes Student B on the odd numbered exercises, and Student B quizzes Student A on the even numbered exercises.

To the best of your ability, give feedback using the learning-levels rubric below on where your peer is in reaching or exceeding Proficient (P) on each question live. Guidance of what a Proficient (P) answer looks like are given.

There may or may not be a member of the course staff assigned to your slot. It is expected that regardless of whether a member of the course staff is present, this is a peer-quizzing activity. If a member of the course staff is present, you may ask for their help and guidance on answering the questions and/or their assessment of where you are at in your learning level.

It is not expected that you can complete all exercises in the allotted time. You and your partner may pick and choose which sections you want to focus on and use the remaining questions as a study guide. You and your partner may, of course, continue working together after the scheduled session.

At the same time, most questions can be answered in a few minutes with a Proficient (P) level of understanding. Aim for 3–4 sections in 30 minutes.

Your submission for this session is an overall assessment of where your partner is in their reaching-or-exceeding-proficiency level. Be constructive and honest. Neither your nor your partners grade will depend on your learning-level assessment. Instead, your score for this assignment will be based on the thoughtfulness of your feedback to your partner.

Submit on Gradescope as a pair. That is, use Gradescope’s group assignment feature to submit as a group. The submission form has a spot for each of you to provide your assessment and feedback for each other.

Please proactively fill slots with an existing sign-up to have a partner. In case your peer does not show up to the slot, try to join another slot happening at the same time from the course calendar. If that fails and a course staff member is present, you may do the exercise with the staff member and get credit. If there is no staff member present, you may try to find a slot at a later time if you like or else write to the Course Manager on Piazza timestamped during the slot.

Learning-Levels Rubric

4 - Exceeding (E)
Student demonstrates synthesis of the underlying concepts. Student can go beyond merely describing the solution to explaining the underlying reasoning and discussing generalizations.
3 - Proficient (P)
Student is able to explain the overall solution and can answer specific questions. While the student is capable of explaining their solution, they may not be able to confidently extend their explanation beyond the immediate context.
2 - Approaching (A)
Student may able to describe the solution but has difficulty answering specific questions about it. Student has difficulty explaining the reasoning behind their solution.
1 - Novice (N)
Student has trouble describing their solution or responding to guidance. Student is unable to offer much explanation of their solution.

29.1 Higher-Order Functions

Exercise 29.1 Suppose you have a very large list of floating-point numbers stored in a parallel sequence, for example, ParSeq(0.1, 12, -500, 76.33, 0, -9.9). Write a function squareRootSum that computes the sum of the square roots of all the positive numbers in this sequence. You can use the scala.math.sqrt function to compute square roots.

import scala.math.sqrt
import $ivy.`org.scala-lang.modules::scala-parallel-collections:1.0.4`, scala.collection.parallel.ParSeq

def squareRootSum(l: ParSeq[Double]): Double = ???
import scala.math.sqrt
import $ivy.$                                                         , scala.collection.parallel.ParSeq
defined function squareRootSum

Note that ParSeq is an abstract data type that has the same higher-order iteration methods as List.

A Proficient (P) answer will recall the higher-order functions filter, map, and one of foldLeft, foldRight or reduce, and use them to filter only positive numbers, compute the square root, and sum the list elements respectively.

def squareRootSum(l: ParSeq[Double]): Double = 
  l filter {_ > 0} map {sqrt} reduce {_ + _}
defined function squareRootSum

Exercise 29.2 Consider the following Scala expression. Can you figure out its type?

List(1,2,2,3,3,3,4,4,4,4).foldRight[(List[Int], List[List[Int]])]((Nil, Nil)) {
  (h, acc) => acc match {
    case (Nil, pacc) => (h :: Nil, pacc)
    case (lacc @ (p :: _), pacc) =>
      if (h == p) (h :: lacc, pacc) else (h :: Nil, lacc :: pacc)
  }
}

A Proficient (P) answer will look at the value of the second case, and see that we are always consing a List[Int] onto another list deduce that the answer is (List[Int], List[List[Int]]).

Another Proficient (P) answer may see observe that the type argument of foldRight is also its return type, and therefore deduce the answer is (List[Int], List[List[Int]]).

Exercise 29.3 Consider the same Scala expression above. Explain what the foldRight call with the given callback function does. What value will the foldRight call return?

Hint: You could step through the first several iterations of the folding function and see what the value of acc becomes each time.

A Proficient (P) answer will recall the type deduced above, and then step through the code and see that the left side of the accumulator remembers the current list of consecutively equal-valued integers in the input, while the right side collects such lists when the the consecutive integer values in the input differ. It will then extrapolate to get the final output of (List(1), List(List(2, 2), List(3, 3, 3), List(4, 4, 4, 4))).

Selection sort is a sorting algorithm that repeatedly removes the smallest element of an unsorted list to create a new sorted list. In the next few exercises, we will implement selection sort to sort a list l: List[A] by a custom specified le: (A, A) => Boolean comparison function. The le(x,y) comparison function returns true if x is less-than-or-equal to y.

def sortBy[A](l: List[A], le: (A, A) => Boolean): List[A] = ???
defined function sortBy

Exercise 29.4 First, let’s write a function findMin to find the minimum element of l according to le if the l is not empty. The findMin function returns None if l is Nil and otherwise Some(a) for the minimum element according to le. Do not use recursion and instead use higher-order iteration methods.

def findMin[A](l: List[A], le: (A, A) => Boolean): Option[A] = ???
defined function findMin

You may pattern match for Nil or use isEmpty: List[A] => Boolean to detect if l is empty.

A Proficient (P) answer might use foldRight or foldLeft:

def findMin[A](l: List[A], le: (A, A) => Boolean): Option[A] = 
  l.foldRight(None: Option[A]) {
    case (x, None) => Some(x)
    case (x, Some(y)) => if (le(x, y)) Some(x) else Some(y)
  }
defined function findMin

An Exceeding (P) answer might use reduceRight instead to apply le to each pair of elements starting from the right, and take the minimum of them to compare to the next one.

def findMin[A](l: List[A], le: (A, A) => Boolean): Option[A] = 
  if (l.isEmpty) None
  else Some(l reduceRight { (x, y) => if (le(x, y)) x else y })
defined function findMin

Exercise 29.5 Next, write a function to remove any specified element e from l if it exists. Again, do not use recursion and instead use higher-order iteration methods.

def removeOne[A](e: A, l: List[A]): List[A] = ???
defined function removeOne

Hint: You can write a recursive version of removeOne and then translate it into a foldRight or foldLeft.

A Proficient (P) answer will observe that we need a flag to determine whether we have removed an element already or not:

def removeOne[A](e: A, l: List[A]): List[A] = {
  val (_, accl) = l.foldRight((false, Nil: List[A])) {
    case (x, (false, accl)) if x == e => (true, accl)
    case (x, (removed, accl)) => (removed, x :: accl)
  }
  accl
}
defined function removeOne

Exercise 29.6 Finally, combine both of these functions to complete the implementation of sortBy. You may define sortBy using recursion.

def sortBy[A](l: List[A], le: (A, A) => Boolean): List[A] = ???
defined function sortBy

A Proficient (P) answer will combine the two functions to first find the min, put it at the head of a list, then recursively sort the remainder of a list with that element removed.

def sortBy[A](l: List[A], le: (A, A) => Boolean): List[A] = findMin(l, le) match {
  case None => Nil
  case Some(min) => min :: sortBy(removeOne(min, l), le)
}
defined function sortBy

29.2 Static Typing

Consider the syntax of TypeScripty with base values, functions, and immutable objects:

\[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{number} \mid\texttt{bool} \mid\texttt{string} \mid\texttt{Undefined} \\ & & \mid& \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' \mid\texttt{\{} \overline{ f\texttt{:}\,\tau } \texttt{\}} \\ \text{expressions} & e& \mathrel{::=}& n \mid b \mid\mathit{str} \mid\mathbf{undefined} \mid\mathop{\mathit{uop}}e_1 \mid e_1 \mathbin{\mathit{bop}}e_2 \mid\cdots \\ & & \mid& \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid e_1\texttt{(}e_2\texttt{)} \mid\texttt{\{} \overline{ f\texttt{:}\,e } \texttt{\}} \mid e_1\texttt{.}f \\ \text{variables} & x, y \\ \text{fields} & f \\ \text{numbers} & n \\ \text{booleans} & b \\ \text{strings} & \mathit{str} \end{array} \]

For simplicity, observe that function literals are anonymous and always have annotated return type.

Exercise 29.7 Define the values of this language (assuming the operational semantics is defined via substitution).

A Proficient (P) answer states a value form for each type: \[ \begin{array}{rrrl} \text{values} & v& \mathrel{::=}& n\mid b\mid\mathit{str}\mid\mathbf{undefined} \mid\texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid\texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} \end{array} \] An object value is one where each component of an object literal is a value.

An Exceeding (E) answer considers whether a function literal or a closure is the value form for function types. However, because the question states the semantics is defined via substitution, the answer can consider function literals as values.

An Exceeding (E) answer may also state that the above grammar for \(v\) is a shorthand for the unary judgment form \(e\;\mathsf{value}\) that is analogous to how we implement in Scala with the isValue function:

\(\fbox{$e\;\mathsf{value}$}\)

\(\inferrule[NumVal]{ }{ n\;\mathsf{value} }\)

\(\inferrule[BoolVal]{ }{ b\;\mathsf{value} }\)

\(\inferrule[StringVal]{ }{ \mathit{str}\;\mathsf{value} }\)

\(\inferrule[UndefinedVal]{ }{ \mathbf{undefined}\;\mathsf{value} }\)

\(\inferrule[FunctionVal]{ }{ \texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e_1 \;\mathsf{value} }\)

\(\inferrule[ObjectVal]{ e_1\;\mathsf{value} \and \cdots \and e_n\;\mathsf{value} }{ \texttt{\{} f_1\texttt{:}\,e_1\texttt{,} \ldots\texttt{,} f_n\texttt{:}\,e_n \texttt{\}} \;\mathsf{value} }\)

The \(e\;\mathsf{value}\) judgment form makes it evident that with object literals, it must be an inductively-defined relation.

Exercise 29.8 Give typing rules for the function and object expressions forms:

\(\texttt{(} \overline{y\texttt{:}\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e_1\)

\(e_1\texttt{(}e_2\texttt{)}\)

\(\texttt{\{} \overline{ f\texttt{:}\,e } \texttt{\}}\)

\(e_1\texttt{.}f\)

A Proficient (P) answer gives four typing rules: one for each form (e.g., \(\TirName{TypeFunction}\), \(\TirName{TypeCall}\), \(\TirName{TypeObject}\), and \(\TirName{GetField}\)) from the preceding chapters.

An Exceeding (E) answer might note that with this simplified expression language for function literals, we only need one rule for function literals (corresponding to \(\TirName{TypeFunctionAnn}\) in the preceding chapters).

Exercise 29.9 Consider the following JavaScripty code:

const x = 7;
const y = "hello";
const b = x < 0;
const f = (n) => n + 5;
const test = {
    a: b,
    b: {z: y}, 
    c: b,
};
test.b.z

Suppose we want to refactor it into TypeScripty. What do we need to do?

A Proficient (P) answer will recognize that we need to annotate the function literal with types. Specifically, we need to update the line binding f as follows:

const f = (n: number): number => n + 5;

Exercise 29.10 The above code refactored into TypeScripty is well-typed. Consider this judgment that is in a sub-derivation of type checking the above TypeScripty code:

\[ \Gamma \vdash \texttt{test} \texttt{.} \texttt{b} \texttt{.}\texttt{z} : \tau \]

What is the type environment \(\Gamma\) and the result type \(\tau\) for this judgment?

A Proficient (P) answer will recognize \(\Gamma\) as resulting from the \(\mathbf{const}\) bindings: \[ \begin{array}{rl} \Gamma\colon & \texttt{x} : \texttt{number} , \texttt{y} : \texttt{string} , \texttt{b} : \texttt{bool} , \texttt{f} : \texttt{(} \texttt{n} \texttt{:}\, \texttt{number} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \texttt{number} , \\ & \texttt{test} : { \texttt{\{} \texttt{a} \texttt{:}\, \texttt{bool}\texttt{,} \texttt{b} \texttt{:}\, \texttt{\{} \texttt{z}\texttt{:}\,\texttt{string} \texttt{\}} \texttt{,} \texttt{c} \texttt{:}\, \texttt{bool} \texttt{\}} } \end{array} \] which shows that \(\tau\) is \(\texttt{string}\).

Exercise 29.11 Now consider the following JavaScripty code snippet instead. Can we refactor this code snippet to TypeScripty? If yes, give their new types. If no, explain why, and give a possible solution.

const x = 7;
const y = "hello";
const b = x < 0;
const f = (n, m) => n + m;
const test = {
    a: b,
    b: {z: y}, 
    c: b,
};
const r1 = f(test.b.z, y);
const r2 = f(1, x);
const r3 = f(test.b.z, x);

A Proficient (P) answer will note that we can no longer annotate the type of (n, m) => n + m, since it is ambiguous whether it is concatenating strings or adding numbers now. It should recognize that + is being used for concatenating strings on the line binding r1, + is being used for adding numbers on the line binding r2, and + is being used for concatenating strings with a number to string coercion on the line binding r3. A Proficient (P) answer may say that it is not just not possible to do this refactoring.

An Exceeding (E) answer may say that you can create two function literals (n: number, m: number): number => n + m and (n: string, m: string): string => n + m for the r1 and r2 lines, respectively, but (n: string, m: number): string => n + m will not type check for the r3 line. An Exceeding (E) answer may consider the possible solution of creating a type that includes both \(\texttt{number}\) and \(\texttt{string}\) and update typing to allow for coercions between numbers and strings. As a comment for an accelerated student, there are multiple ways to allow for this polymorphism, including subtyping and union types.

Recall that our type checking rule for && and || was as follows:

\(\inferrule[TypeAndOr]{ \Gamma \vdash e_1 : \texttt{bool} \and \Gamma \vdash e_2 : \texttt{bool} \and \mathit{bop}\in \left\{ \texttt{\&\&}, \texttt{||} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)

Suppose we instead replaced this rule with the following four rules to try to more closely match our standard small-step operational semantics (cf. Figure 28.1 in Section 28.3) that does short-circuiting evaluation:

\(\inferrule[TypeAndFalseShort]{ }{ \Gamma \vdash \mathbf{false} \mathbin{\texttt{\&\&}} e_2 : \texttt{bool} }\)

\(\inferrule[TypeAndTrueShort]{ \Gamma \vdash e_2 : \tau_2 }{ \Gamma \vdash \mathbf{true} \mathbin{\texttt{\&\&}} e_2 : \tau_2 }\)

\(\inferrule[TypeOrTrueShort]{ }{ \Gamma \vdash \mathbf{true} \mathbin{\texttt{||}} e_2 : \texttt{bool} }\)

\(\inferrule[TypeOrFalseShort]{ \Gamma \vdash e_2 : \tau_2 }{ \Gamma \vdash \mathbf{false} \mathbin{\texttt{||}} e_2 : \tau_2 }\)

Exercise 29.12 Are these new rules unsound? Unsound means that it allows expressions to be type-checked that would then get stuck during evaluation using our standard small-step operational semantics (see Section 26.7 for further discussion about soundness). If you say they are sound, explain why our standard small-step interpreter cannot get stuck. If you say they are unsound, give an expression that type checks but would get stuck during evaluation.

A Proficient (P) answer will explain that the rules are in fact still sound because the four rules correspond to the four \(\TirName{Do}\) rules that implement short-circuiting evaluation of \(\texttt{\&\&}\) and \(\texttt{||}\).

Exercise 29.13 Compare this new set of rules (i.e., \(\TirName{TypeAndFalseShort}\), \(\TirName{TypeAndTrueShort}\), \(\TirName{TypeOrTrueShort}\), \(\TirName{TypeOrFalseShort}\)) with the original set (i.e., \(\TirName{TypeAndOr}\)) for type checking. Are there expressions where the old set would allow but the new rules would not? If so, give an example expression and explain briefly. What about vice versa?

An Exceeding (E) answer will see that the expressions that can type checked with the two sets are incomparable. For example, the \(\mathbf{false} \mathbin{\texttt{\&\&}} \texttt{1} \) is well-typed with the new set but not the old set. And vice versa, the \( \texttt{(}\mathbf{false} \mathbin{\texttt{\&\&}} \mathbf{false}\texttt{)} \mathbin{\texttt{\&\&}} \mathbf{true}\) is well-typed in the old set but not the new set.

A Proficient (P) answer will likely see one direction but not the other. An example like \(\mathbf{false} \mathbin{\texttt{\&\&}} \texttt{1} \) that is well-typed with the new set but not the old set is typically easier to see.

Exercise 29.14 Suppose that our type system is sound (i.e., our judgment form \(\Gamma \vdash e : \tau\) is sound with respect to our small-step operational semantics \(e \longrightarrow e'\)). Further suppose that our implementations of these two judgment forms hastype and step, respectively, are correct. Now suppose that we have a closed TypeScripty expression e that type checks with hastype (i.e., hastype(Map.empty, e) does not throw StaticTypeError). Will iteratively running step on e always terminate in a value, or is it still possible that it results in an error? If you think it terminates in a value, justify why. If you think it could still encounter an error, give an example and explain what types of errors are possible.

A Proficient (P) answer may note that there can still be other run-time issues like division by 0 or infinite loops. Therefore, there is no guarantee that the program will now terminate in a value.

An alternative Proficient (P) answer can state that type checking will eliminate typing errors that would otherwise result in a StuckError or MatchError at run time. This is what is stated as soundness in Exercise 29.12.

An Exceeding (E) answer will distinguish between typing errors that are all soundly caught at compile time and other run-time issues like division by 0 or infinite loops. The answer may state this is what is stated by the progress and preservation properties of a sound type system.