OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of "set", and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has "algebraic data types". "Algebraic" because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or "sum" of the types X and Y. So is Either what is meant by a "sum type"? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has "product" in the name. So is this a "product type"? So not only do we have "types" which denote "sets of possible values", but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (->) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single-parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a "closed" set. A type, on the other hand, is an "open" set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) => Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) "Container". So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the "type" keyword). It's not quite the same as a "newtype", since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have "kinds". As best as I can tell, kinds exist only to distinguish between /types/ and /type functions/. For type constructors, this is the whole story. But for associated types, it's more complicated. For example, Element :: * -> *, however the type argument is statically guaranteed to belong to the Container set (class). In other news... my head hurts! >_< So what would happen if some crazy person decided to make the kind system more like the type system? Or make the type system more like the value system? Do we end up with another layer to our cake? Is it possible to generalise it to an infinite number of layers? Or to a circular hierachy? Is any of this /useful/ in any way? Have aliens contacted Earth in living member? OK, I should probably stop typing now. [So you see what I did there?] Also, I have a sinking feeling that if anybody actually replies to this email, I'm not going to comprehend a single word of what they're talking about...