I'd like to demonstrate a technique for using types
to guide the construction of functional programs.
I have here a Haskell source file with three functions.
The types are given,
but the implementations are stubbed out.
I'll try to fill in the implementations
using what I know about the types,
but I'll otherwise pretend I don't know
what the functions are meant to do.
The first thing I'll do
is make a new name for 'undefined'.
This isn't really necessary,
but it will make things a bit more meaningful.
So a hole is just something that needs to be filled in.
Now let's look at 'compose'.
We can see from the type that it takes three arguments,
so let's give them names: 'f', 'g' and 'x'.
Now let's pull apart the type of 'compose'
so we can write down the type of each argument.
We'll also write down the type of the hole
which is the same as the result type of 'compose',
which is 'c'.
So we need something of type 'c',
and from the arguments, we see that
the only way we'll get that
is by applying 'f' to something of type 'b'.
So let's replace the hole with an application of 'f'.
We don't yet have anything of type 'b',
so we'll just make a new hole for the argument,
and we'll make a note that
the type of the new hole is 'b'.
Similarly, the only way we'll get something of type 'b'
is by an application of 'g',
so let's replace this hole with an application of 'g'.
We now need a new hole for the argument to 'g',
so the type of the hole must be 'a'.
And finally, we already have an 'x' of type 'a',
so we can just use it to fill in the last hole,
and we've arrived at an implementation.
So you see that the technique is to
write down the types of what we have
starting with what we're given as arguments
and also to write down the types of what we need,
starting with the result we need to return.
As in this example, we can then work
backwards from what we need
filling each hole using what we have,
possibly revealing new holes
that we we subsequently need to fill.
As we'll see shortly, we can also work forwards,
constructing new things from what we have,
with the aim of eventually constructing
something that will fill a hole.
But I'm not really happy with
the way we've gone about this.
For one thing, our type assertions are just comments
and they're not checked
so a mistake will lead to wasted effort.
Secondly, it might be awkward
to track the types of multiple holes.
And finally, we have to work out the types ourselves,
when we know that the compiler
ought to be able to do that for us.
So let's start again,
but this time we'll write our assertions
so they can be checked by the compiler.
For the arguments, we'll add a 'where' clause
with a set of dummy bindings.
Visually, this is similar to the comments we wrote before,
but now the types can be checked.
In case it's not clear what's going on here,
we're just taking each argument to the function,
and binding its value to a wildcard pattern
within the scope of the 'where' clause.
The wildcard pattern ensures
that we don't actually create any new names
so we can't change the meaning of the program,
but the type annotations will be checked.
As it is, the compiler won't accept this,
because in plain Haskell,
type variables in the function signature
are not scoped over the function definition.
so the 'a's, 'b's and 'c's in our assertions
are not recognised as the 'a's, 'b's and 'c's in the signature.
We can fix that by turning on a language extension
called 'ScopedTypeVariables'.
We also need to write an explicit 'forall'
to mark the scope to which we want the type variables bound.
That type-checks, and now we can see that
if we make a mistake in one of our annotations,
for example, here,
we get a type error that tells us
not only the location of the error
but what the type should have been,
in this case, 'a' rather than 'b'.
Let's look at the hole.
Rather than work out the type of the hole myself,
I'd like the compiler to tell me.
I can get it to do that by provoking a type error.
To systematically provoke type errors,
we just need a value of a concrete type
that is different from every type
we might use in our programs.
So let's just make a type
and a corresponding data constructor,
both called Hole, with a capital 'H'.
Now we have two varieties of hole.
I'll call the upper-case variety a noisy Hole,
since it will always provoke a type error,
and I'll call the lower-case variety a silent hole,
since it will always be accepted anywhere.
The idea is that if we have several holes,
we'll use only one noisy Hole at a time,
and leave the rest as silent holes.
That way, when we're looking at an error message
provoked by a noisy Hole,
we don't have to think about
which Hole caused that error.
Let's make this hole noisy.
If we look below, the error message tells us that
GHC was expecting a 'c' instead of a Hole.
Using the same reasoning as before,
we replace the Hole with an application of 'f',
and now the compiler tells us that
the new Hole needs to be filled with a 'b'.
So we replace that with an application of 'g',
and now the new Hole needs to filled with an 'a'.
And finally, we can satisfy that with an 'x'.
Now, because the noisy Hole is a type
as well as a value,
we can also use it in type contexts.
For example, if we weren't sure of the type of 'x'
while writing assertions about the arguments,
we can just use a noisy Hole to ask the compiler.
So this error message tells us that
the Hole should have been an 'a'.
Now that we're done,
we can remove the superfluous dummy bindings,
and since we're no longer referring to type variables
in the body of the function,
we can also remove the 'forall' binders.
So much for 'compose'.
Let's move on to a slightly more interesting example.
In the type of 'apply',
we see that the variable 'm' stands for a type constructor,
and we can further see that it is constrained
to the type-constructor class 'Monad'.
The constraint means that we know more about 'm'
than if it were unconstrained.
In particular, we know that we can,
and indeed will probably have to make use of
the methods of the 'Monad' type-constructor class
in our implementation.
Proceeding as before, we see from the type that
'apply' takes two arguments,
so we'll name them 'mf' and 'ma'.
We'll write assertions for the types of the arguments.
And, of course, we need to remember
to explicitly bind the type variables in the signature.
OK, so that compiles now.
But remember that if we weren't sure of
the type of an argument
we can use a noisy Hole to ask the compiler.
Here it's telling us that it was expecting
'mf' to have the type 'm' of 'a' to 'b'.
Looking back at the implementation,
if we make our Hole noisy, we see that we need to
construct something of type 'm b'.
Clearly, we can't do that
with a simple application of what we have,
so we're going to have make use of the fact that
'm' is a Monad.
Now, if we need to remind ourselves
of the type of any function or method we want to use,
we could use a GHCi query, or alternatively,
we can use a dummy binding.
In particular, we can use a dummy binding
to check whether we can
specialise any variables in the type of the function
to the particular types that we want to use.
For example, if we add a dummy binding
for the monadic 'bind' operator
we can use a noisy Hole to ask for its type.
For reasons I don't quite understand,
GHC doesn't tell us the full story,
but it's enough to get us by.
Notice that the error uses fresh type variables,
'm0', 'a0' and 'b0'.
These are universally quantified, which means
we should be able to instantiate them to anything we like.
Since we want to construct an 'm b',
it seems likely that we'll want
the 'bind' operator to return 'm b' as well,
so we might as well specialise
by instantiating 'm0' and 'b0' with 'm' and 'b' respectively.
But since I'm not sure what 'a0' will be,
I'll leave that polymorphic for now,
and, in fact, I'll write an explicit 'forall' to make this clear,
and I'll rename 'a0' to 'h'
to avoid any confusion with the type variable 'a'.
This now passes the type checker, which means that
this is a valid partial specialisation.
Now, we have two choices
for applying the bind operator: 'mf' and 'ma'.
If we want to, we can use dummy bindings
to explore the resulting types.
For example, if we partially apply "bind' to 'mf',
this will swallow the first parameter.
Since this will also instantiate the type variable 'h',
we can use a noisy Hole to find out its type.
And, of course, we can do the same
for a partial application of 'bind' to 'ma'.
OK, back to the implementation.
Without anything else to tell us which argument to bind first,
we'll just follow convention,
and bind the left-most argument first.
So we replace our Hole with 'mf' bound to a new Hole.
We see that the new Hole requires a function of one argument,
and in order to make assertions
about the type of the argument,
we need a name and a scope to write those assertions,
which means we also need to name the function.
So we'll name the function 'k',
and its argument 'f',
and we'll use a silent hole for the result of 'k'
while we're dealing with assertions about the type of 'f'.
Writing the assertion, we find that 'f' has type 'a' to 'b'.
Now, switching to a noisy Hole for the result of 'k',
we see that again we need to construct an 'm b'.
We still have no way to do this with
a simple application of of what we have,
so we turn to the monadic 'bind' operator,
this time on 'ma'.
Again, the new Hole requires
a function of a single argument,
so we'll name the function 'r',
and the argument 'x',
and we'll write an assertion for the type of 'x',
using a noisy Hole to ask for the type.
This time the form of the error message is different,
but the interpretation is the same:
we need an 'a' in place of the Hole.
Returning to the result of the function 'r',
we see that GHC is expecting something of type 'm b0',
where 'b0' is a fresh type variable,
which implies that it is universally quantified.
In this case, it appears that GHC has
generalised the type it is expecting of 'r'.
Although it's not clear to me exactly when
GHC will perform this generalisation,
to see that it's reasonable for it to do so,
consider that if 'r' is polymorphic enough
to allow any type 'b0',
then clearly it can allow the specific type 'b'.
The problem is that we don't want
to implement such a polymorphic 'r'.
In fact, in this case, that would be impossible.
Instead, we want to implement
the most specific type we can,
because that is likely to be easier than
implementing a more general type.
So, if we're not sure what the specific type should be,
how can we find out from the compiler?
The trick is to move the noisy Hole
to the relevant place in a type annotation.
Then GHC is happy to tell us that
we merely need a 'b' in place of the Hole.
Now, we still have no way to directly construct
something of type 'm b'.
But we do have an 'f' of type 'a' to 'b',
and an 'x' of type 'a',
so we can construct 'f' of 'x',
and use an assertion to check its type.
Finally, to get from a 'b' to a 'm b',
we once again need to make use of the fact
that 'm' is a Monad.
If we want, we can use a dummy binding
to check that we can make
a suitable specialisation of the type of 'return'.
Then we can check that 'return' of 'f' of 'x' has the right type,
and since it does, we can fill our last hole.
Things have become a little messy,
so let's back-substitute.
Here, 'k' becomes 'lambda f' to 'ma' bound to 'r',
but since 'r' is not in scope here,
we immediately substitute 'lambda x' to 'return' of 'f' of 'x'.
We no longer need the dummy bindings,
nor do we need the explicit binders
for the type variables in the signature.
At this point, we could convert this to 'do'-notation,
or simplify using 'liftM', or both,
but I'll leave that for another time.
Instead, if you're not already exhausted,
let's do one final example.
Here, we'll see that when we encounter
concrete types and type constructors,
we typically have to make
more choices about our implementation.
We can see from the type that
'filterM' takes two arguments.
Let's name them 'p' and 'xs',
and as usual, let's write assertions about their types.
And, let's not forget to write
explicit binders for the type variables.
Now, I'm pretty sure I already know
the type of the hole,
so I'll just write that in there.
Again, we can't construct an 'm' of list of 'a'
by a simple application of what we have,
nor do we have any monadic value to bind.
But we do have a list of 'a',
so we could either pattern-match on 'xs'
or apply some list function to it.
But which list function would we apply?
There are many list functions,
so it's not an easy question to answer,
but since list is a recursive structure,
the most useful solution is likely to involve
recursion over 'xs'.
And the right-fold function, 'foldr',
captures the most general recursion scheme over lists.
So let's replace the hole with
an application of 'foldr' to 'xs',
leaving two new holes
for the remaining arguments.
The second of these arguments
corresponds to the base case for the recursion.
In other words, it's the result when 'xs' is empty.
And indeed, using a noisy Hole,
we see that it must have type
'm' of list of 'a'.
As in the previous example,
we can use 'return' to construct one of those
from a list of 'a',
and the only list of 'a' we can construct out of thin air
is the empty list,
so we should be able to replace this Hole
with 'return' of the empty list,
Now, looking at the other Hole,
we see that GHC has again
generalised the type a little more than we'd like,
but we can at least see that we need
a function of two arguments,
so let's name the function 'f',
and its arguments 'x' and 'r',
and let's write an assertion to find out
the type of 'x', which is 'a'.
Similarly, we find that the type of 'r'
is 'm' of list of 'a'.
Next, we look at the type of the result of 'f',
which we see should also be 'm' of list of 'a'.
Obviously, we could satisfy the types
by simply returning 'r',
but that gives a trivial solution
which is not useful.
Instead, we notice that we haven't yet
used the argument 'p',
which is a function from 'a' to 'm' of Bool.
Since we have an 'x' of type 'a',
we can apply 'p' to 'x' to get an 'm' of Bool,
and since 'm' is a Monad,
we can bind the result to a new Hole.
Now we see that the new Hole
requires a function of one argument,
so we name it 'k',
and its argument 'c',
and we use an assertion to find that
the type of 'c' is Bool.
Looking back at the type of the result of 'k',
we see that GHC generalises the type,
so we use the usual trick
to get a more specific type for 'b0',
and that turns out to be list of 'a'.
Now, to get a non-trivial result,
we should really do something with 'c'.
Since 'c' is a Bool, the natural thing to do is branch,
so let's replace the hole with a branch on 'c'.
This gives us two new holes, one for each branch.
Now we just need to come up with two
meaningfully different ways to construct
an 'm' of list of 'a' from 'x' and 'r'.
There are many ways to do this,
but the one seems most meaningful
is the one which relates each condition 'c'
most directly to the 'x' which produced it.
So therefore, we'll use 'x' if and only if
the condition 'c' is True.
In the False case, we'll just return 'r'.
Now, in the True case,
we want to combine 'x' and 'r'.
If we had a little experience with monads,
we might recognise that 'liftM' would do the job,
like this, but suppose we don't see that.
Then, our only real option is to bind 'r',
which is a monadic value,
to a new Hole.
The new Hole requires a function,
so we name it 'j',
and name its argument 'ys',
which GHC tells us
should have type list of 'a'.
When we try to discover
the type of the result of 'j',
we run into a new problem.
Previously, we have only seen
over-generalised type variables,
but this time GHC has given us
an over-generalised type constructor variable 'm0'.
Our usual trick to discover a more specific type won't work,
because Hole has the wrong kind.
We just get a kind error,
which doesn't tell us anything about the types.
But we can introduce a hole constructor
with the right kind.
Let's call it 'Hole1',
and notice that it takes a type argument.
Then, when we try to set the result type of 'j'
to 'Hole1 Hole',
GHC tells us first that it expected
'm' instead of 'Hole1'
And then list of 'a' instead of 'Hole'.
Now that we have 'x' and 'ys',
we can combine them to make a new list,
and use the monadic 'return'
to construct a value of the right type.
Since that fills our last hole,
and since we've used all of the arguments
to filterM' in a meaningful way,
we've arrived at a non-trivial,
and hopefully useful implementation.
In fact, this implementation is
equivalent to 'filterM' in the standard library.
Let's just clean up by back-substituting 'k',
and then 'j',
and then removing superfluous dummy bindings,
'forall' binders and type annotations.
Finally, we can disable
the 'ScopedTypeVariables' extension,
and remove the hole definitions
to make absolutely sure there's
nothing left to fill in.
And we're done.
To summarise, we've seen an approach for
using types to guide the construction
of functional programs,
which consists of writing down
the types of what we have,
and the types of what we need,
and systematically joining the dots in between.
We've also seen some tricks
for getting some help from GHC.
But don't confuse the tricks
with the underlying approach.
The underlying approach is timeless,
and in fact comes from mathematical logic,
where it's called natural deduction.
The tricks are only really applicable
to current versions of GHC,
as of early 2013.
In fact, sometime in the next few months,
we expect a release of GHC
which is likely to include a new extension
called 'TypeHoles',
which will make development
in the natural deduction style considerable smoother.