# 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:

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

where are unit expressions themselves and is a base unit:

You may use to denote the set of the unit types

For readability, we use the syntactic sugar

and

## a)

Give the type rules for the arithmetic operations . 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

## b)

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

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 in the following code fragment. The values in angle brackets give the unit type expressions of the variables and is the usual constant 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 .

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 and . 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 and , then adding them directly as 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. , , but no compund types like . Assume also that the only operators within expressions are , 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 , where may be compound. Prove the following theorem for this case.

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

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

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

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

The result type of this expression is (seconds). Therefore, if we multiply both and 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 is an expression (which may contain variables and possibly some other variables), and are expressions, let

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

Prove the above theorem.

Note: We assume that neither nor 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.