Re: Why would anyone want opacity?

[Matthias Blume <blume@CS.Princeton.EDU>]

From: "Guillermo J. Rozas" <gjr@martigny.ai.mit.edu>
Subject: Re: Why would anyone want opacity?
Date: Thu, 9 May 96 19:22:54 -0400

> What is a pointer?  Scheme has no such beast.  Scheme has objects.
> Implementations may represent objects as pointers, but that is
> architecture-dependent, and pre-supposes an implementation, so it does
> not apply to blackboard/pen-and-paper discussions.

Well, this is indeed so, but only because we have already gotten used
to the underlying abstraction.  In the beginning there was the pointer
-- worse -- there was the `Content of the Address part of the
Register' and the `Content of the Decrement part of the Register'.  We
have accepted the abstraction from such low-level things, and we have
taken advantage of it -- now being able to represent values and
objects by other means than pointers.

This clearly demonstrates the *usefulness* of abstraction.

> As an aside, several _implementations_ allow poking at the bits of the
> pointers that represent objects.  It is extremely useful when building
> hash tables and other system-level stuff.

I wouldn't use the qualifier `extremely' here, rather `perhaps, in
some cases'.  Anyway, as soon as you allow such low-level manipulation
you can NOT freely choose the representation of values and objects
anymore.  You have to be careful with your copying collector, because
it moves objects around and changes the underlying pointers.  Breaking
the abstractions always seems to have negative long-term effects, no
matter how useful they might appear to be in the short run.

> 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.

> Gerry is not arguing against abstraction.  He is arguing against
> building spelling checkers into languages.  They are useful, but as
> tools.

No, this is not the correct metaphor.  Lexical and syntax analysis
(which amount to spell-checking) are there even in Scheme.  What Gerry
objects to is a set of rules that let you decide statically (by just
looking at the sentence), whether it makes sense or not.  He prefers a
system where we find out by `running' the sentence.  He would find out
that `At night it is cooler than outside.' doesn't make much sense
only when his audience starts making funny faces.  Or, we would only
realize that it isn't a good idea to insult our mother when we do so
and she gets very upset.  (Mind you, I don't think ML type checking
would catch the latter. :-)

> For example, Scheme has this nice property that a LET is just
> syntactic sugar for a combination with a LAMBDA expression as the
> operator.

What is this `nice' property good for?  Actually, I think it should be
dropped.  I envision a LET construct (in Scheme), which can bind
(mutable) variables, constants, macros, and (perhaps) types.  The
correspondence with LAMBDA only holds if there is one kind of binding
(variables) that one can introduce with LET.  Which is why we need a
*separate* LET-SYNTAX in current proposals for macro systems.  So we
reduce LET to an application of LAMBDA, but we do so at the cost of
having to use *another*, new syntactic construct, for which there is
no rewrite rule into core language constructs.

> Thus adding an ML-style type discipline would remove an ability that I
> now have.  In particular, I wold have a heck of a time writing some
> macros because I would have to take into account whether the checker
> would find them legal one way but not another.  You call this freeing
> me of something?

This is indeed an interesting topic -- marrying macros with
types. Definitely worth some research.

> Static types do not add any new functionality.  They remove the
> ability to express programs that make perfect sense at the dynamic
> semantics level, just because they do not make sens at the static
> semantics level when you've imposed a particular type discipline.

But how many times do you write correct Scheme programs that can't be
typed in ML (after perhaps some minor, straightforward modifications)?
I found, that whenever I was wrestling with ML's type system I
eventually discovered a serious design flaw in my program.  Of course,
this is just a bit of personal, experimental evidence, and things
might work differently for other people.  All I am saying is: it works
for me, and very well so.

> If you find them useful for your thinking, you can use them, and you
> are welcome to do so.  I may even do so on occasion.  However, they do
> not add new concepts/ability in the dynamic semantics.

I never claimed they would add anything new to the dynamic semantics.
That was never the point.

> |   I know, you think that types are actually hindering you in your design
> |   efforts.  Apparently, different people think differently, because I
> |   found that often there is a remarkable coincidence between ``getting
> |   the design right'' and ``getting the types right''.
> 
> That must mean that you are only dealing with statically decidable
> properties in your programs.  How boring. :-)

I sure hope I do.

> Your argument is like saying the following:
> 
> Using a car imposes an abstraction on you.  You are being inconsistent
> by accepting this imposition while you do not accept restrictions to
> freedom of speech.

Well, for one thing, I do not believe in absolute freedom -- not even
of speech.  (This might shock you, but I think it is a good thing that
now in my country Nazi propaganda, inciting racial hatred, etc. are
prohibited by law.  -- But be careful. I do not want to compare
dynamic typing to incitement of racial hatred here. :-)

-Matthias