[Prev][Next][Index][Thread]

Re: abstraction power

Matthias,

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. 

but said

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

-Jon

--------------------------------------------------------------------------
signature STACK =
sig
  type stack
  exception EmptyStack
  val empty : stack
  val emptyP: stack -> bool
  val push  : stack * int -> stack
  val pop   : stack -> int * stack
end


structure Stack : STACK =
struct  
  type stack = exn

  exception S of int list
  exception EmptyStack

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