Principle: The signature is the contract

[josh11b]

Introduces a new principle called "the signature is the contract," where Carbon requires the information needed to use an entity is present in the entity's declaration (its "signature"). The signature is authoritative, and is not modified by the definition body.

[geoffromer]

Moving a Discord discussion here: I find this name quite opaque and non-mnemonic, to the extent that when revisiting the topic after only a few days, I had to skim this PR again to remind myself what the principle is actually about. I'd suggest instead something like "the signature is self-contained" or "the definition doesn't affect the signature".

To me, "the contract" refers to things like preconditions and postconditions (more broadly, everything that you need to reason about whether the calling code is correct), whereas "the signature" refers to the language-semantic content of a function declaration (i.e. everything that you need to reason about whether the calling code is well-typed). So "the signature is the contract" sounds to me like it's saying that Carbon will have statically-checked contracts as a language feature, and even suggests that we're trying to fully embed program correctness into the typesystem.

[josh11b]

I would be interested to hear if others find the title confusing.

[danakj]

I don't have any background with C++ contracts so to me the title is not confusing. But I could see how one might read it as being specifically about Contracts (a technical term) rather than a contract (an agreement between two parties)

[geoffromer]

I'm not very familiar with C++ contracts either, and I agree that a contract is an agreement between two parties, but I don't understand how that alleviates this concern. For example:

// Sorts the given array in increasing order.
fn Sort[T:! Core.Ordered, N:! Core.BigInt](ref a: array(T, N));

Would you say this function's contract includes the guarantee that a will be in increasing order after the call?

[danakj]

Would you say this function's contract includes the guarantee that a will be in increasing order after the call?

To other developers, yeah. But not to the type system/compiler.

I think I see your point, which is that I was reading it as being the latter and you are reading it as saying something about the former. Though given the language does not know anything outside of the compile-time values/type system, I don't personally find it too ambiguous still, and I worry any other word that means the same is not doing any better then, since this is about "agreements between the caller and callee" and not an issue with a specific word.

[geoffromer]

How about "usages aren't checked against definitions", or if we want something pithier, "usages don't see definitions"?

[github-actions]

We triage inactive PRs and issues in order to make it easier to find active work. If this PR should remain active, please comment or remove the inactive label.

This PR is labeled inactive because the last activity was over 90 days ago. This PR will be closed and archived after 14 additional days without activity.

[chandlerc]

I think it would be good to discuss this a bit in one of our open discussions...

I really like the direction here, and so I want to find a way to land this in some form.

However, there are two aspects that I'm still struggling with a bit in the current presentation of the principle:

• I also struggle a bit with the name of this principle, I think for similar reasons to what @geoffromer is getting at in the in-line comment: specifically, it is hard to pin down what exactly is meant by "signature" and "contract" in the title. The suggestions here so far have been to pivot to a more directly descriptive formulation, which might work for me although so far none of the suggested formulations really resonate. The other way to improve this is if there is some additional word or words in the title that help give context to what is meant by "signature" and "contract" -- for example "The declared signature is the type-checking contract" is a bit long but works better for me than without the two contextual clues.
• The distinction between a use that does and a use that doesn't reference the members of an entity is I think needs more or better delineation. I don't think there is any confusion or controversy here, just that it is a subtle distinction that we maybe haven't yet found good ways to articulate.

I somewhat think we might benefit from trying to pin down the second of these, because that might give us more precise words around what we are actually doing here, and those in turn might provide easier ways of writing the title that convey the intended design principle?

[josh11b]

From discussion, it sounds like the substance here around things like supporting separate compilation are already part of the information accumulation principle. Is there something we want to append to that principle?

[dirk-bester]

Reading the brief Discord discussion the concern seems to be that part of contracts should or could be surfaced to the signature.

Parts like postcondition are irrelevant but useful for compile time reasoning about the code. However, what if for example your entry conditions contain things like valid values? Again, useful for compile time reasoning, but I have wondered if such things should be part of a language in addition to just Type? I don't mean just default values as are already in signatures. I mean things like
int8 min 1 max 7
Currently you have to maybe make a class that enforces that in the constructor or use asserts or contracts or enums or other code. But it could just be in the language and the compiler produces the boilerplate or safety code as necessary.
The nice thing is your testing and fuzzing can be automated for in range and out of range values. Potentially a compiler could introduce checking code only at points where casting from dubiously compatible types happens? Or ubiquitous checking for debug builds, release checks only if the compiler can detect dangerous casting or source values that may not comply? Or linting can require range checks before using user or network data etc. but that would be out of scope requiring libraries to annotate such data as unsafe and validation code that can remove the annotation?

It would also move it into the signature and make the signature more complete. Which then clearly separates signature parameter concerns from the local implementation details that the remaining contract items deal with.

So call it "pact" or some other synonym for contract. "Pact" then stands for the standard signature plus relevant parts of contracts moved to the signature. Or just the standard signature if adding to it is too onerous or future stuff.