Sometimes it is helpful to be able to say: this function produces a result, without specifying what that result is. For example, in a recent type systems proof I've been working on, we have:
function typing(Environment R, Term t) -> Type:
...
function reduce(Store S1, Environment R, Term t1) -> (Store S2, Term t2)
requires typing(R,t1) == ??
Here, I don't care what the type produced is, only that one can be produced. (Technically, we also need termination but that is an orthogonal issue). To resolve this, I made a wierd hack:
function typing(Environment R, Term t) -> null|Type:
...
function reduce(Store S1, Environment R, Term t1) -> (Store S2, Term t2)
requires typing(R,t1) != null
Of course, typing can never return null (and this could be stated in the precondition). Eitherway, it does the trick! Therefore, we want a syntax like this:
function reduce(Store S1, Environment R, Term t1) -> (Store S2, Term t2)
requires typing(R,t1) == _
(see also #35)
Sometimes it is helpful to be able to say: this function produces a result, without specifying what that result is. For example, in a recent type systems proof I've been working on, we have:
Here, I don't care what the type produced is, only that one can be produced. (Technically, we also need termination but that is an orthogonal issue). To resolve this, I made a wierd hack:
Of course,
typingcan never returnnull(and this could be stated in the precondition). Eitherway, it does the trick! Therefore, we want a syntax like this:Here,
_is a don't care value.