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