[plt-dev] compound units and contracted signatures

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 :-)

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

>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