Re: [Haskell-cafe] type metaphysics

On Mon, Feb 2, 2009 at 2:25 PM, Ketil Malde wrote:

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