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

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

We call this descriptionâ€”"function from types to types"â€”its

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

From their doc:

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):

(Of course, you can also write

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.

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.

33mhzI sat up and took notice 'cause "A Gentle Introduction to Haskell" is a strongly recommended optional reading for my current Programming Languages class for when we get to the section on functional programming (which is gonna focus on Haskell as its main language for code samples).

I got some exposure to Haskell last semester in the form of a small programming assignment, but I didn't really end up liking it too much. Hopefully I'll get a better handle on it this time around.

mulixI read it, and I mostly understand it, but I don't usually have time to follow through on it (or sadly even comment). Do go on...

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

Yup. Although I don't understand what's so spiffy about not knowing the size of an undefined struct, but actually knowing the size of a pointer to it. Seems pretty basic. Just try to get a compiler to allocate memory for that!

zezuraevnosex_snej373And every time you mention OCaml it refreshes my interest in learning it. I've still got that tutorial for C programmers bookmarked. Sigh! I'm not even good at Ruby yet!