Re: Why would anyone want opacity?

[Michael R. Blair <ziggy@martigny.ai.mit.edu>]

> > These are facilities that I may or may not use.  Enforced static type
> > checking, by its definition is not optional.  Neither Gerry nor I will
> > object to new facilities that provide abilities not previously
> > present, at most we will ignore them.  We will reject facilities that
> > _remove_ abilities.
> 
> I simply don't think there are any abilities that are removed.  It is
> trivial to transliterate *any* Scheme program into an ML program.  You
> just have to insert the right injections and projections.  The outcome
> is a bit verbose, and all `type' errors in Scheme are turned into
> `Match' or `Bind' exceptions in ML.  Enforced static typing doesn't
> take anything away, it just makes it a bit harder to keep up certain
> habits.
> 
> Static typing gives you the ability to have your programs type-checked
> at compile time.  It doesn't take anything away.  With a suitable type
> system Scheme may also offer such.  So in the end it comes down to
> whether we believe static type checking should be the default or not.

[1] Will Clinger wants to use the exception system to extend generic
arithmetic.  For example, + is not defined on vectors. Will might choose a
vector representation of `surreal numbers' or he might want to implement
complex or rational numbers in a Scheme that currently does not have them,
again using vectors as a data type representation.

He might use the exception system to accomplish this.  So he would now
accept expressions like:

  (+ '#(1 2) '#(23 42))

...which your static type checking would presumably reject.  In fact, the
whole point of using the exception system to extend generic arithmetic is
that the _run-time_type_error_ signalling mechanism can be run-time
extended.


[2] Andy Berlin's master's thesis provided a partial evaluator for
arithmetic Scheme code by `advise'-ing the standard arithmetic primitives
to generate and propagate `symbolic values'--- that is, he effectively
used SET! to reassign things like `+' to accept symbolic values (pairs).

In a static type checking system like ML, this would presumably be verboten
since, in such a system, one cannot SET! a variable (like +) to anything
that is not type-equal to its default type (number x number -> number).

---

So what will you do about these in your static type checker, Matthias?

Would you forbid these programs being written this way?  Then you would
take away an ability Will and Andy currently have.

Would you not restrict assignment/rebinding of a variable (like `+') to
be type-consistent with the default system value?  Then this is not ML-style
static type checking.

Would you just define all the default system variables like `+' to be of
type `any' to permit this sort of re-binding?  Then everything would be
of unrestrained type and there would be nothing for you to check!

---

Please explain. Enquiring minds want to know.