CozySynthesizer / cozy

The collection synthesizer
https://cozy.uwplse.org
Apache License 2.0
209 stars 18 forks source link

ambiguous empty issue (WIP) #104

Closed izgzhen closed 5 years ago

izgzhen commented 5 years ago

We should fix this to let argmin/max return null if the argument list is empty. this should simplify a lot of real world code, e.g. datastructure-synthesizer/followup/eval/mongo/spec.ds

Test: cozy argmin.ds

izgzhen commented 5 years ago

or we might not want it because we want things to be sound -- both okay, just curious which might be better off

Calvin-L commented 5 years ago

For whatever it's worth, here are my thoughts on various designs for partial functions like argmin in Cozy. Note that the the operator is another partial function that could also return null instead of behaving how it does now, so it is also related to this topic.

  1. Have partial functions return a "default" value of the appropriate type (e.g. 0 for integers). This can be surprising because adding an element to a set might cause the minimum to increase: if the set changes from {} to {1} because you added 1 to it, then the minimum goes from 0 to 1.
  2. Use design 1, but forbid specifications where a partial function could return a default value. This is what Cozy does today, and it is why you need to add additional assumptions and if-conditions to specifications when you use primitives like argmin. I like this design because it forces programmers to think more carefully about what should happen when you try to extract elements from an empty collection.
  3. Throw an exception at run time when a partial function would fail. This is what Java does so it might feel more familiar to programmers, but the synthesis engine does not reason about exceptions so it is very difficult to implement. (Issue #19 exists to track progress on this.) Unlike design 2, this would allow programmers to write specifications with methods that fail at run time even when the method preconditions written in the specification are satisfied. Therefore I don't like this design as much.
  4. Introduce a safe "Maybe" or "Optional" type for the output of partial functions. This was actually how Cozy behaved at one point in the past, but I removed it in favor of design 2 because it required many more internal primitives and much longer synthesis times. Instead of using the output of a min computation directly, synthesis would need to introduce lots of extra primitives to "unpack" the optional value, which makes solutions have more AST nodes and therefore harder to discover.
  5. Extend all existing types (integers, booleans, collections, etc.) with a null value. This would require a lot more run time checks from the code generator, and would introduce more overhead into the generated code. It also means that we cannot use, say, the native C++ bool type because it does not have a null value.
  6. Have min return the set of all smallest elements in the collection rather than one of those smallest elements. This design is very elegant from an implementation standpoint: it does not introduce an optional type but represents the "optional" output using an empty or nonempty collection. Cozy already has many good heuristics for working with collections. However, I decided this design was too confusing from a specification-writer standpoint.