add static interfaces in the form of signature types#1543
Draft
zerbina wants to merge 1 commit intonim-works:develfrom
Draft
add static interfaces in the form of signature types#1543zerbina wants to merge 1 commit intonim-works:develfrom
zerbina wants to merge 1 commit intonim-works:develfrom
Conversation
beef331
reviewed
May 12, 2025
| and `macro`:idx: are not. | ||
|
|
||
| For every routine declaration in the body, at least one parameter must be of | ||
| type `placholder`, `var placeholder`, or `sink placeholder`. Declarations must |
beef331
reviewed
May 12, 2025
| or more candidates that satisfy the requirements listed above, application | ||
| fails. If sucessful, the resulting application is said to *bind* to `y`. | ||
|
|
||
| Two applied signatures are equal are equal iff both are applications of the |
Collaborator
Author
There was a problem hiding this comment.
The spelling is deliberate. "iff" is a short form of "if and only if" (source).
Contributor
There was a problem hiding this comment.
Perhaps it's not shorter if you have to provide this message along with all reading material 😛
Collaborator
Author
There was a problem hiding this comment.
Well, iff is already used in other places of the manual.
Nonetheless, you're right in that the usage does make the text less accessible; I'll expand it.
beef331
reviewed
May 12, 2025
| On application of `S` to `T`, for every routine declaration `x` of `S`, a | ||
| routine `y` must be *visible* in the current context such that: | ||
| * `x` and `y` have the same name | ||
| * after all `placholder`s in the parameter list of `x` are replaced with `T`, |
Contributor
There was a problem hiding this comment.
placholder -> placeholder
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Signature types are meant to provide static interfaces, which would be a first step towards type-checked generic routines and (maybe) eventually removing
.borrow.The name
signatureis a working title. It's not yet clear whether the feature will take overconceptor stay as its own entity, and thus theconceptsyntax is simply reused.The current specification is not meant to represent the final form. It's a version of the feature as discussed so far that's narrowed-down as much as possible in order to make a robust implementation feasible/possible with the current compiler. Further restrictions due to issues discovered during implementation are likely.
The feature was inspired by the
signaturefeature of Standard ML.To-Do
TTypekinds for signature types and their applied form