TAPL is also a great book for getting up to speed on type theory:
http://www.cis.upenn.edu/~bcpierce/tapl/
I am no type theorist, and I nonetheless found it very approachable.
I've never read TTFP; I will have to check that out. (-:
On Nov 19, 2010, at 4:31 PM, Daniel Peebles wrote:
There's a lot of interesting material on this stuff if you start
poking around :) http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
might be a good introduction.
I'd consider typeclasses to be "sets" of types, as you said, but
more generally, a relation of types. In that view, an MPTC is just
an n-ary relation over types.
Yes, you can get arbitrarily deep on the hierarchy of types and
kinds. Agda does this, and even lets you define things that are
polymorphic on the "universe level".
If you do read through TTFP, you might want to follow along with
Agda, as it fits quite nicely.
On Fri, Nov 19, 2010 at 4:05 PM, Andrew Coppin <[email protected]
> wrote:
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...
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
