Homework 5

Due on Monday, 3 December at 10:15am sharp (right before the class).

NOTE: It is your responsibility to ask us if any part of the problem formulation is unclear.

Task 1: Type system rules

Give the type system rules that best describe the implementation of your type checker.

Type up the rules in Latex and submit as a PDF file.

The submission will be via Moodle.

You are free to use any package you prefer for typesetting of your rules. One possibility are the mathpartir and inferrule packages for Latex:

http://cristal.inria.fr/~remy/latex/
http://cristal.inria.fr/~remy/latex/mathpartir.html

Another option is the bussproofs package: http://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/index.html

Task 2: Type system for physical units

This part of the homework is again a pen-and-paper exercise.

Please write actual and complete type derivation trees as seen in class, and not just syntax trees with type annotations. Make sure, that each step is valid according to type system rules.

A unit expression is defined by following grammar

$\begin{equation*} u, v, w := \quad b \quad | \quad 1 \quad|\quad u * v \quad|\quad u^{-1} \end{equation*}$

where $u, v$ are unit expressions themselves and $b$ is a base unit:

$\begin{equation*} b := \quad m \quad|\quad kg \quad|\quad s \quad|\quad A \quad|\quad K \quad|\quad cd \quad|\quad mol \end{equation*}$

You may use $B$ to denote the set of the unit types

$\begin{equation*} B = \{ m, kg, s, A, K, cd, mol \} \end{equation*}$

For readability, we use the syntactic sugar

$\begin{equation*} u^n = \begin{cases} u * ... * u & n > 0 \\ 1 & n = 0 \\ u^{-1} * ... * u ^ {-1} & n < 0 \end{cases} \end{equation*}$

and

$\begin{equation*} \frac{u}{v} = u * v^{-1} \end{equation*}$

a)

Give the type rules for the arithmetic operations $+\;,\; *\;,\; /\;,\; \sqrt{\ } \;,\; \sin\;,\; abs$ . Assume that the trigonometric functions take as argument radians, which are dimensionless (since they are defined as the ratio of arc length to radius). You can denote that a variable is dimensionless by

$\begin{equation*}\Gamma \vdash e: 1\end{equation*}$

b)

The unit expressions as defined above are strings, so that e.g.

$\begin{equation*} \frac{s^4m^2}{s^2 m^3} \ne \frac{s^2}{m} \end{equation*}$

however physically these units match. Define a procedure on the unit expressions such that your type rules type check expressions, whenever they are correct according to physics.

c)

Determine the type of $T$ in the following code fragment. The values in angle brackets give the unit type expressions of the variables and $Pi$ is the usual constant $\pi$ in the Scala math library. Give the full type derivation tree using your rules from a) and b), i.e. the tree that infers the types of the variables $R, w, T$ .

val x: <m> = 800
val y: <m> = 6378
val g: <m/(s*s)> = 9.8
val R = x + y
val w = sqrt(g/R)
val T = (2 * Pi) / w

d)

Consider the following function that computes the Coulomb force, and suppose for now that the compiler can parse the type expressions:

def coulomb(k: <(N*m)/(C*C)>, q1: <C>, q2: <C>, r: <m>): <N> {
  
  return (k* q1 * q2)/(r*r)

}

The derived types are $C = As$ and $N = \frac{kg \;m}{s^2}$ . Does the code type check? Justify your answer rigorously.

e)

Suppose you want to use the unit feet in addition to the Si units above. How can you extend your type system to accommodate for this? Explain your answer.
(Assume that 1m = 3.28084 feet.)

Make sure that your extension makes physical sense. For example, if $x: feet$ and $y: m$ , then adding them directly as $x+ y$ is illegal. On the other hand, it should still be possible to add together quantities that can be meaningfully added together (do not make your system more restrictive than necessary).

f)

For this problem we consider expressions whose free variables have only basic types, i.e. $kg$ , $s$ , but no compund types like $\frac{m}{s}$ . Assume also that the only operators within expressions are $+, *, /, \sqrt{\ }$ , but that they can be combined in arbitrary ways and be arbitrarily large, as long as they type check.

Consider such an expression that computes a value of some type $T$ , where $T$ may be compound. Prove the following theorem for this case.

Theorem: Suppose that the result type $T$ does not contain a base unit $b_1$ (or, equivalently, this base type occurs only with the overal exponent 0, as $b_1^0$ ). If we multiply all variables of type $b_1$ by a fixed numerical constant $K$ , the final result of the expression does not change.

For example, suppose that we want to compute the center of mass $x_c$ of two objects in 2D, using the following expression:

$\begin{equation*} \frac{m_1 x_1 + m_2 x_2}{m_1 + m_2} \end{equation*}$

Here $m_1, m_2$ are the masses of the objects in $kg$ , and $x_1, x_2$ are their distances in $m$ (meters) from some reference point. Because the final result has type $m$ , by the above theorem, we can multiply $m_1$ and $m_2$ by, e.g., $42$ ; the value

$\begin{equation*} \frac{(42 m_1) x_1 + (42 m_2) x_2}{(42 m_1) + (42 m_2)} \end{equation*}$

is the same as the previous value. As another example, suppose we estimate a gravity $g$ on Moon by measuring a free fall from height $h_1$ , then compute the time needed for a free fall from another height $h_2$ , computing $t_2$ as

$\begin{equation*} \sqrt{ \frac{2 h_2}{\frac{2 h_1}{t_1^2}}} \end{equation*}$

The result type of this expression is $s$ (seconds). Therefore, if we multiply both $h_1$ and $h_2$ by a constant, say 100, the value of this expression does not change.

Let us re-state the theorem by introducing a little more notation. If $e$ is an expression (which may contain variables $y_1,\ldots,y_n$ and possibly some other variables), and $v_1,\ldots,v_n$ are expressions, let

$\begin{equation*} e(y_1\mapsto v_1,\ldots,y_n \mapsto v_n) \end{equation*}$

denote the result of replacing in $e$ in $y_1$ with expression $v_1$ , and so on, with $y_n$ replaced by $v_n$ . The theorem above then says that, under the stated assumptions, for every constant $K$ and all variables $y_1,\ldots,y_n$ whose type exponent $b_1$ in $e$ is zero, the following equality holds for all values of all variables (including $y_1,\ldots,y_n$ but also variables other than $y_1,\ldots,y_n$ ):

$\begin{equation*} e(y_1\mapsto v_1,\ldots,y_n \mapsto v_n) = e(y_1\mapsto K \cdot v_1,\ldots,y_n \mapsto K \cdot v_n) \end{equation*}$

Prove the above theorem.

Note: We assume that neither $e(y_1\mapsto v_1,\ldots,y_n \mapsto v_n)$ nor $e(y_1\mapsto K \cdot v_1,\ldots,y_n \mapsto K \cdot v_n)$ divide by zero or take square roots of negative numbers. You do not need to worry about such errors in this problem.

Hint: You may need to prove a more general theorem and derive the desired theorem as a consequence.