[Haskell-cafe] type metaphysics

[Gregg Reynolds]

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?
Since we can define "aleph" constructors, each of which can yield "aleph"
values, well that's a lot of values.)


>
> >> I don't follow this argument.  Are you saying you can remove a
> >> data constructor from a type, and still have the same type?  And
> >> because of this, the values of the type do not constitute a set?
>
> > Yep.
>
> I don't see why you would consider it the same type.  Since, given any
> two data types, I could remove all the data constructors, this would
> make them, and by extension, all types the same, wouldn't it?
>

I don't think so; considered as sets, they have different intensions, and
considered as predicates, they're clearly distinct even if there are no
objects.  Different names (descriptions), different things, unless we
declare they are equal.

You would probably find "When is one thing equal to another thing", by Barry
Mazur (at http://www.math.harvard.edu/~mazur/<http://www.math.harvard.edu/%7Emazur/>).
A fascinating discussion of equality in the context of category theory.  See
also "On Sense and Intension" at http://consc.net/papers.html

-gregg
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090203/dea78e33/attachment.htm