[Prev][Next][Index][Thread]
abstraction power
Jon, you claim that 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. I have put together just such a stack example below in
MzScheme. Our dialect of Scheme provides two things you won't find in
regular Scheme:
1. define-struct, which creates a new class of values every time it is
evaluated
2. units, which make nothing visible except for those things I wish to
expose.
[Note: Neither can be macro-expressed in Scheme (in my formal sense of
expressivenees). I conjecture that the two features are necessary to make
Scheme's data representations abstract but I don't have a proof that
Scheme by itself can't do it.]
My claim that the two representations are abstract doesn't mean that I have
a compile-time guarantee. Instead, it means that I have a run-time
guarantee that if you write a client unit, you can't tell which of the two
representations I am using. I can also slap a signature on it that actually
enforces the comments and will immediately nail the client or the server
unit if they break the contract.
I am paying the price via _abstract_ and _represent_ functions, but I never
claimed it would come for free.
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.
-- Matthias
;; SIGNATURES
(define-signature stackS
(empty ;; stack
push ;; stack num -> stack
pop ;; stack ->* num stack
empty? ;; stack -> bool
))
;; IMPLEMENTATION UNITS:
(define stack1
(unit/sig stackS (import)
;; a mechanism for setting up the abstraction
(define-struct stack (val))
(define abstract make-stack)
(define represent stack-val)
;; the concrete representation
(define empty (abstract '()))
(define (push s e) (abstract (cons e (represent s))))
(define (pop s)
(let ((s (represent s)))
(if (null? s)
(error 'pop "the stack's empty")
(values (car s) (abstract (cdr s))))))
(define (empty? s)
(null? (represent s)))))
(define stack2
(unit/sig stackS (import)
;; a mechanism for setting up the abstraction
(define-struct stack (val))
(define abstract make-stack)
(define represent stack-val)
;; the concrete representation
(define empty
(abstract
(lambda (x)
(if x
#t
(error 'pop "the stack's empty")))))
(define (push s e)
(abstract
(lambda (x)
(if x
#f
(values e s)))))
(define (pop s)
((represent s) #f))
(define (empty? s)
((represent s) #t))))
;; LINKING and TESTING
(define (tester stack-unit)
(invoke-unit/sig
(compound-unit/sig
(import)
(link
[STACK : stackS (stack-unit)]
[TEST : () ((unit/sig () (import stackS)
(define t (push empty 0))
(define-values (e s) (pop t))
(values (= e 0) (empty? s)))
STACK)])
(export))))
(tester stack1)
(tester stack2)