Skip to content

proposal: spec: comparable as a case of a generalized definition of basic interfaces #53734

Open
@atdiar

Description

@atdiar

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
intimplements 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 includes I itself
    • if type I = interface {~T} the typeset of I is the set of types whose underlying type is T
    • 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
  • 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 type U of an element with a restricted version of U where the type set is now a singleton composed of any one of the members of the initial type set of U. If T is not a composite of interface types, type set of T is therefore the singleton {T}
    • if T is not a composite type, then the type set of T is the the singleton {T}

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} implements interface{int | string | bool} but does not satisfy it or itself (the interface is not in the type set)
  • any satisfies comparable 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 interface S(e.g. in the body of a function, the type parameter is used where a comparable type is expected), then S must implement C.
This is easy to see as any type that satisfies S (i.e. in the type set) has to satisfy C 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:

Would need modifications:

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

No one assigned

    Type

    No type

    Projects

    Status

    Hold

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions