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

[dfe...@ccs.neu.edu]

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


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

Thanks again,
Dan



____________________
Racket Users list:
http://lists.racket-lang.org/users

[Matthew Flatt]

At Thu, 3 Apr 2014 02:49:23 -0400 (EDT), dfe...@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^`.

[Matthias Felleisen]

On Apr 3, 2014, at 9:04 AM, Matthew Flatt <mfl...@cs.utah.edu> wrote:

> 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

If you follow the Java precedent, it is somewhat useful to have
interfaces that define 'global' constants:

width = 10
height = width * 2
...

Same here. -- Matthias