[plt-dev] compound units and contracted signatures

On Tue, May 19, 2009 at 10:33 PM, Philippe Meunier <meunier at ccs.neu.edu> wrote:
> Carl Eastlund wrote:
>>The reason you can't export your imports is to prevent direct cycles
>>in definitions.
>
> Okay, but IMHO the cure might be worse than the disease.  I have a
> program with seven units, and three of them have to re-export some
> imports (two out of these three cases are because of contracted
> signatures) and all the (define same-t? t?) followed by renames of
> same-t? into t? in unit exports are a bit of a pain.  Just saying :-)

The cure predates the disease, in this case.

>>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.
>
> Yes.
>
>>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.
>
> Yes, but see below.
>
>>You need a sharing constraint as in ML
>>modules: the specification of make-t and wrap-make-t need the same T.
>
> Yes.  That's why I'm suggesting something like
> compound-unit-with-contracted-signatures where the sharing constraint
> would be implicitely specified based only on the names used in the
> signatures.  I believe that in the vast majority of cases this would
> just be the right thing to do, since in practice people do not tend to
> to use the same names for different data structures.
>
> If, as in your example above, two units exported incompatible t?
> predicates, then either compound-unit-with-contracted-signatures would
> fail at expansion-time with a message like "two units export t? so I
> don't know which one you want me to use in the signature contract
> (symbol? . -> . t?)", or, less nicely, the user would just get a
> runtime contract failure saying "expected <t?>, given: #<t>" (which is
> the kind of error message you already get today when two modules
> provide data structures with the same name and you mix them up).  In
> such a case the programmer would just have to rename one of the data
> structure, or use some kind of prefix system.

All of this assumes inferred linking, and that compound units export
all signatures.  For explicit linking that may hide some exports, your
reasoning does not apply.  You can have many different t?'s, and a
later linking won't see earlier ones.

And for uses of units that instantiate some generic library for
particular dependencies -- say, a set unit based on an ordered type,
instantiated on different types -- (a) there may be many Ts, and (b)
it is important to contract based on the right Ts.

While we don't use units for these things a lot in Scheme, it's a use
case that gets more and more realistic with things like (a) inferred
linking, making units syntactically lighter weight, and (b) Typed
Scheme, typed idioms necessitating this kind of instantiation more
often.

>>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.
>
> Then when you link your units together using
> compound-unit-with-contracted-signatures you'd get an error message
> saying "t@ and u@ both export t? so I don't know which one to use in
> the contract of s^".
>
>>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.
>
> Great.
>
> Thanks,
>
> Philippe