Comparable interfaces, isComparable

Comparing two interfaces may cause a runtime error if both dynamic values are incomparable. For example, slices are not comparable in Go:

func main() {
	var x any = []int{1, 2}
	var y any = []int{3}
	if x == y { // error
	}
}

panic: runtime error: comparing uncomparable type []int

goroutine 1 [running]:
main.main()
	/home/gobra/comparable.go:52 +0x77
exit status 2

Gobra provides the function isComparable, which takes as input an interface value or a type and returns whether it is comparable according to Go. When the value of an implementation is stored in an interface value, Gobra records whether the resulting interface value is comparable. In the following example, we assign the numeric constant 5 to x, which makes it comparable.

func compare(x any) {
	// @ assert !isComparable(type[[]int])
	// @ assert isComparable(type[string])
	x = 5
	// @ assert isComparable(x)
}

As an example, we change the linked List type to store values of type any (which is a shorthand for the empty interface interface{}).

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value interface{} // previously int
}

Note that we can store arbitrary values in the list, as the empty interface is trivially implemented by every type.

The recursive function Contains that searches the list for a value might panic because of the comparison l.Value == value between possibly incomparable values, which Gobra detects:

// @ requires acc(l.Mem(), 1/2)
// @ pure
// @ decreases l.Mem()
func (l *List) Contains(value interface{}) bool {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l != nil && (l.Value == value || l.next.Contains(value))
}

ERROR Comparison might panic.
 Both operands of l.Value == value might not have comparable values.

To require that the List contains only comparable elements, we define the function Comparable. With isComparable, we state recursively that each element must be comparable.

/*@
ghost
requires acc(l.Mem(), 1/2)
pure
decreases l.Mem()
func (l *List) Comparable() bool {
	return l != nil ==> unfolding acc(l.Mem(), 1/2) in (isComparable(l.Value) && l.next.Comparable())
}
@*/
// @ requires acc(l.Mem(), 1/2)
// @ requires l.Comparable()
// @ pure
// @ decreases l.Mem()
func (l *List) Contains(value interface{}) bool {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l != nil && (l.Value == value || l.next.Contains(value))
}

The following client code verifies.

func client() {
	var l *List = nil
	// @ fold l.Mem()
	l = &List{Value: "hello", next: nil}
	// @ assert isComparable(l.Value)
	// @ fold l.Mem()
	l = &List{Value: 1, next: l}
	// @ fold l.Mem()
	// @ assert l.Contains("hello")
	// @ assert !l.Contains([2]int{0, 1})
}

Comparing two interfaces may cause a runtime error if both dynamic values are incomparable.

The function isComparable takes as input an interface value or a type and returns whether it is comparable according to Go.

Ghost equality ===, !==

The ghost comparison === compares values of arbitrary types by identity and does not panic. If we used the normal equality == instead in the following example, Gobra reports an error since the sequence contains elements of type any which might not be directly comparable.

// @ ghost
// @ decreases
// @ requires 0 <= i && i < len(s)
// @ requires 0 <= j && j < len(s)
// @ requires s[i] == s[j]
// @ func GhostEq(s seq[any], i, j int) {}

ERROR Comparison might panic. 
Both operands of view[i] == view[j] might not have comparable values.

Full example

package main

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value interface{} // previously int
}


/*@
// Represents access to the List element and all elements in its tail.
pred (l *List) Mem() {
	l != nil ==> (acc(l) && l.next.Mem())
}
@*/

/*@
ghost
requires acc(l.Mem(), 1/2)
pure
decreases l.Mem()
func (l *List) Comparable() bool {
	return l != nil ==> unfolding acc(l.Mem(), 1/2) in (isComparable(l.Value) && l.next.Comparable())
}
@*/

// @ requires acc(l.Mem(), 1/2)
// @ requires l.Comparable()
// @ pure
// @ decreases l.Mem()
func (l *List) Contains(value interface{}) bool {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l != nil && (l.Value == value || l.next.Contains(value))
}


func client() {
	var l *List = nil
	// @ fold l.Mem()
	l = &List{Value: "hello", next: nil}
	// @ assert isComparable(l.Value)
	// @ fold l.Mem()
	l = &List{Value: 1, next: l}
	// @ fold l.Mem()
	// @ assert l.Contains("hello")
	// @ assert !l.Contains([2]int{0, 1})
}


func compare(x any) {
	// @ assert !isComparable(type[[]int])
	// @ assert isComparable(type[string])
	x = 5
	// @ assert isComparable(x)
}