Gregg Reynolds
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".
Reminiscent of arguments between dynamic and static typing camps - as far as I understand, a "dynamic type" is just a predicate. So division by zero is a "type error", since the domain of division is the type of all numbers except zero. In contrast, I've always thought of (static) types as disjoint sets of values.
My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type).
I guess I don't quite understand what you mean by "Tcon Int" above. Could you give a concrete example of such a type?
To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set.
I suspect that since types and values are separate domains, you avoid the complications caused by self reference.
In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially.
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? I guess it boils down to how "Tcon Int" does not depend on any particular constructor. -k -- If I haven't seen further, it is by standing in the footprints of giants