Description
Abstract
By reviewing a few concepts, we can define type sets, constraint interface satisfaction, interface implementation, in a way that makes the comparable
interface obey a general rule instead of being an exception. In doing so, constraint interfaces would be strictly equivalent to interface types. This would future-proof their use as regular types.
Basically, a Go type defines structure and behaviors i.e. (a set of constraints) on raw data.
Some set of constraints are first-class citizens in Go and are represented by interface types.
The types that satisfy a given set of constraints form a type set.
- Interface satisfaction is then simply the satisfaction of the set of constraints denoted by that interface
- Interface implementation ensures that a type is at least as constraining as a given interface
e.g. any
is less constraining than comparable
: it does not implement comparable because its type set holds types that do not satisfy comparable
int
implements comparable
: every type in the type set of int
satisfies comparable
- constraint satisfaction is type set membership of a type
- interface implementation is type set inclusion of the type set of a type.
Now comparable
can just simply be one of these interface types that describe a set of constraints: {"has the comparison operators == and !=} just as defined in the spec.
All current Go interface types satisfy this constraint even though they rarely implement it. That's why they can instantiate type parameters constrained by comparable
.
comparable
could be used as a regular type in the future: assignment requiring interface implementation, it would ensure the absence of panic on equality testing for types satisfying it.
Remains to model type sets in terms of sets of constraints.
While type sets are often infinite, we know that the constraints of the language are of finite quantity.
The rest is set operations on sets of sets of constraints (this is not a stutter, this is accounting for unions)
Proposal
(Re)define type set, interface satisfaction, interface implementation so that comparable
follows a general rule of interface types. And in doing so, lay the ground work for a potential use of all interfaces outside of generic code ( interfaces as sum/union types).
Background
What is an interface?
Types specify structural and behavioral constraints on raw data.
The Go language has a special construct in its type system that can be used to describe some of these constraints: interface types.
(note that, by virtue of being types themselves, these interface types also satisfy their own set of constraints that may be completely unrelated)
An interface type can describe constraints on types such as:
- a set of methods
- the underlying element ( ~T)
- the availability of the comparison operators (
comparable
)
An interface type may also describe a set of constraints as a combination of the above, using:
- union interfaces
- interface embedding (which provides intersection)
What is a type set?
Since a type specify a set of constraints that can be potentially satisfied by other types as well, we can gather these constraint-satisfying types into what is called a type set.
Type sets are fully described by a set of constraints. In mathematics, this would be set comprehension notation. A constraint would be a set intension i.e. a proposition.
As such, we do not need to compute type sets specifically (theoretically, a lot of type sets are infinite anyway).
We can just describe them using the finite number of constraints that can be modeled in Go.
- type set of an interface type
I
:- if I is a basic interface, it is composed of every type that has the methods of
I
. By definition, that includesI
itself - if
type I = interface {~T}
the typeset ofI
is the set of types whose underlying type isT
- if
I
is defined as a union of type terms, the type set of I is the union of the type set of each term
- if I is a basic interface, it is composed of every type that has the methods of
- type set of a concrete type
T
:- if
T
is a composite type (struct, array, slice, channel, ...), the type set of T includes all possible combinations obtained by substitution of the typeU
of an element with a restricted version ofU
where the type set is now a singleton composed of any one of the members of the initial type set ofU
. If T is not a composite of interface types, type set ofT
is therefore the singleton{T}
- if
T
is not a composite type, then the type set ofT
is the the singleton{T}
- if
It's interesting to note that for composites of interface types, the type set includes types that may have not been defined in a Go program.
In theory, these are subtypes. Since variance is restricted in Go, they do not necessarily appear as runtime types. This is not an issue since we do not propose to compute type sets explicitly but to rather operate on the set of constraints that define them.
Constraint satisfaction and interface implementation
While a type may satisfy a set of contraints, if that type is an interface type, that interface type may be used to describe a totally different set of constraints.
For example,
interface {int | string | bool}
satisfies the constraints shared by all interface types. But it describes a whole other set of constraints. Therefore, it does not satisfy the set of constraints it denotes.
The aforementioned example shows that constraint satisfaction and interface implementation are different notions altogether, where interface implementation is taken to indicate constraint enforcement (or entailment).
If types may satisfy some constraints, they do not necessarily enforce them. (e.g. any
satisfies comparable
just as any interface currently, but a type satisfying any
does not mean it satisfies comparable
)
Said otherwise, interface implementation tests that the constraints described by an interface can be found in the set of constraint defined by another type. This is a comparison of constraintive power.
A type T
implements an interface I
- iff
typeset(T) ⊆ typeset(I)
- iff
constraint_set_described_by I ⊆ constraint_set_described_by T
i.e. every type that satisfies the constraints of T also satisfies I.
Interface implementation is constraint satisfaction over the type set of a type. It is not constraint satisfaction of the type itself.
As showed above, in general, interface implementation does not imply interface satisfaction and vice versa.
For example:
interface{int | string | bool}
implements itself but does not satisfy itself. (this is good, this is what we'd expect)interface{int | string}
implementsinterface{int | string | bool}
but does not satisfy it or itself (the interface is not in the type set)any
satisfiescomparable
but does not implement it
With the introduction of interface types and their semantics, there is a distinction between a type and its type set which is the reason for such difference.
type set of a type parameter
The type set of a type parameter is somewhat unknown. We just know that the type parameter itself satisfies a constraint interface.
In general, it can only be known to be assignable to itself.
It can be understood as a mostly opaque type variable but not necessarily an interface type.
Note If a type parameter is constrained by an interface
C
and must also satisfy another interfaceS
(e.g. in the body of a function, the type parameter is used where a comparable type is expected), thenS
must implementC
.
This is easy to see as any type that satisfiesS
(i.e. in the type set) has to satisfyC
too (type set inclusion).
Comparable type parameter
The spec states that: "In any comparison, the first operand must be assignable to the type of the second operand, or vice versa."
Assignability is based on interface implementation. The issue here is that a type parameter is not known to implement any specific interface more often than not.
Usually, we don't know a type parameter's type set before instantiation in the general case. We just know that every type implements itself.
The general rule is that a type parameter satisfies an interface if its constraint implements it.
Examples
Let's borrow the examples from #56548 (spoiler: we arrive at the same result)
type mymap[K comparable, V any] map[K]V
func _[P any, Q comparable]() {
var (
_ map[func()]string // invalid with current and new rules: func() is not comparable
_ map[struct{ f P }]string // invalid with current and new rules: P is not assured to be comparable
_ map[struct{ f Q }]string // valid: key type is comparable
_ mymap[any, string] // currently invalid, valid with new rules: any supports ==
_ mymap[struct{ f any }, string] // currently invalid, valid with new rules: type of f supports ==
_ mymap[struct{ f func() }, string] // invalid with current and new rules: f is not comparable
_ mymap[struct{ f int }, string] // valid: key type satisfies comparable
_ mymap[struct{ f P }, string] // invalid with current and new rules: P may not be comparable because any does not implement comparable
_ mymap[struct{ f Q }, string] // valid: key type satisfies comparable
)
}
To be comparable means to satisfy comparable
which itself means to satisfy the set of constraint described by comparable
.
It does not mean to implement comparable
, the latter implying some sort of substitutability (which appears in Go during value creation such as struct{any}{int(2)}
or type assertions)
If we want to be able to require from a type parameter that it implements comparable
, we will need something else. In the meantime, there should be no difference between what can be expressed in generic Go vs regular Go.
Observations
- All types could be part of type sets, including interface types. This should not be an issue since type sets are not first-class types themselves. No Russell's paradox: the set of all type sets is not a type nor a type set.
- type safety is guaranteed for variable assignment since it requires interface implementation
- In terms of implementation, it could require a little bit more work around type sets (to be redefined in terms of constraint sets). However, I believe that this is the way to make it work as evidenced by the theory
- This proposal ignores the current restrictions on constraint interfaces. They can remain and be lifted progressively. Especially since, for union types, it is expected that dealing with terms whose type set intersection is not empty may require some attention.
- some constraints are inter-related (notably methods imply restrictions in terms of signature for a same method name) and should be accounted for when checking set inclusion of constraint sets.
- a union of sets of constraints is not the set of the union of constraints
- since variance is restricted (no subtyping), a variable's type is fixed. Constraints sets are not mutating. It should simplify things and make constraint satisfaction checking tractable.
spec (AFAICT)
Unchanged:
- https://go.dev/ref/spec#Comparison_operators
- https://go.dev/ref/spec#Assignability (afaict)
- https://go.dev/ref/spec#Type_assertions
Would need modifications:
- https://go.dev/ref/spec#Interface_types (somehow the definition of a type set is correct for basic interfaces, but general interfaces and interface implementation need to change; something about interface satisfaction could be added too)
- https://go.dev/ref/spec#Type_parameter_declarations (the paragraph defining comparable implementation would need amendments)
Appendix
A similar treatment can be found in the type theory literature under the name semantic subtyping and perhaps CSP.
For most of the constraints expressed in Go, we would rarely (if ever) need to prove the satisfiability of interface types (which is just proving that they can be inhabited, i.e. proving that their type set is not empty).
Notably because the type checker forbids a lot of unsatisfiable interfaces already, and also because the expressivity around creating new interfaces is limited. Union interface changes that a little but not that much.
In any case, it should let us establish the semantics of an hypothetical FutureGo in one fell swoop, hopefully.
Metadata
Metadata
Assignees
Type
Projects
Status