[Prev][Next][Index][Thread]
Re: type safety
Matthias,
I struggled with myself: should I respond or shouldn't I?
You make some good points about the differences between types and
safety, but I fear that the point-of-view is bound too closely to
the Scheme implementation model. Most importantly, it presumes
that the set of values for each operation CAN be divided into
"good" and "bad". That is certainly the case when all values come
with tags saying whether they're an integer, a procedure, an
atom, but it may not, and need not, always be the case.
I agree with you that types are a syntactic discipline, but I take
my cue from John Reynolds' paper "Types, Abstraction, and
Parametric Polymorphism". In that paper, Reynolds' thesis is
Type structure is a syntactic discipline for enforcing
levels of abstraction.
The fact that they enforce abstraction is CRUCIAL. When one has
such a notion, one can freely mix values that happen to have the
same representation. For instance, it's not hard to conceive of a
language which uses integers to represent pointers to lists and
integers themselves. A static type system makes sure the compiler
generates the right code, and that the code never mixes the two
representations in unexpected ways.
I believe this point-of-view separates "dynamic" and "static"
notions of typing. Of course, it also supports the viewpoint that
types give some means of safety. I just don't believe that
providing some notion of safety (necessarily weak, as you
correctly point out) is all that there is to types.
Best,
-Jon