[Grace-core] Grace feedback

[Andrew P. Black]

On 8 Nov 2010, at 0:46, James Noble wrote:

>> However, I don't know how to do ADTs without types.  ADTs fundamentally need types to achieve the encapsulation
> 
> sure - but these could be static types or dynamic types...

The "Greek types guys" would make you wash your mouth out with soap for uttering such a statement!  Yes, you can do encapsulation with dynamic tag checking, but there is significant overhead to this, and it is surprisingly tricky.   Morris' original  "Types are not Sets" paper did something like that, as did CLU (with in and  out operations).  The problem, IIRC, is to allow the same operations to be used from inside the ADT as well as from outside the ADT with a clean semantics and excessive run-time checks or conversions.  Anyway, round about 1990 [1] the Greek types guys figured out that existential types could do ADTs with no run-time cost.  I'm sure that Kim knows the details of this better than I do.

Anyway, I'm assuming that we are not going down this path, and that we are staying committed to the one true object model.    Comparing ADTs and Objects is a nice topic for a PL concepts course in year 4; I think that the way to teach this is to compare Grace to another language, like ML or Haskell, that does ADTs.

>> One thing that we have not discussed is whether there should be some sort of "protect" or "narrow" operation that hides some operations on an object from certain clients, while exposing them to other clients.
> 
> right - so long as those restrictions are checked dynamically if necessary,
> and the static restrictions are no stronger than the dynamic ones,

The reason that one needs protect is EXACTLY to impose a more restrictive regime dynamically.  The normal case is that the dynamic regime is more permissive than the static one — that's why people want dynamic checking.  

For example: the static type system says that s is a stream.  s is actually (dynamically) a fileStream.    This means that with dynamic checking, an attempt to do a seek will succeed, but with static checking, it will fail.

Narrowing would let someone "hide" the extra operations (like seek) on s.  So
	
	let f = restrict s to Stream

makes f an object of type Stream that cannot later be dynamically widened back to FileStream.

Incidentally, this means that f can't be egal to s; they understand different sets of operations, so they are not observationally equivalent.

	Andrew

[1] Checking the reference, it was a bit earlier:

@article{mitche1988,
	Author = {Mitchell, John C. and Plotkin, Gordon D.},
	Journal = {TOPLAS},
	Number = {3},
	Pages = {470 - 502},
	Title = {Abstract Types Have Existential Type},
	Volume = {10},
	Year = {1988}}