[Haskell-cafe] type metaphysics
wren ng thornton
wren at freegeek.org
Tue Feb 3 21:05:08 EST 2009
Gregg Reynolds wrote:
> On Mon, Feb 2, 2009 at 2:25 PM, Ketil Malde <ketil at malde.org> wrote:
>> Gregg Reynolds <dev at mobileink.com> writes:
>>> Just shorthand for something like "data Tcon a = Dcon a", applied to Int.
>>> Any data constructor expression using an Int will yield a value of type
>> Right. But then the set of values is isomorphic to the set of Ints,
> The values constructed by that particular constructor, yes; good point.
> Isomorphic, but not the same. (And also, if we have a second constructor,
> what's our cardinality? The first one "uses up" all the integers, no?
No. If we have the type (Either Integer Integer) we have W+W values.
There's a tag to distinguish whether we chose the Left or Right variety
of Integer, but having made that choice we still have the choice of any
Integer. Thus, this type adds one extra bit to the size of the integers,
doubling their cardinality.
Which is why ADTs are often called "sum--product types". Replacing
products and coproducts with, er, products and summations we can talk
about the cardinality of types (ignoring _|_):
|()| = 1
|Bool| = 1 + 1
|Maybe N| = 1 + |N|
|(N,M)| = |N| * |M|
|Either N M| = |N| + |M|
Really we're just changing the evaluation function for our ADT algebra.
Extending things to GADTs, this is also the reason why functions are
called exponential and denoted as such in category theory:
|N -> M| = |M| ^ |N|
That's the number of functions that exist in that type. Not all of these
are computable, however, as discussed elsewhere.
More information about the Haskell-Cafe