Tags/semantic decorators #3768
Replies: 6 comments
-
Are you sure youre not just describing Shapes? |
Beta Was this translation helpful? Give feedback.
-
@Flutterish I thought I made a pretty good distinction there. Shapes specify how classes should behave, i.e. what members they should have. Tags extend how instances of classes behave when invoked or combined with others by adding tags to the return type. Shapes encode compile-time invariants about the type. Tags encode runtime invariants about the value. The shape of a type is specified just once as a constraint. The tag of a type is flexible and can be added or removed wherever the type is used, based on the value, which we then say to be parsed as the tagged type when the runtime invariants the tag specifies are checked. Shapes are compiled as interfaces and this way they allow the runtime to call methods on the witness. Tags remain static classes and they are not handled by the runtime at all, only present in metadata/signatures (similarly to static classes in System.Runtime.CompilerServices). "Applying" a shape to a type requires compatibility of the members. Applying a tag to a type only requires it matching the explicit constraints specified by the tag itself (possibly a shape). If a tag has any members, they don't have to be present on the to-be-tagged type, it only specifies what invariants can be implied for members or results of operations. In general, a shape is a specific condition that an input type must meet, and this allows you to call its methods. A tag is an implied condition a value must meet, and prevents you from using "invalid" values without spilling checks all over the place. You are probably using a tag without even realizing it, and the tag is "NonNullable". The distinction between The only slight issue is that tags are "safe" only when encoding information about a value that never changes once checked, but still, if you are using immutable data structures, you are safe and free from checks. And In a sense, tags are generalized explicit contracts when treated as a part of the type system. |
Beta Was this translation helpful? Give feedback.
-
This sounds a lot like roles (#1711) to me. |
Beta Was this translation helpful? Give feedback.
-
@333fred Good point! It seems the declaration of a tag is essentially a generic role, but I am unsure about the members: public role NonEmpty<T> of T
{
public override Positive<> Length => base.Length;
public override Positive<> Count => base.Count;
} The point was either one of |
Beta Was this translation helpful? Give feedback.
-
I think the comparison with nullable is a lot closer than with roles. They are less a type system and more a way to augment static type checking, which lands them pretty close to source generator territory. I have mixed feelings about that, on one hand this is something may be possible to create right now. On the other hand, it seems like potentially a lot of headache, and source generators sit pretty high on my list of "Things I should learn and want to learn, but get put off by the entry barrier" Perhaps it would be worthwhile to add "tags-like system" to the list of common use cases for source generators and investigate potential roadblocks to doing so and if there are any ways to streamline their creation? For what it's worth, tags would be incredibly useful to me currently. I'm in the midst of writing a compile time type and stack checked abstraction layer over reflection.emit that is implemented entirely through generics, and it is quite the headache at times. |
Beta Was this translation helpful? Give feedback.
-
This is a weird pull, but this use case most reminds me of Ada's subtypes feature. I could see being able to restrict a type (but not necessarily imply an inheritance relationships) being useful. I do agree with @333fred, I think the roles proposal covers this use case and more. I would imagine that the design of "roles" could be changed so, at minimum, it would behave like "type tags". I think that is actually the main use case for roles when combined with pattern matching and (hopefully) discriminated unions. Related discussions: |
Beta Was this translation helpful? Give feedback.
-
This proposal is inspired in part by F# and its units of measurement feature, and in part by Parse, don’t validate.
A "tag" is a kind of a type that can be attached to any type or value on a per-use basis, and serves to further distinguish values of any type. The main purpose of tags is to introduce lightweight "decorators" into the type system that don't affect the runtime behaviour of the code, but allow the static type checking to guarantee certain invariants are upheld, similarly to non-nullable reference types.
Syntactically, a tag is a combination of a static class, an interface, and a shape. However, instead of restricting functionality of types it is used in combination with, like an interface, it can extend any operation on a normal type by means of specifying the result tag.
As a simple example:
A tagged type is considered its own type in C#, acting as a derived/more specific type when compared with its untagged version. Specifically, a tagged type can be used as a return type, parameter/variable type, as a generic argument or constraint, or even the base type. In contrast, a tag itself, without being applied to anything, is only valid as the operand of
typeof
, or when inherited by another tag. Method overloads distinguished solely by the tags of their parameters should be allowed.A tag can be derived from another tag, a specific non-static type (class, struct, delegate, enum, interface), a tagged type, or a shape, all permitted simultaneously. When derived from a tag, it specifies implication; when derived from anything else, it indicates a restriction (the to-be-tagged type must be assignable/conform to the restricted type).
A type tagged with the same tag twice is different from when it is tagged only once, also the order of applied tags matters.
Operations
A tag can also specify its members. but any member that is an instance member or an operator method is considered special. Non-special (thus static) members work like on any other type; they are accessed and invoked via the tag itself. Special members are not permitted to have a body, and any type used therein can be a tag.
When invoking members on a tagged type, the lookup works the same as for an untagged type. However, when the tag itself has a member that matches the invoked member, it can add tag information to the type of the member.
Positive(3) + Positive(5)
isPositive(int)
, butPositive(3) - Positive(5)
is simplyint
. As long as the tag is applied in a semantically safe way, all its subsequent uses are also safe.A private pseudo-constructor syntax could be used to restrict the accessibility of the tag when applied to values:
Generics
It makes sense to allow tags to be generic. It also makes sense to allow not only tagged types as generic arguments, but also tags themselves, when the generic parameter specifies it.
In the case of a tag parameter, the constraints are always necessary.
int
specifies the tag can be applied toint
(not restrictively, but only permissively), andnew()
specifies its "constructor" is visible and thus it can be freely applied to values.Implementation
In signatures, it is viable to emit tags as either
modreq
ormodopt
. At runtime, it seems better not to represent tags at all. A considerable option would be to representNonZero(int)
asNonZero<int>
andNonZero(1)
asnew NonZero<int>(1)
for a new type similar toValueTuple<int>
, but this violates the inheritance chain and makes(object)NonZero(1) is int
fail.Alternatives
There are several other options for the syntax, from which I have chosen the one that seemed both easy to grow accustomed to, and easy to parse.
Beta Was this translation helpful? Give feedback.
All reactions