[Haskell-cafe] type metaphysics

[wren ng thornton]

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
>> 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