[Haskell-cafe] Musings on type systems

[Daniel Peebles]

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 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20101119/aba782fe/attachment.html