[Haskell-cafe] type metaphysics
Ketil Malde
ketil at malde.org
Mon Feb 2 13:39:44 EST 2009
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
More information about the Haskell-Cafe
mailing list