Gregg Reynolds wrote:
On Mon, Feb 2, 2009 at 2:25 PM, Ketil Malde <ke...@malde.org> wrote:
Gregg Reynolds <d...@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
Tcon
Int.
Right. But then the set of values is isomorphic to the set of Ints,
right?
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|
etc
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.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
