Checking contracts without crashing

[ranfdev]

I need to change the behavior of a function depending on the type of the parameter. I have many complex contracts and I can't use them to check a value without crashing the whole program when the contract isn't valid.

It would be nice having a function contract.validate Contract myrecord returning just a Bool, without crashing.

The alternative is to write a is_mycontract function for every MyContract I've defined, but that's impractical and unfeasible for contracts defined in external libraries (like num.Nat)

[yannham]

It's actually a tricky question, because contracts are not predicates. It's a tad technical, but this blog post touches upon the subject and how it makes it difficult to define and and or operators for contracts.

A possible solution is to express most of your contracts as boolean predicates (if they are), that is functions Dyn -> Bool, and then just use contract.from_predicate to generate the corresponding contract:

# my contract library
{
  predicates = {
    Foo = fun value => ...,
    Bar = fun value => ...,
    Baz = fun value => ...,
  },
  contracts = record.map (fun _name => contract.from_predicate) predicates,
} 

Then you have an easy access to the predicate corresponding to a contract. Of course this is quite limiting, as you loose the ability to use record contracts, merging, you can't have custom error messages for different cases, and so on. In practice I guess this is acceptable if all your contracts are pretty specific boolean predicates.

I can see two ways of implementing contract.validate:

1. accept that contract.validate Contract myrecord forces the evaluation of myrecord recursively. Then we would just deeply evaluate myrecord | Contract with a kind of catch-like exception mecanism recovery, but is not out of the question.

2. have a partial contract.validate function, similar to a partial or function hinted to at the end of the blog post on union and intersection contracts. Under the hood It would automatically deduce a predicate from some contract: e.g. {foo | Num, bar | {baz | Str}} would be

    fun r => builtin.is_record r
      && record.has_field "foo" r
      && record.has_field "bar" r
      && builtin.is_num r.foo
      && builtin.is_record r.bar
      && builtin.has_field "baz" r.bar
      && builtin.is_str r.bar.baz
   

   but would fail on any custom contract written as a function.

[ranfdev]

Thank you for the thorough explanation, I needed it.

I understand having lazy evaluation is a major objective of nickel, but in this case, I think both the solutions you proposed require strict checking of the entire contract anyway.

In the blog article you linked the issue is different, because the contract needs to be evaluated lazily and partially.

Having said that, I would prefer the first option, the catch-like one, because it would let me validate any contract.

[yannham]

You're right with respect to both points:

• the predicate approach still forces values. The difference, I think, is that we don't need to have this catch-like mechanism in the abstract machine, which sounds dangerous (could break future optimizations in non-obvious ways, be incompatible with some other features, etc.). Because this catch wouldn't be accessible for the user, only for the primop contract.validate in a scoped way, I suspect it's still fine (that is: it wouldn't break important properties of the language). But this needs some thinking.
• the union/intersection contract is a bit different, because here we are talking about a specific primop contract.validate, and it may be fine to say "warning: this will forces the underlying values", as long as it doesn't affect standard contract. That being said, you can be sure that if contract.validate is available, people will use it to implement unions and implement contracts that are more eager than needed/expected :upside_down_face: