[Haskell-cafe] Musings on type systems

[wren ng thornton]

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