[Haskell-cafe] type metaphysics

[Gregg Reynolds]

Hi Martijn,

On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen <
martijn at van.steenbergen.nl> wrote:
>
> There are many answers to the question "what is a type?", depending on
one's
> view.
>
> One that has been helpful to me when learning Haskell is "a type is a set
of
> values."

That's the way I've always thought of types, never having had a good reason
to think otherwise.  But it seems it doesn't work - type theory goes beyond
set theory.  I've even found an online book[1] that uses type theory to
construct set theory!  At least I think that's what it does (not that I
understand it.)

>> This gives a very interesting way of looking at Haskell type
>> constructors: a value of (say) Tcon Int is anything that satisfies
>> "isA Tcon Int".  The tokens/values of Tcon Int may or may not
>> constitute a set, but even if they, we have no way of describing the
>> set's extension.
>
> Int has 2^32 values, just like in Java. You can verify this in GHCi:
>

Ok, but that's an implementation detail.  My question is what is the
theoretical basis of types.

Notice that the semantics of Haskell's built-in types are a matter of social
convention.  The symbols used - Int, 0, 1, 2, ... - are well-known, and we
agree not to add data constructors.  But we could if we wanted to.  Say, Foo
::  Int -> Int.  Then Foo 3 is an Int, distinct from all other Ints; in
particular it is not equal to "3".

I suspect a full definition of type would have to say something about
operations.

>> To my naive mind this sounds
>> suspiciously like the set of all sets, so it's too big to be a set.
>
> Here you're probably thinking about the distinction between countable and
> uncountable sets. See also:
>

It could be that values of a constructed type form an uncountably large set,
rather than something too big to be a set at all. I'm afraid I don't know
how to work with such critters.

In any case, the more interesting thing (to me) is the notion that sets
contain their members "essentially", but data types don't, as far as I can
see.

Thanks much,

gregg


[1] http://www.cs.chalmers.se/Cs/Research/Logic/book/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/8680a5b4/attachment.htm