Add more assertion operators

[byorgey]

trafficstars

See https://github.com/disco-lang/disco/pull/217#discussion_r455930497 . Right now Disco has an operator =!= : a -> a -> Prop ("assert equal to") which asserts the equality of two things (and fails with a nice error message showing the values of the two sides if they are not equal). We should also have corresponding operators for other sorts of assertions, for example, !< ("assert less than"), !<=, etc. which work similarly. This should not be too hard to add following the general pattern of the way =!= is already implemented.

Or, as a more radical proposal:

• Get rid of =!=
• Optionally make Bool no longer a subtype of Prop
• Add a single prefix unary "assert" operator (unfortunately ! is already taken for factorial; !! might work; we could also provide the function name assert) of type assert : Bool -> Prop. It has the effect of both turning a boolean value into a Prop, and also finding the top-level boolean operator and turning it into an equivalent assertion which does nice reporting if the proposition fails. This way we wouldn't need to have a bunch of special operators parallel to the normal operators, just a single assertion operator. The downside is that it might feel a bit magic.

[shaylew]

Some thoughts on assert:

• Would it be able to play nice with prop-level connectives? I suppose it could just distribute over boolean connectives, making them act on props instead.
• If we go this route without removing the subtyping, I don't see a reason not to silently wrap quantifier bodies and property tests in files with assert.
• There's still no getting around spelling out the assert when you create a prop to pass around (to something like forallElements : Bag a -> (a -> Prop) -> Prop) or to return (e.g. from assertBetween : Q * Q -> Q -> Prop). This is probably not a big deal.

[byorgey]

Hmm, the design space here is definitely trickier than I thought.

Would it be able to play nice with prop-level connectives? I suppose it could just distribute over boolean connectives, making them act on props instead.

That sounds sensible at first, but it worries me: so suppose assert (x and y) automagically turns into (assert x) and (assert y), but what about let f = \_. x and y in assert (f 3) ? You can easily imagine arbitrarily complex scenarios where Boolean connectives are hiding inside multiple layers of definitions, and it's unreasonable to expect that we could automatically turn them into Prop-level connectives (or is it?). But when we're using :test there might be an important difference between assert (x and y) and (assert x) and (assert y). For example, in the latter case it might be able to report to you that it was able to find an example satisfying the assert x but not the assert y, whereas with assert (x and y) maybe it's only able to tell you that it never found any examples making the boolean true.

If we go this route without removing the subtyping, I don't see a reason not to silently wrap quantifier bodies and property tests in files with assert.

That makes me feel vaguely uneasy for similar reasons.

There's still no getting around spelling out the assert when you create a prop to pass around

I'm not sure I understand what you're saying here.

[shaylew]

I guess what had me looking down that path was thinking of assert as more a macro or tactic than a function: it operates on the syntax of a boolean expression and through a syntactic transformation gives you back a version with error reporting. In a language with pervasive macros, I'd expect a macro like that to know how to look through top-level connectives in the expression -- admittedly, part of that expectation is just that most languages/libraries would just avoid the macro in favor of regular assertion operators unless the macro was doing some nontrivial work.

The rest of the comment was just seeing how far an "automagic best effort" approach could go, and where it would still require some manual annotations -- your example with an equality test behind a definition is one example, and the couple of higher-order props I handwaved into existence were also examples of places the user really does want to use an assertion operator but no magical (syntactic) approach to inserting them is going to cut it.

Though actually... is there an issue with determining whether you mean boolean == or prop == based on type, without any syntactic analysis or syntactic user guidance? The sketch would be:

• make comparison operators have type (QCmp a, QBool b) => a * a -> b, and pass them b at runtime so they know what to return
• default otherwise-unconstrained QBool variables to B (unless qualified types are on), so user-visible types stay the same
• drop the prop/bool subtyping and require an explicit conversion from B to Prop (with assert or some other builtin), in the cases where that's still necessary.

I think this handles all our examples in a satisfactory way, it defaults to giving thorough messages (if you get an "assertion failed: value was false" you know it's because you used assert not because you forgot to use assert), and it's relatively nonmagical.

(Despite writing a bunch here I don't think I'm super attached to any of these ideas. I'm poking around trying to think of a way to minimize the conflict for users between "writing the simplest thing that disco will accept", "writing the thing that most looks like the notation I'm used to", and "writing something that will give good error messages", but there might just have to be a tradeoff made and that's also fine.)

[byorgey]

I was thinking about this more today and I realized that we would also want things like !/\ ("assert and"), and so on. But if the left side of an and is false, we might want that to recursively contain an =!=, and so on. I realized that there is something more general going on here: the point is that when a proposition fails, we want to present some evidence why it failed to the user. e.g. "This proposition failed because it is a conjunction, where the left side was true but the right side failed; the right side failed because it is an equality test, and the left-hand side of the equality was X whereas the right-hand side was Y..." Maybe what this is really arguing for is that we shouldn't need any kind of special "assertion" operators, but rather the evaluation of propositions can automatically do this kind of evidence reporting (much like we already do for forall and exists).

[byorgey]

Closing this now that we have merged #365 .