[racket] Confused about define-values(-for-export) forms in define-signature

At Thu, 3 Apr 2014 02:49:23 -0400 (EDT), dfeltey at ccs.neu.edu wrote:
> > A `define-values` in a signature adds a definition to any *importing*
> > context (in contrast to `define-values-for-export` which adds a
> > definition in any *exporting* context). The `define-values/invoke-unit`
> > form "imports" the signature into the definition context.
> 
> I reread the documentation for define-values/invoke-unit and it makes a bit 
> more sense after reading that the export clause gets treated as an import to a 
> local definition context, but I don't really understand why this is the right 
> thing to do. This seems to differ from simply invoking a unit with the `invoke` 
> form which doesn't need exports to be listed explicitly. Why should the exports 
> be treated as imports in a local definition context, this just seems 
> contradictory to the meaning of exports.

One context's exports are another context's imports.

When you write

 (define-values/invoke-unit y@ (import) (export y^))

then the intent is to import into the enclosing context all of the
bindings that are exported by `y@`. The `(export y^)` part says that
`y@` is expected to export `y^`; so, anything listed in `y^` is
imported into the definition context.

The `invoke` form is something like `(dynamic-require <mod> #f)` at the
module level. That is, `invoke` instantiates a given unit where you
don't care to use the unit's exports, and so it doesn't bind anything.

> >> Since the y^ signature is being exported instead of imported I expected 
> >> that the value of y should not be available in the y@ unit, and furthermore 
> >> there is no need to declare y in the signature as a variable which the unit 
> >> must define. So why is it the case that this unit defines and exports the 
> value 
> >> of y, when according to the documentation this shouldn't happen.
> 
> > As you say, `y` isn't bound in the unit `y@` by the export of `y^`.
> 
> > With the `define-values/invoke-unit` form in the same context, though,
> > the unit `y@` will be able to refer to `y`, just like any other binding
> > in the unit's environment.
> 
> 
> I can understand how `define-values/invoke-unit` adds a definition for `y` in a 
> local context that the `y@` unit can then refer to, but since the unit doesn't 
> export `y` through an exported signature I don't see why this generates a 
> global binding for `y`? I would expect only the exports of the unit should be 
> added as new bindings, I think this is what the docs say, but since `y@` 
> doesn't export any values there should be no new bindings added.

If you have

 (define-signature y^
  [y])

and assuming `y@` that exports `y^`, then hopefully it's now clear why

 (define-values/invoke-unit y@ (import) (export y^))

binds `y` in it's definition, context.

The way to read

 (define-signature y^
  [(define-values (y) 5)])

is that it's the same as the original `y^`: an implementation of `y^`
provides a binding for `y`. But this latter `y^` directly defines the
`y` binding that all implementations provide (so that the
implementations of `y^` don't actually need to implement `y`).

In other words, defining a variable in a signature is a lot like
defining a method in an Java interface. Defining `y` as a constant is
not especially useful, but something like

 (define-signature arith^
   [plus
    minus
    zero
    (define-values (negate) (lambda (n) (minus zero n)))])

might be useful to implement (and enforce) a relation among `negate`,
`minus`, and `zero` in an implementation of `arith^`.