Monomorphization: Traits feature

[wrwg]

Suppose I define a theory generic over some type T, let's say vectors, and I want to specify a contains function for vectors:

type Vec _;
... 
function Contains<T>(v: Vec T, e: T): bool {
   (exists i: int:: InRange(v, i) && ReadVec(v, i) == e)
}

Yet the problem here is that I do not may have extensional equality for T. So I would prefer to use an equality specific for T.

If one wants to have specific operations on generic type parameters T in programs, there are type classes in functional languages and traits in Rust and C++.

Here I'm going to claim that in an axiomatic language with monomorphization for generics it is even simpler than in programming languages to achieve something similar than traits. So lets try this example again:

type Vec _;
... 
function Contains<T>(v: Vec T, e: T): bool {
   (exists i: int:: InRange(v, i) && IsEqual(ReadVec(v, i), e))
}
function {:trait} IsEqual<T>(x1: T, x2: T): bool;

There is now an abstract uninterpreted function which describes the equality being used here. This equality would be instantiated by axioms which are specific to the type instantiation:

axiom {:trait} (forall x1, x2: int :: IsEqual(x1, x2) <=> x1 == x2);
axiom {:trait} (forall<T> x1, x2: Vec T :: IsEqual(x1, x2) <=> IsEqualVec(x1, x2));
...

Because we monomorphize, we actually end with IsEqual_int and IsEqual_vec_T being separate functions, and the above axioms would expand to what we expect.

Some open questions:

• Do we really need a special {:trait} attribute?
• Do we need to specify something similar like {:ctor} today to instantiate the axiom? Can we perhaps get rid of this and compute the information it provides?
• .. and possibly many more

@shazqadeer @RustanLeino

[shazqadeer]

Thanks for the interesting feedback. I ran boogie on the following program with the options /monomorphize /printInstrumented and manually confirmed that the expected definitions and axioms are generated.

type Vec _;

function InRange<T>(v: Vec T, i: int): bool;
function ReadVec<T>(v: Vec T, i: int): T;
function IsEqual<T>(x1: T, x2: T): bool;
function IsEqualVec<T>(x1: Vec T, x2: Vec T): bool;

function Contains<T>(v: Vec T, e: T): bool {
   (exists i: int:: InRange(v, i) && IsEqual(ReadVec(v, i), e))
}

axiom (forall x1, x2: int :: IsEqual(x1, x2) <==> x1 == x2);
axiom {:ctor "Vec"} (forall<T> x1, x2: Vec T :: IsEqual(x1, x2) <==> IsEqualVec(x1, x2));

procedure A(x: Vec int, y: int) {
    assert Contains(x, y);
}

procedure B(x: Vec (Vec int), y: Vec int) {
    assert Contains(x, y);
}

This experiment suggests that the `{:trait}' attribute could be simulated by the currently supported features.

Your message also contains the orthogonal idea of eliminating the :ctor attribute and automatically calculating axiom instantiations. This is an interesting idea and I will think about incorporating it.