[Haskell-cafe] type metaphysics

[Ketil Malde]

Gregg Reynolds <dev at mobileink.com> writes:

> 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