Thursday, April 16, 2009 11:36 PM bart

Type Theory Essentials in Pictures – Part 1 – Answers

A while back I posted Type Theory Essentials in Pictures – Part 1 – Quiz, a series of non-annotated pictures representing concepts from type theory. Though the first part was intended to be simple, I got some feedback that people were puzzled about it… So let’s go ahead and explain it today. Next time, we’ll get into more advanced concepts; hopefully this first batch of answers will make subsequent parts easier to absorb.

Here we go:

Figure 1

image

Dotted lines indicate the abstract notion of some type, e.g. T. Given the type, we can create an instance of it (through an instance constructor that is, hence the factory in the middle). An instance therefore is indicated as a solid body. So far, we’ve just stated there is a way to go from type to instance, nothing more. We haven’t yet said what that type is. Everything is still very abstractly defined as “an instance” of “a type”, hence the black and white.

 

Figure 2

image

Here we’ve gotten more concrete (= colorful). The dotted lines have been traded for solid lines and our type T has been substituted for something real: Block. Our factory is very concrete as well, there’s a real constructor somewhere that knows how to create new blocks. The output of this is a concrete instance, in this case a blue Lego block.

 

Figure 3

image

Besides values there are functions that act upon data. The most abstract notion of this is a function going from some type T to some type R. What those types are is still unknown, and so is a possible implementation of such a function. Hence everything is abstract, still dotted. The block on the left represents type T, the one on the right type R. The sad face in the middle is a unary function: it has two arms but one is disabled (meaning it has one arm to grab something of type T and transform it somehow to produce something of type R). The function by itself is still abstract, as its type parameters are not concrete either.

 

Figure 4

image

With dotted lines gone, we enter the world of concrete types again. T has been substituted for Block and R for Pin. Now we have “a function” that takes a block and produces a pin. We haven’t said how it does that transformation though; the function is still sad as it doesn’t have any concrete value to play with.

 

Figure 5

image

First we need to concretize the function, saying how it can take “some block” and produce “some pin”. A practical implementation of such a function could be a kid that demolishes a Lego block and returns the top left pin of it. The functional kid is slightly more happy because it already knows how to play with blocks (in a deterministic way though, given any Block it will produce the same corresponding Pin), but it’s still sad enough not to have concrete blocks to play with. But that’s changing now…

 

Figure 6

image

Now our functional kid got a blue Lego block to play with: everything’s happy. Given the blue block, we get the top left (obviously still blue) pin back. So far for unary functions: we’ve gone from a parameterized type Func<T, R> to a concrete function type Func<Block, Pin>, have implemented it next and finally fed it some data to act upon.

 

Figure 7

image

Same story as before, but this time for a binary function, one that takes two arguments (notice how the second arm is not disabled). Everything is still abstract.

 

Figure 8

image

Getting more concrete again, having a function that can take two blocks and produce a stack of blocks out of it. Notice the shape of the data is already known: a Stack type likely has two Block fields inside it.

 

Figure 9

image

Next we give the concrete implementation of such a function. We assume there’s a binary + operator available that acts upon Block objects to produce a Stack of the given blocks. Alternatively you could think of “new Stack(b1, b2)” as a possible implementation for the function.

 

Figure 10

image

Finally our function can play with real blocks: given a blue block and a red block, a stack of those blocks is produced with the former block placed on top of the latter block.

 

Figure 11

image

This is a bit more of a brainteaser. Here we’re currying a function: we specify not enough arguments for the function to produce a final value. Instead, we get a remainder function back. In this case we have a function to produce stacks but we only fed it one block. The result is a unary function that takes the remainder block and puts it below the already provided block.

The syntax in the title is not valid in C#: there’s no built-in support to apply a function partially. Instead you could write:

Func<Block, Block, Stack> playingKid = (b1, b2) => b1 + b2);
Block blueBlock = new Block(Color.Blue);
Func<Block, Stack> partiallyPlayingKid = otherBlock => playingKid(blueBlock, otherBlock);

The bold part indicates the explicit burden put on the developer to carry out the currying manually.

Note: Actually none of the function titles are valid C# code. A lambda expression like “(int a) => a” doesn’t have a type by itself because of various reasons (one is there are two ways to represent lambdas: as delegates or as expression trees).

 

Figure 12

image

Function composition. The big circle should be read as “after”. Here it says to compose a function from some type S to some type R with another function from some type T to some type S, by feeding the output from the latter to the input of the former:

Func<S, R> O Func<T, S>

Again the different types are indicated by different line dotting styles. Notice though how the types in the middle have to match. In mathematical terms you’d say that the range (= output type) of the first should correspond with the domain (= input type) of the second:

f : T –> S
f(t) = t + 3

g : S –> R
g(s) = s * 2

g o f : T –> R
(g o f)(t) = g(f(t)) = (t + 3) * 2

Or stated otherwise, going from T to S and S to R makes it possible to ignore the intermediate phase of S and hide it as an implementation detail by applying function application: the resulting function simply goes from T to R.

Note: I’ve omitted the smiley faces from this point on. Black solid arrows represent the concept of functions.

 

Figure 13

image

The last picture was an abstract notion of function composition: everything was still generically typed. To make it more concrete, we substitute the type parameters for concrete types. If we have a kid that removes the pins of a block (how it does that precisely is not stated yet; it could hammer the pins off or pull them off or set them on fire or …), leaving the “body” of the block, and another one that pulls some side (which one is yet not specified) off the body, we can make them play together in a room: the input of which is a Block and the output of which is a Side. We don’t need to know the kids implement it by dividing the tasks among themselves.

I’ve indicated “some side” as a titled and rotated rectangle. It’s yet unknown what the precise side will be for a particular implementation: it could be the top or the bottom, the left or the right, the front or the rear.

 

Figure 14

image

Things get concrete now. The first kid is implemented by returning the “Body” property of the block (how that one works you have to imagine yourself, as long as it has some concrete implementation), while the second one chops of the floor from the body. The result is that given a Block x, we ultimately get back its Floor side. The intermediate state of Body is irrelevant to the outsider.

Look how the types “flow” in the title.

1.                     (Block b => b.Body)(x)
2. (Body c => c.Floor)(              """"    )

Given a block, we get the body, which we feed into the function that produces a floor.

 

Figure 15

image

Feed in a blue block to this whole thing and back you get its blue floor (assuming the – mostly invisible – floors of Lego blocks have the same color of the rest of the block).

Composition is the single most important concept when dealing with complexity: implement the simpler parts and glue them together to make something more complex. We’ll see more of that in a next series.

Happy puzzling!

Del.icio.us | Digg It | Technorati | Blinklist | Furl | reddit | DotNetKicks

Filed under:

Comments

# Dew Drop - April 17, 2009 | Alvin Ashcraft's Morning Dew

Pingback from  Dew Drop - April 17, 2009 | Alvin Ashcraft's Morning Dew