[Haskell-cafe] Musings on type systems
andrewcoppin at btinternet.com
Fri Nov 19 16:05:03 EST 2010
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
More information about the Haskell-Cafe