Re: abstraction power
Subject: Re: abstraction power
From: Jon Riecke <email@example.com>
Date: Sat, 01 Jan 2000 16:42:04 -0500
In-reply-to: Your message of "Thu, 30 Dec 1999 21:31:00 CST." <200001011544.KAA01910@localhost.localdomain>
I liked your example, even though I do not have the details of how
your additions to Scheme work here at home. The concept of
"generativity" may be more fundamental than static type checking.
Nevertheless, I did not understand the following paragraph:
> Finally, I believe that there is a bit of power there that ML doesn't
> have. ML's generative datatype is close to this idea BUT you can't comingle
> values of identical looking datatype and break them open. As you say, the
> type system (now) enforces that this can't happen. But the real reason is
> that you can't even have the two sets of values live in the same extend and
> scope. We can. Now I don't know of a good practical example right now, but
> I can write "poems" that you can't.
People who are familiar with the papers comparing the expressive
power of exceptions and continuations (Lillibridge's paper and my
paper with Thielecke) know that ML does have a feature that allows
one to mix values in a single datatype: it's called "exn". I've
coded up your first implementation of stacks in Standard ML (the
code is below), and the other looks easy too. Does this resemble
your implementation in MzScheme? Are there examples in MzScheme
that couldn't be done in this style?
If you agree that this follows the style of your MzScheme code,
then it seems that ML and MzScheme are quite close: ML has a type
for the "universal type", and MzScheme allows one to protect and
segregate values in the "universal type" from each other.
I would be curious to hear from the "dynamically typed" OO
community as well. It seems to me that this kind of generativity
occurs there as well.
Finally, let's agree to be careful about claims/counterclaims. I
did not say
> in a UNItyped language you can't represent stacks in
> two different ways so that there is no way to break the abstraction from
> the outside.
> The bottom line: a system is a type system if it allows one to
> enforce abstractions. I'm open to examples, but I don't know of
> an example of a purely dynamic "type system" that allows
> representation independence-like properties.
It was a challenge, not a blanket claim.
signature STACK =
val empty : stack
val emptyP: stack -> bool
val push : stack * int -> stack
val pop : stack -> int * stack
structure Stack : STACK =
type stack = exn
exception S of int list
fun abstract lst = S lst
fun represent (S lst) = lst
val empty = abstract 
fun emptyP s = null (represent s)
fun push (s,e) = abstract (e::(represent s))
fun pop s = let val lst = represent s
in case lst of (x::rst) => (x,abstract rst)
| _ => raise EmptyStack