Mechanically Deriving Implementations from Types

Overview: Type-Directed Programming

There are a number of valid ways to look at types. For example, two common ways to look at types are:

  1. A way to explain to the compiler/interpreter what sort of operation should occur
  2. A way to statically check for certain kinds of programmatic errors

This assignment directly explores yet a third way to look at types: as a means to guide software development.

Small Example

Say we have the following two functions available:

def foo(a: A): B = ...
def bar(b: B): C = ...

Say we've determined that we need a new function baz, which takes something of type A and returns something of type C:

def baz(a: A): C

Given the functions available, an implementation which typechecks is immediately apparent:

def baz(a: A): C = bar(foo(a))

Additionally, given the provided types and type information, it's immediately apparent that the following would fail to typecheck (i.e., cannot possibly be a valid implementation):

def baz(a: A): C = foo(bar(a))

Note how little information we're using here: not a thing has been stated about what foo, bar, or baz does. The only information used is type information. Even so, this is sufficient to eliminate candidate programs.

With the above example, we're taking the error-checking capabilities of types one step further to actively eliminate programs which cannot possibly exist. This sort of technique can be used to help guide the implementation when only the most basic of information is available. In the real world, this can be used to eliminate the vast majority of otherwise syntactically-valid implementations. Specifically with this assignment, you'll likely find that in many contexts very few functions are applicable based on the needed input and output types. If you're stuck, types can be exploited in this way to help narrow the range of possible implementations.

Larger Example

The example below shows how to mechanically derive the implementation of translatePt. While this only goes over translatePt specifically, the general process is applicable to all the code you need to write.

First, we will derive translatePt's type signature. Relevant to this process is the comment corresponding to translatePt, which is copied below:

// Define a method named 'translatePt' that:
// -Takes a Vector, and
// -Returns a TransformPt that translates a point according
//  to the given Vector.  Recall that to translate a point
//  by a vector, you add the vector's X component to the point's
//  X coordinate and the vector's Y component to the point's
//  Y coordinate.

We can incrementally break this comment down to form a type signature. First:

// Define a method named 'translatePt' that:

...so:

def translatePt

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

// -Takes a Vector, and

...so:

def translatePt(arg: Vector)

Now for the return type. From the comment:

// -Returns a TransformPt

...so:

def translatePt(arg: Vector): TransformPt

Now that we have translatePt's type signature, we need to derive its 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 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 for Mechanically Deriving Types

This process allows us to incrementally move forward from a type signature, using bits and pieces of existing type information along the way. 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 this process won't work, because you're starting with incorrect information. 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 programming in statically-typed languages. 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 understood this assignment is that it makes all subsequent Scala-based assignments trivial: oftentimes, it is sufficient just to write something that typechecks, and the code will quite frequently be correct or at least close to correct. 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 programming in good statically typed languages 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), and Scala is not designed as a dependently-typed language. Dependent types are so powerful that you can encode types which reason about program termination, and typechecking such types 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 is because we intentionally have made typechecking very difficult in order to get maximum expressibility in the type system. 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.