[Haskell-cafe] Musings on type systems

[Andrew Coppin]

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...