Mechanically Deriving Programs from Types for Assignment 2

There are two major challenges in assignment 2:

  1. Deriving the correct type signatures for the different methods and functions
  2. Implementing Scala code that satisfies (that is, code which is compliant with) the aforementioned type signatures

It is recommend to try to get the function signatures right first, and then fill in the bodies with ???. This way, you can compile your code incrementally as you compile the bodies, which should help find problems faster. The most difficulty in this assignment tends to be in getting things just to compile.

One you have the correct type signatures (or are at least reasonably sure you have the correct type signatures), you can start to derive the bodies of the methods. That is, you can start replacting ??? with actual executable code. While this derivation may seem challenging (after all, this is the real “meat” of the code), this usually is a mechanical process once you get the hang of it.

To illustrate this process, I have an example below which derives the implementation of translatePt. While this only goes over translatePt specifically, the general process is applicable to all the code you need to write.

Deriving translatePt

Deriving translatePt's Type Signature

The first task is to implement the type signature for translatePt. Relevant to this process is the comment corresponding to translatePt, which is copied below:

// define a method named 'translatePt' that takes a Vector as
// argument and returns a TransformPt that translates a point
// according to the given Vector. recall that to translate a point
// by a vector, you simply add the vector's x component to the
// point's x coordinate and the vector's y component to the point's
// y coordinate.

Taking this comment, piece-by-piece, we can incrementally define the type signature. First:

// define a method named 'translatePt'

...so:

def translatePt

We still need the arguments, the return type, and body. Stepping forward through the comment, we see this:

// that takes a Vector as
// argument

...so:

def translatePt(arg: Vector)

Now for the return type. From the comment:

// and returns a TransformPt

...so:

def translatePt(arg: Vector): TransformPt

Deriving translatePt's Body

Here, we're stuck a bit. We need a function that takes a Vector and returns a TransformPt, but there isn't such a function in the file. Taking a more indirect route, we could also find a series of functions that would allow us to derive TransformPt from Vector. For example, if there was something like:

foo: Vector => Foo
bar: Foo => Bar
baz: Bar => TransformPt

...then we could write something like:

baz(bar(foo(arg)))

Unfortunately, there doesn't appear to be anything in the file that would allow us to do this, so there isn't a way to simply piece together what's already there.

That said, we're not completely stuck at this point. Note that TransformPt is a type alias (i.e., it was introduced with Scala's type reserved word). For any type alias, it is possible to go back and forth between representations as desired. Additionally, type aliases can reference other type aliases, as with ImgMask referencing Img, where Img is another type alias. To try to get some additional information, let's expand out TransformPt as much as possible:

// TransformPt = Point => Point
def translatePt(arg: Vector): Point => Point

Now we have a bit more information which can help guide the body's creation. We see that what's returned must be a function (i.e., the return type contains =>that takes a Point and returns a Point. There doesn't appear to be anything applicable already in the file, so let's define something new. Here, recall that the syntax to define an anonymous function in Scala is:

(param1: Type1, param2: Type2, ..., paramN: TypeN) => Body

With this in mind, we can start to define the body:

def translatePt(arg: Vector): Point => Point =
(point: Point) => ???

...where ??? in the above code is a placeholder for something of type Point. We know that ??? must be of type Point, because we've just implemented the Point => part of the function (the above is a function that takes a Point).

Now for finding something of type Point. Note that the function's parameter is of type Point, and so we could just use that directly, like so:

def translatePt(arg: Vector): Point => Point =
(point: Point) => point

The above will typecheck, though the implementation will not be correct. After all, the method translatePt is supposed to perform a translation, but the above implementation simply returns the original point (with the variable point). This is effectively a no-op.

Here is where we must go back to the original comment, which described exactly what sort of translation translatePt is supposed to do:

// recall that to translate a point
// by a vector, you simply add the vector's x component to the
// point's x coordinate and the vector's y component to the point's
// y coordinate.

With this in mind, we can define the following:

def translatePt(arg: Vector): Point => Point =
(point: Point) => Point(arg.x + point.x, arg.y + point.y)

Now we have something that both typechecks and is correct.

Summary of General Process

Basically, with this process the goal is to incrementally move forward, using bits and pieces of information to move forward. With a type system as powerful as Scala's, this sort of process is useful on a day-to-day basis, especially when it comes to interacting with existing libraries. For example, say I want to perform a particular operation that should yield something of type A. I can then peruse the standard libraries for something that returns something of type A. If no such thing exists, then I can look for a chain of calls that would derive something of type A. If I do find something, then the input types tell me what I need to provide. If no such thing exists, then I know I must implement my own routine. This sort of process allows one to cover the documentation quite rapidly, since you don't need to look at method implementations, descriptions, or even names. This is in contrast to dynamically-typed languages, wherein essentially everything has the same type, necessitating much more reading.

A special note regarding method signatures should be made here. Do make sure that your method signatures are correct before going through this process. If your method signature is incorrect, then all bets are off. You may be able to derive something, but at the positions where the method is used typechecking will almost assuredly fail.

This whole process illustrates something very powerful about functional programming. The “hard part” of coding lies in defining correct method and function signatures, whereas the implementation of these signatures tends to be mechanical. In fact, some of the feedback we have gotten from students who really get the hang of assignment 2 is that it makes all subsequent Scala-based assignments trivial: oftentimes, it is sufficient just to write something that typechecks, and often the code will at least be very close to working. This is reflective of the fact that the focus tends to move from the actual code you write to the type signatures you write, and the type signatures are usually fixed throughout these assignments. This is why we say that this assignment, and often functional programming in general, tends to be type-directed: the types heavily guide the actual implementation.

Aside: When Typechecking Isn't Enough

A potential lingering question: why is it that the original proposed implementation of translatePt that simply returned the provided point (with the variable point) typechecked when it was otherwise not correct? Ultimately, the problem is that Scala's type system is not powerful enough to express exactly what translatePt is supposed to do, only a brief summary of what it does (specifically, its type signature). We'd like the type itself to actually say what the transformation is supposed to do, but here we only encoded that the type has a shape of some transformation. Thinking of types as a set representation of values of that type, this is like saying that both the correct and incorrect implementations are in the set Point => Point. With a more constrained type, the incorrect implementation would not be included in this set, but the correct implementation would be (i.e., the constrained type forms a strict subset of Point => Point).

So why isn't Scala's type system powerful enough to handle the more specific type? Ultimately because this generally means we need dependent types (http://en.wikipedia.org/wiki/Dependent_type), which would be undecidable to typecheck in Scala. Dependent types are so powerful that you can encode things like terminating programs as a type, and typechecking such a type amounts to solving the halting problem. As one might expect, these type systems are incredibly powerful in what they allow programmers to express, powerful to the point where they allow for verified code. That is, code that is known to work correctly across all possible inputs, even if there is an infinite set of such inputs. However, this power comes at a tremendous cost: the programmer must effectively guide the typechecker along by hand in order to typecheck anything of any significance. This starts to look incredibly similar to doing proofs in first-order logic (and from a theoretical level, there isn't that much of a difference!). As this tends to be inconvenient, we don't cover it to any real degree in this class.