[Haskell-cafe] Musings on type systems

[Matthew Steele]

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 <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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe