Guarantees
Modules
Spec
Types6Runtime6Witnesses4RFC0001
Overview0Constraints17TypeCase37Representation3Discussion0No function recovers the type of every value from its representation, because two values of different types can share one. An untagged union type therefore cannot support a type test, and it is excluded.
The subset test accepts a use of a constrained variable if and only if every type the variable can be instantiated to satisfies the required constraint. It rejects nothing sound and accepts nothing unsound.
A type satisfies the intersection if and only if it satisfies both constraints, so replacing two constraints by their intersection changes no program's meaning.
It entails each of the two constraints, and any constraint that entails both of them entails it. The solver therefore makes the most general choice, which is what principal types need.
When two constraints share no member, no instantiation satisfies both, so reporting an error is the only sound outcome.
When exactly one type is left, every instantiation that satisfies both constraints is that type, so the solver may replace the variable by it.
This is derived satisfaction. When the check passes at the definition, every type that satisfies the constraint yields a specialization with the declared type. A call site is never the first place where an operation on the constrained variable is found unsupported.
When the check fails, there is a member at which the body is not well typed. The diagnostic can name it.
A body that checks against a member set checks against every set that entails it. Removing a member from a constraint never breaks the definition, so only adding one can.
Inside a body whose variable has one member set, calling a definition that was checked against another is sound when the first entails the second. Every type the caller can be instantiated to is one the callee was checked at.
A body that applies one operation to its parameter checks if and only if each member has a witness
for that operation with the declared result type. The result type may mention the variable, which
is how x + x has type 'T at both int and float.
Whenever a body specializes at a type, the specialization returns exactly what the reference meaning returns at that type, on every input. The reference meaning inspects the instantiating type and the specialization has no access to it. The static type-case is therefore erased completely: no run-time test, tag or type argument is needed to implement it.
Evaluation of a specialization that has a type never gets stuck, and the value it returns has that type. This rests on the assumption that every witness is implemented at its declared type.
Take a definition whose check passes, any type satisfying its constraint, and arguments of the parameter types at that type. The definition's meaning at that type is a value of the declared result type. The check at the definition is all that is needed: nothing is checked again at a call site or at run time.
Its specialization does not depend on the instantiating type. Only a type-case can make a set-constrained definition behave differently per member, so the loss of uniformity is confined to bodies that ask for it.
Its meaning is the same at every type, on every input. A set-constrained definition that does not use a type-case is as uniform as an unconstrained one.
When each type-case tests every member, saturation finds an arm for every instantiating type that satisfies the constraint. No instantiation is left without code.