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 an interface value or a type as input and returns whether it is comparable according to Go. When an implementation's value 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 every type trivially implements the empty interface.

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.

We define the function Comparable to require that the List contains only comparable elements. 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 an interface value or a type as input 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.

// @ 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) {}

If we used the normal equality == instead in the preceding example, Gobra would report an error since the sequence contains elements of type any that might not be directly comparable.

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)
}