[Haskell-cafe] Musings on type systems
mdsteele at alum.mit.edu
Fri Nov 19 16:39:20 EST 2010
TAPL is also a great book for getting up to speed on type theory:
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 <andrewcoppin at btinternet.com
> > 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
> 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
> Haskell-Cafe at haskell.org
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe