Nondeterministic/oracular constraints (e.g., guess / oneOf)

[shonfeder]

A special place for discussing this topic that we've been kicking around for a while.

There is some concern that if we expose non-deterministic constraints or oracular inputs -- or however we ought to think of this -- to spec authors that they will be confused or end up writing specs that don't behavior as they'd expect. (Actually, I realized I'm not 100% clear on the concern.)

A key discussion on this may be #377 (comment) In particular, see @bugarela's proposal for extending the effect system to account for nondet effects in a general way: #377 (comment)

This is proposed as an alternative to what @konnov has been advancing, which is a syntax that has special rules for nondet values, only allowing them to appear on the rhs of a binding prefixed with a keyword (viz. nondet) and only allowing these bindings in particular contexts (e.g., not on the top level, and only in operators that have Update).

[shonfeder]

Ported from #393 (comment)

---

If we are thinking of nondet as of something similar to for-yield in Scala, what would be a similar construct to the embedded expression in Scala?

I don't think there is an equivalent in Scala! afaik, we were confined to expressing this kind of thing with monadic idioms, we'd either need a binding operator or some kind of callback (e.g., the bind combinator, of which I think we can see guess a special case). afaict, if we carried your proposal with nondet through to its most general and coherent conclusions, we'd end up with something that looks very much like a monadic binding operation that can be used only in a non-deterministic computational context. However, with the critical difference that we would only be enforcing this through some relatively adhoc syntactic rules, rather through our type system. For a point of comparison, it looks to me like nondet as you've proposed it is quite like a special case of OCaml's binding operators.

afaiu, when taken to its full generality -- in Haskell's do notation or Scala's for comprehensions -- we get a way of expressing a sequence of bindings parameterized over an arbitrary computational context (see https://binaryanalysisplatform.github.io/bap/api/master/monads/Monads/Std/index.html#intro for an exposition of this perspective). This lets us represent different computational effects through a uniform syntax, but it does not let us reason about effects in a "direct style". In other words, Haskell's do notation and Scala's for comprehensions, and OCaml's binding operators are all just syntax sugar over a chain of callbacks :)

However, afaiu, the fact that we can move our reasoning into our effect systems opens up the opportunity to support the direct style proposed by @bugarela. I can explain this in more detail if that would be helpful.

But the gist is basically that, if we are using the monadic idiom to, e.g., sequence partial computations in Scala, we can do stuff like:

scala> val x : Option[Int] = for { 
  x <- Some(1); 
  y <- Some(x + 1) 
} yield x + y
x: Option[Int] = Some(3)

scala> val x : Option[Int] = for { 
  x <- Some(1); 
  y <- None 
} yield x + (y : Int)
x: Option[Int] = None

And the for comprehension here is just syntax sugar for a chain of callbacks that allow us to bind to the computed value (if there is one):

scala> val x : Option[Int] = 
  Some(1).flatMap( x => 
  Some(x + 1).flatMap( y => 
Option(x + y)))
x: Option[Int] = Some(3)

In this context, flatMap and <- provide binding operations to optional values (meaning values constructed from partial computations) without letting letting that value "leak" into the outside (unless we pattern match against the Option of course). My observation here was that guess looks like a way of providing a binding operation on non-deterministic values while keeping the nondeterministic effect from "leaking" into the outside. Of course, we weren't representing this nondet effect explicitly in our type system, but we were instead hiding it inside a boolean value that could only be used in an action. This has the same effect of preventing the value derived from within a non-deterministic context from "leaking out".

Now, the important point of comparison here w/r/t the suggestion that we allow oneOf to be used as a value is that the following is not supported in Scala (or Haskell or OCaml) etc:

scala> val x : Option[Int] = for { 
  y <- Some(Some(1) + 1) 
} yield Some(1) + y
<nope!>

I.e., we cannot substitute Some(1) for the x we bind using <- or flatmap in the previous examples. This is because the point of the monadic binding is to enable binding the value inside the context of partial computations and the "partiality effect" is managed by the binding operations on the basis of the reification of this partiality into the language (i.e., via the Option type). However, this limitation comes from the fact all these languages use their monadic idioms to represent effectual computations, and if we are only looking at these monadic constructs, there is no way of representing the effects other then through the composition of the binding operations.

However, with access to an effect system, we can reason about and handle effects in a "direct style". I think this is what @bugarela and I have been advocating for. As a point of comparison, this is what it can look like to leverage an effect system (in this case, OCaml 5's) to manage partial computations in a direct style:

https://github.com/shonfeder/ocaml-effstudies/blob/58fe0fa35b9c2df47dcd3387713d8af79765ab3d/lib/partial.ml#L65-L93

let%test_module "partial computation effects" = (module struct
  open Partial


  let (/) n = function
    | 0. -> none ()
    | d  -> some (Float.div n  d)


  let head = function
    | []     -> none ()
    | x :: _ -> some x


  let tail = function
    | []      -> none ()
    | _ :: tl -> some tl


  let%test "direct style with successful operations" =
    let progn () =
      (head [4. ; 3. ; 2.]) / 2. :: tail [2. ; 3. ; 4.]
    in
    Optional.handler progn () = Some [2. ; 3. ; 4.]


  let failing_progn () =
    let z = 1. / 0. in
    let x = head [z ; 2. ; 3.] in
    let y = tail [1.] in
    x :: y


  let%test "direct style with a failing operation" =
    Optional.handler failing_progn () = None

Note that we can apply the partial operations / and hd as if they were normal expressions, and have the effects handled "behind the scenes". This is what we are proposing with oneOf, afaiu.

If we were bound to using mondaic idioms, we'd have to write the progn in direct style with successful operations as (switching back to Scala):

for {
  h  <- head(List(4, 3, 2));
  x  <- y / 2 ;
  tl <- tail(List(2, 3, 4));
} yield x :: tl

I.e., we'd have to bind each intermediate optional value. I think this is roughly what we get if we end up requiring the nondet keyword for any values bound from oneOf.

[bugarela]

All of this makes sense to me! I prefer the idea of propagating non-determinism in a monadic way much better than having a single specific way of using it as we currently do with nested nondet named values. I believe our effect system is a good place to track this monadic encapsulation without adding complexity to our type system. Perhaps in #399 we can drive the type system to this direction, by defining signatures in terms of a -> m a and m a -> a, i.e. next should look like Action e -> Temporal e.

[shonfeder]

Trending on Hacker News and similar is a discussion around the Verse programming language, which is a functional logic programming language, like Mercury or Curry, that includes first-class data-nondeterminism.

[konnov]

I also looked at it and did not get whether it was about non-determinism or just generators

[shonfeder]

IMO, this partially depends on perspective. It's possible the easiest way in to thinking about this (and this may be useful for our thinking here) is in reference to use of the list monad to model non-determinism.

I think this is an approximate translation into current Quint syntax of the example given in the first answer there:

action experiment = {
    nondet newCoin = oneOf(pick)
    nondet result = oneOf(newCoin.toss())
    all {
       result == Head,
       coin' = coin
    }
}

iiuc, the key point is basically just that you can model non-determinism by reasoning over the space of all possible values. The generators (in the linked example given by the <- bindings) enable this.

[konnov]

Ah, that's an interesting perspective!

[konnov]

I know that we still have some disagreements on nondet x = oneOf(A) ..., but this syntax did not seem to cause any issue with our early users (except that the effect checker needs to be fixed). Closing this discussion.