evan_tech

Previous Entry Share Next Entry
09:33 pm, 23 Jan 04

type systems atop type systems

My pasttime recently has been to try to read "A Gentle Introduction To Haskell" because if I want to be a type system geek, I really ought to understand Haskell. Half the papers I see use it, and it's got a bunch of neat stuff ML lacks. It's sorta what you'd expect researchers to produce: elegant and powerful, but (for example) strings really are lists of characters so you get the associated performance penalty. OCaml's been treating me well because it's a mix of fancy and fast (OCaml strings, for example, are special-cased), but I need to branch out.

The section on type classes has been giving me trouble, particularly the bit about functors, but I think I get it now.

Suppose you have a parameterized datatype, like a List of [x]s. The C++ way of using it would be like List<int> x = ...;.
What is a List? It's not a type, because you can't use it directly. One way to look at it is that it is a function from types to types: you give it a type (int) and it gives you back a type (List of int). You can imagine even more complicated types.
We call this description—"function from types to types"—its kind, much in the way "type" is a way of describing a function from integers to integers.
In a pure language like Haskell, there is only one basic kind, which they call *. All concrete types (ints, chars, functions, etc.) are of this kind. Then we have stuff like our List, which takes a concrete type (int) and gives you back a concrete type (List of int), so that is of kind *->* much like functions are written int->int.

From their doc:
As we know, the type system detects typing errors in expressions. But what about errors due to malformed type expressions? The expression (+) 1 2 3 results in a type error since (+) takes only two arguments. Similarly, the type Tree Int Int should produce some sort of an error since the Tree type takes only a single argument. So, how does Haskell detect malformed type expressions? The answer is a second type system which ensures the correctness of types! Each type has an associated kind which ensures that the type is used correctly.
Fancy!



Ok, that's all complicated and mysterious, but it even applies back to normal C-land:
C has more than one basic kind, and we even are totally comfortable using a type function from one kind to another!
Consider this (perfectly normal C this time):
struct _F;  /* F is abstract! */
typedef struct _F F;  /* simplify below examples. */
...
int x;  /* legal; int has the common kind. call it C for concrete */
F foo;   /* illegal!   F is a type, but it is of a different kind than int.
           call it A for abstract */
F* bar;  /* legal!   "*" in a type declaration is a suffix function from A->C. */

(Of course, you can also write int* y, which calls * with a C argument. So C must be a subtype of A.
And this probably isn't fully right, because dereferencing bar from above is a compile-time error. But hopefully you get the idea.)


PS: Does anybody read and understand this? I'd hate to bore y'all.