[plt-dev] compound units and contracted signatures

Philippe,

> - I think it would be nice to get rid of the "imports cannot be
>  exported" restriction.  It looks to me like it only forces one to do
>  extra gymnastic with things like same-t? and I'm not sure what the
>  benefit of the restriction is.  And if I have several imports that I
>  want to re-export to use in the contracted signature s^ then using
>  something like (define same-t? t?) multiple times becomes rapidly
>  ugly.

The reason you can't export your imports is to prevent direct cycles
in definitions.  Consider U@ that imports x and exports it as y, and
V@ that imports y and exports it as x.  Linking U@ and V@ to form W@
results in a unit that exports x and y, neither of which has a
definition at all.

> - It's a bit annoying that I have to have t? listed in both t^ and s^:
>
>  (define-signature t^
>    ((contracted (t? (any/c . -> . boolean?))
>                 (make-t (symbol? . -> . t?)))))
>
>  (define-signature s^
>    (t? ; already contracted in t-sig.ss
>     (contracted (wrap-make-t (symbol? . -> . t?)))))
>
>  and that I have to remember that the t? in s^ should not be
>  contracted a second time.  It would be nicer to be able to simply
>  define s^ as:
>
>  (define-signature s^
>    ((contracted (wrap-make-t (symbol? . -> . t?)))))
>
>  and then have a compound-unit-with-contracted-signatures form that
>  would automatically bind the t? used in s^ with the t? contracted in
>  t^ when the different pieces of the compound unit are put together.
>  Any chance of having something like this in the future? :-)

I don't think either of your formulations -- importing t? from t^ and
directly re-exporting it via s^, or simply leaving t? "free" in s^ --
express quite what I read from your code.  It looks like you
explicitly want wrap-make-t to share the same contract as make-t: they
both map symbols to Ts, for the same notion of T.

In the first case (t? in both s^ and t^), it would be trivial to write
an implementation of s@ that exported an entirely different t? in s^
than it imported from t^.  Thus make-t and wrap-make-t would actually
have completely different output types, and their results would not be
usable in the same context.  You need a sharing constraint as in ML
modules: the specification of make-t and wrap-make-t need the same T.

In the second case (t? free in s^), you get "the same" t? as anything
else you link to, but there's no guarantee in the signature that what
you link to is t^.  A client unit may import t^ and s^ and try to use
make-t along with wrap-make-t... only to find that the imported s^ was
actually constructed by linking with u^, which has a t? used for an
entirely different purpose.  Here, t? is shared, but with the wrong
other thing.

Stevie tells me there is currently no analogous feature to "sharing
constraints" in unit contracts, but that he and Matthias are aware of
the issue and considering several options for resolving it.  For now
you're probably stuck with the encoding you chose, but they're working
on improving it.

-- 
Carl Eastlund