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

...

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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 19 November 2010 22:14, Albert Y. C. Lai wrote:

On 10-11-19 04:39 PM, Matthew Steele wrote:

...

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.

TAPL is surprisingly easy-going. It is long (many pages and many chapters, each chapter short), but it is the good kind of long: long but gradual ramp to get you to the hard stuff. Its first chapter explains convincingly why you should care about types to begin with (summary: a lightweight formal method).

But it is not entirely for Haskell. It covers subtyping, and it doesn't cover type classes.

It is also too bulky to be mobile (because it's long).

IIRC It Does not deal Hindley-Milner type system at all. i.e. it does not cover ML's type system. Its successor ATTAPL :- http://www.cis.upenn.edu/~bcpierce/attapl/index.html Handles an ML like type systems using constraints. AFAICT This area area of type theory's history is not covered properly in any of the sources I have came across. Aaron

On 11/19/10 10:05 PM, Ryan Ingram wrote:

On Fri, Nov 19, 2010 at 1:05 PM, Andrew Coppin wrote:

...

So is Either what is meant by a "sum type"? Similarly, (X, Y) [...] is this a "product type"?

Yes and no. Unfortunately there's some discrepancy in the terminology depending on who you ask. In the functional programming world, yes: sum types are when you have a choice of data constructors, a la Either; and product types are when you have multiple arguments in a data constructor, a la tuples.[1] However, in set theory and consequently in much of the research on dependent types, (the dependent generalization of) function types are called ``(dependent) product types'' and (the dependent generalization of) tuples are called ``(dependent) sum types''. There's a convoluted story about why this supposedly makes sense, but it doesn't match functional programmer's terminology nor the category theoretic terminology which is often invoked in type theory. ObTangent: this is much like the discrepancy between what is meant by ``source'' and ``target'' for folks who come from a machine learning background vs people who come from a signal processing background. Thankfully, most of the NLP folks caught in the middle have decided to go with the sensible (ML) definitions. [1] In a lazy language like Haskell we have to be careful about how we phrase this. There are different notions of products[2] depending on how they behave with respect to strictness, and depending on which one you choose you'll change how you have to reason about the types abstractly. This shows up canonically in the difference between domain products and smash products. When Haskell was designed they decided not to have two different versions of products in the language, so the tuples in Haskell aren't either of these two well-behaved kinds of products. This has ramifications when people try to reason about which program transformations are valid without introducing too much or too little laziness. By and large Haskell's tuples and ADTs are good at doing what you mean, but they do complicate the theory. [2] The same is true for different kinds of sums, but that's less problematic to deal with.

...

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.

Sort of, but I think your discussion later gets into exactly why it *is* fundamentally different.

There are a few different ways to think about functions/arrows, which is why things get a bit strange. In functional programming this is highlighted by the ideas of ``functions as procedures'' vs ``functions as data'' ---even though we like to ignore the differences between those two perspectives. In category theoretic terms, those ideas correlate with morphisms vs exponential objects (or coexponential objects, depending). There's a category theoretic relation between exponentials and products (i.e., tuples) which is where un/currying comes from. But this is also why the Pi- and Sigma-types of dependently typed languages cause such issues. For example, there's an isomorphism between A->(C^B) and (A*B)->C in certain categories, namely curry/uncurry. And there's also an isomorphism between A*B and B*A, namely swapping the elements of a pair. Together these mean, A->(C^B) ~= (A*B)->C ~= (B*A)->C ~= B->(C^A). In Haskell this is obviously true because we have Prelude.flip. However, if we generalize this to dependent functions and dependent pairs then it's no longer true in general, because B may require an A to be in scope in order to be well-kinded; e.g., assuming f : (a:A) -> (b: B a) -> C a b, then what is the type of swap f? So on the one hand arrows and products are just type constructors like any other, but on the other hand they're not. It's sort of like how zero and one are natural numbers, but they're specialer than the other natural numbers (you need them in order to define the rest of Nat; they have special behavior with respect to basic operations like (+), (*),...; etc). ObTangent: When we dualize things to co-Cartesian closed categories we get the same thing, except it's between sums/coproducts and coexponentials.

...

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.

Well, I find it's better to think of GADTs as types that have extra elements holding proofs about their contents which you can unpack.

Ultimately, GADTs are just a restricted form of Pi- and Sigma-types. The type argument whose value varies depending on the constructor isn't actually a phantom type. You can think of there being four sorts of type variables. There are the variables for parametric polymorphism where the _same_ variable occurs on both sides of the = defining the type. There are phantom types where the variable only occurs on the left. There are existential types where the variable only occurs on the right. And there are dependent types which are like a combination between phantom variable on the left, an existential variable on the right, and an equality constraint relating the left variable to the right variable. -- Live well, ~wren

On 20 November 2010 12:05, Tillmann Rendel wrote:

I would expect the "exponential type" to be (a -> b):

Terminologically, "Bananas in Space" (!) agrees with you. http://www.cs.nott.ac.uk/~gmh/bananas.pdf Regards Stephen

On 21/11/2010 8:33 PM, wren ng thornton wrote:

On 11/20/10 6:33 AM, Ketil Malde wrote:

...

I guess this makes [X] an exponential type, although I don't remember seeing that term :-)

Nope. (a->b) is the exponential type, namely |a->b| = |b|^|a|.

[_] is just a solution to the recursive equation [x] = 1 + x*[x].

So that [X] correspond to the 'type' 1/(1-X). This is sometimes called the 'asterate' in other contexts, since it corresponds to the Kleene star. The nice thing about the 'asterate' is that it exists for many many semi-rings -- and one can use it as a replacement for both 'minus' and 'exact division' in the Gaussian Elimination algorithm. Jacques