[Haskell-cafe] type metaphysics

[Lennart Augustsson]

Thinking of types as sets is not a bad approximation.  You need to add
_|_ to your set of values, though.

So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}

2009/2/2 Gregg Reynolds <dev at mobileink.com>:
> 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/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>