|
 |
There is a saying about Haskell: "When it compiles, it usually works
correctly first time."
In solemn truth, there are plenty of examples of Haskell code that
compiles just fine, but doesn't work correctly. And yet, you'd be
surprised how often that "usually" proviso holds.
(I also can't emphasise enough how many times I've written and rewritten
code, only to find out the type signatures don't line up, and in the
process realised that there's something fundamentally "wrong" with what
I'm trying to do. The compiler has almost caught DESIGN ERRORS at
compile-time!)
Another commonly heard statement is: "Sometimes you can tell WHAT A
FUNCTION DOES just by looking at its TYPE SIGNATURE."
This hints at why the first statement is true: If there really /is/ a
deep connection between what a piece of code does and what its type
signature says, then it makes sense that type-checking the program is
going to find a hell of a lot of bugs for you at compile-time.
But why does all this work in Haskell, and not in (say) C++ or Java or
VisualBasic?
The short answer is "parametric polymorphism".
The idea is pretty simple. If I'm moving some data from A to B, I don't
have to know OR CARE what type of data it is.
Let's consider a very simple example:
extract :: [x] -> x
This says that the "extract" function takes a list of values as its
argument, and returns one value as the result. The list can contain
values of ANY TYPE, and the value returned is of THE SAME TYPE as the
type of the list elements.
Let's consider implementing this function in C. Well, first of all, the
only way to implement "any type" in C is with a void pointer. (Or a
preprocessor macro, but that's just frigging EVIL!) So it would be a
function that takes a container of void pointers and returns a void pointer.
What might this function do? Well, it could return the first element of
the container. Or the last one. Or the middle one. Or the Nth one (if
there are N elements). But it could also do several other things:
- Query a global variable to decide which element to return.
- Return a null pointer.
- Call malloc to generate a new pointer [to gibberish].
- Pluck a random integer out of thin air, and cast it to a pointer.
- Examine the data pointed to, and decide what to do based on the bit
strings it finds there. [Obviously it can't know what they MEAN.]
- Modify the data pointed to.
- ???
- PROFIT!
In short, this function could do more or less /anything/.
Now let's consider the same thing in C++. Well, you could implement it
the same way as above, but more likely it would be a template function.
So what might that do? Well, again, it can return one of the elements of
the container. But it can also do things like conjure up some random
data and type-cast it to the result type. Or inspect global variables to
decide what to do. Or analyse the bit strings of the argument to decide
what to do.
I won't pretend to be a template expert, but as I understand it, a
template is allowed to call any function that exists. (With the proviso
that when the template is compiled, the result might not type-check.) So
our extract() function template might search the container for the
highest or lowest element (and fail to compile when the element type
doesn't support order comparisons).
C and C++ are both quite low-level languages. The emphasis is more on
allowing the programmer access to every possible ability of the
hardware, rather than on guaranteeing sane operation.
So how about Pascal? [Not that anybody writes production code in Pascal
any more.] Well, the situation is similar to C. [Not that every Pascal
dialect supports untyped pointers. If not, a few type casts will fix that.]
OK, so let's try Java. OK, well the closest Java can manage to "any
type" is the Object class. (If your data is a primitive type like int,
you'll have to wrap it in an object. Way to support efficient
primitives, Java! :-P ) Otherwise, the situation is much like C++. In
particular, you can downcast your objects to any class in the system.
Unlike C or C++, this is CHECKED at run-time, so it can fail. This
raises the possibility of trying lots of downcasts to figure out what
the actual class of the object is. C++ can do the same thing with
multiple templates.
Actually, Java has the reflection API, so you can actually /look up/ the
exact class at runtime. And look up what methods it has, and call one of
those. So here, you can /literally/ do /anything/!
So how about Haskell?
OK, well /obviously/ Haskell doesn't have global variables. So the
output of "extract" can /only/ depend on its input. And the output will
always be the same for a given input. But we know that already.
Haskell (or rather, GHC) /implements/ polymorphism using pointers. But,
much like Java, this isn't visible at the programmer level. (In
particular, no pointer arithmetic. No casting integers to pointers. No
allocating memory without knowing its type.)
But here is the huge, huge difference. I will say this very slowly:
Haskell DOES NOT HAVE type casts.
There is literally no way I can take some random garbage and cast it to
the correct result type. It's not possible. So the ONLY way to construct
a value of a specific type is... to know what that type is.
A polymorphic function has NO IDEA what type of data it is dealing with.
There is NO WAY to find out. Put simply, you cannot create data of a
polymorphic type.
And THAT means that "extract" cannot CREATE a result value out of
nothing. It has to OBTAIN one from somewhere. And since the only place
it has access to is the list passed in as an argument, the language 100%
guarantees that the result returned from "extract" is definitely one of
the elements of the input list.
In other words, the type signature of a function in C or C++ or Java or
whatever tells you next to nothing about what the function does. But in
Haskell, a function type can tell you WHAT THE FUNCTION DOES.
Notice that we don't know WHICH element extract returns. Maybe it's the
first one. Maybe it's the last one. Maybe its one in the middle. It
definitely ISN'T the lowest or highest element. You know why? Because
not all types have order comparisons, and the type signature doesn't
specify that the result type has order comparisons. Which means that
extract is not allowed to use comparison operators.
If we wrote
extract :: Ord x => x -> [x]
then extract WOULD be allowed to do order comparisons. So that would
tell us something ELSE about what the function does. (It doesn't HAVE TO
use order operators - but a "sensible" programmer wouldn't add an order
constraint unless the function actually requires one. Admittedly we're
now dealing with common sense rather than absolute proof...)
If I give you a value of type "x", the ONLY thing you can do with that
value is move it around and copy it. You cannot do ANYTHING ELSE with
it. You can't create new values of that same type. You cannot inspect or
alter the value I gave you. You cannot do anything, except move it around.
If I give you a value of type "x" and a function that takes type "x" as
argument, then you can apply the function to the value and do something
with the result. Or you can move the value and/or the function around a
bit. And that is all.
If I give you a value of type "x" which is a member of class "y", then
you can apply any method of class "y" to the value. (And move the value
around, as before.)
If I give you a value of type "Int", you can apply any function in the
system that expects Int values. (There are quite a lot of these.) But if
I give you a POLYMORPHIC type, then you were severely constrained in
what you can do with it. The above rules show you that.
Taking this into account, the following is impossible:
convert :: x -> y
This type signature says that "convert" accepts a value of ANY TYPE and
returns a value of ANY OTHER TYPE. This is quite impossible in Haskell.
Some people make the mistake of thinking that if a function returns a
polymorphic type, that means that THE FUNCTION can decide what actual
type it feels like returning. For example, in Java a method can return
"Object", and then the actual method code decides which subclass of
Object to actually return.
Haskell does not work like this. In Haskell, THE CALLER decides what the
return type should be, not THE CALLEE. This means that any function
returning a polymorphic type must be capable of generating ANY POSSIBLE
TYPE as result - and that is only possible if one or more of the
function's argument provide a way to generate such a value.
In a sense, every Haskell type signature is a logical theorem, and the
corresponding source code is the proof. And now I understand how: Each
type name (polymorphic or not) stands for the statement "this type is
inhabited". A type is "inhabited" if a value exists which has that type.
And the source code of the function is the "proof" in that it shows you
how to /construct/ such a value.
Consider again the type "x -> y". This type is uninhabited. It is
IMPOSSIBLE to construct a value (i.e., a function) with this type
signature. On the other hand, the type "x -> x" is inhabited. It has
exactly one inhabitant: the identity function.
The type signature "x -> y" can more simply be interpreted as "given
that X is true, it follows that Y is true". This is nonsense, since the
statements are unrelated. On the other hand, "x -> x" reads as "given
that X is true, it follows that X is true". Well, duh. Obviously.
Let's try the type signature for map:
map :: (x -> y) -> [x] -> [y]
Literally: "Given that there exists a function from X to Y and there
exists a list of Xs, it follows that there exists a list of Ys." Stated
in this language, it is /obviously/ true, and it is /obvious/ that the
source code for the map function constitutes a mathematical proof of
this statement - for it is a constructive proof!
(Anyone paying attention may have noticed that I said "x -> y" was an
impossible type, and yet that's the type of map's first argument! What
you have to understand is that every Haskell type implicitly has an
invisible "forall" over every type variable. Therefore,
forall x, y: x -> y
is an impossible type. However,
forall x, y: (x -> y) -> [x] -> [y]
is perfectly possible. The former demands a function that can turn any X
into any Y - an impossible feat. The latter says that IF there is a
function that can turn an X into a Y, THEN we can turn a list of Xs into
a list of Ys.)
Incidentally, here is an interesting thing: The map function is
polymorphic. But if I write, say, map toUpper, the toUpper function
accepts only characters and returns only characters. So clearly, the
next argument must be a list of characters, and the result must also be
a list of characters.
Basically, the FUNCTION may be polymorphic, but every CALL to the
function involves fixed types. If the calling function is itself
polymorphic, then you can trace that out to the next step. In summary,
if you take any valid Haskell program and analyse the entire program
text, you can always statically compute the exact type of everything in
the program.
In a sense, this is pretty damned similar to C++ templates. All the
polymorphism is at compile-time. As I understand it, C++ implements
templates by GENERATING new code for every combination of types that the
template is applied to. Haskell (or rather, GHC) doesn't implement it
that way. Instead, it dangles everything off of pointers. (Because,
let's face it, every pointer has the same structure.) But it COULD
implement it the way C++ does, and it would still work.
(Actually, there's a "specialize" pragma that makes GHC do exactly this,
although only for the requested types. For example, you might want to
optimise the map function when it's working on lists of integers.
There's no real benefit to that, but some more complicated function
might do something that benefits from a special-case.)
Post a reply to this message
|
|
|
|
On 10/05/2012 03:04 PM, Invisible wrote:
> Basically, the FUNCTION may be polymorphic, but every CALL to the
> function involves fixed types. If the calling function is itself
> polymorphic, then you can trace that out to the next step. In summary,
> if you take any valid Haskell program and analyse the entire program
> text, you can always statically compute the exact type of everything in
> the program.
>
> In a sense, this is pretty damned similar to C++ templates. All the
> polymorphism is at compile-time.
On closer inspection, this isn't *quite* true...
The counter-example I was shown is this:
wrap :: Show x => Int -> x -> String
wrap 0 x = show x
wrap n x = wrap (n-1) [x]
This is "polymorphic recursion". The function recursively calls itself
with a different type. Basically, it takes some data and wraps it in N
layers of lists. And since N can only be known at run-time, you can't
statically say how many times you need.
Actually, if you're paying attention, you'll notice that if N is
*negative*, this yields an infinite loop, requiring infinity different
type instanciations.
(And if you're *really* paying attention, you'll notice that Int has a
finite number of bits in it...)
This example is fairly stupid of course - why would you want to wrap a
value in a list of lists of lists? But it demonstrates an interesting
edge case.
Notice that since the final type of X is determined by N, the function
cannot *return* X, since there would be no way to write a sensible type
signature for that. It can only apply a polymorphic function to X and
return the result from that. (In this case, the "show" function, which
works for any degree of wrapping.)
IMHO, all of this is probably of theoretical interest only. I can't
imagine there being much practical use for it...
Post a reply to this message
|
|
null> wrote: