[Dogfooding] Nullable of several contracts (or, union of intersections)

[yannham]

Is your feature request related to a problem? Please describe.
During dogfooding on the mantis repo, I had to convert CUE types that are morally unions of intersections, as this one. In this example, Weight is either:

1. an unsigned int AND an int smaller than 100 AND an int greater than -100.
2. or null

Intersections alone (on simple contracts like this, at least: see the paper reference at the end for more info) can just be represented as several contract applications in Nickel. If we take Weight to be NON nullable, we can simply translate this as:

Weight | #nums.Nat
       | #(GreaterEq -100)
       | #(SmallerEq 100)

A nullabe alone is also not so bad. If we forget the bound -100 and 100, then we could write it like:

Weighy | #(Nullable nums.Nat)

Or even Weight | #Nullable #nums.Nat (under the proposal #445).

The problem is that when we mix everything, we cannot pass a series of contract application | #nums.Nat | ... to Nullable: that is, intersection of contracts is not first class. Currently we need to do something like:

let AllOf = fun contracts label value => lists.fold
  (fun c acc => c label acc) contracts value in
{
  Weight | #(Nullable (AllOf [nums.Nat, GreaterEq -100, SmallerEq 100]))
}

While not awful, it is quite more verbose and different than without the Nullable: in one case we just use standard contract application in sequence, but in the other we need a new combinator AllOf.

Describe the solution you'd like

I don't really know of a great solution. We can't have general union and intersection contracts for deep reasons: we actually published a paper about this very specific subject this year. So adding a syntax to do that, even in limited cases, could be very misleading and error prone in case of misuse. I just wanted to report this quirk to see if someone has a better solution on how to handle this.

[thufschmitt]

I’m a bit skeptical of the x | #C1 | #C2 | #C3 way of writing intersections. As much as combining contracts that way makes sense for merging (say (x | #C1) & (x | #C2)), I feel like it’s a weird way of directly writing an intersection − because what we want is one contract that says “C1 and C2 and C3” − modulo the fact that it’s not really an intersection, not a succession of each.
So I’d rather have a dedicated operator for that (Thinking about it, couldn’t C1 & C2 & C3 do just that? I suspect not because & on functions can’t be merged, but maybe there’s a way to get that). Which would also solve the Nullable issue since the result would be a new contract

[yannham]

I’m a bit skeptical of the x | #C1 | #C2 | #C3 way of writing intersections. As much as combining contracts that way makes sense for merging (say (x | #C1) & (x | #C2)), I feel like it’s a weird way of directly writing an intersection − because what we want is one contract that says “C1 and C2 and C3” − modulo the fact that it’s not really an intersection, not a succession of each.

I guess it's a matter of taste. To me it quite reflects the actual semantics of the "intersection", as it says apply contracts #C1, #C2 and #C3 in sequence. This is very similar to the pipe operator for values, in the end:

value
|> c1
|> c2
|> c3

which is almost what the former several contracts application desugar to, modulo labels and conversion of contracts-as-record to contracts-as-function. However, the problem is that this construction is not first class, either on the value side (we can't write Nullable (< > | C1 | C2 | C3) where < > would be e.g. a hole) nor on the types side foo | #Nullable ( | C1 | C2 | C3), which is the root of the problem here IMO.

Once again, there are two "worlds", or syntactic categories, to consider: the values side, and the types side.

Introducing an & on the type side may be quite deceiving, since as you note, this is not intersection, and it won't do what you think for e.g. functions. Also, the user could expect that we actually have intersection types on the static side, which we clearly don't plan to implement (say {foo = 1, bar = 1} : {foo: Dyn, bar: Num} & {foo: Num, bar: Num} would be actually usable as a {foo: Num, bar: Num}).

On the values sides, it would make sense to use merging indeed, such as let Both = Foo & Bar implements the "sequential intersection" semantics. It is already working when Foo and Bar are records. Currently it is not possible to extend this to all contracts, because contracts are just naked values, so as you say you can't distinguish between two random functions wrongly merged or contracts-as-function that should be composed. However, it is not out of the question to have contract be specific values: related to #318, which advocates for a special syntax to define contracts.

It would be more limiting though, as we can't merge a builtin type. Another solution would be to have something dual to #, allowing to extract the contract from a type as a first-class value.

[thufschmitt]

I’m wondering whether having a “merging” for functions similar to the one for records would make sense (disclaimer: At least at a first look it’s unbearably complex). If we consider records as a special-case of functions (that map each label to its value), then we can have a “natural” extension of & to arbitrary function types, something like:

(a->b)&(c->d) = (a\c -> b) /\ (c\a -> d) /\ (a&c -> (b&d))

where /\ and \ are the set-theoretic intersection and difference.

(except that we’d need to extend that to merging arbitrary intersections, and that gets a bit hairy)

Where this is interesting compared to an unrestricted set-theoretic intersection is that (I hope) the intersections only happen between arrows with a distinct codomain, meaning that there’s an immediate witness of which branch should be taken (like for discriminated unions).

At least on the paper it looks like it could lead to a somewhat decent semantics (as long as we don’t pretend that it’s an intersection), and solve the issue as it would just become a Nullable of the merge of several contracts. But it’s Friday afternoon, so maybe this is just all nonsense.

[yannham]

Closing as this is solved by std.contract.Sequence. There are interesting side ideas and questions here, but I think they will be better tracked and considered as separate issues. I think the last idea of @thufschmitt is really hard to do because it requires set-theoretic type (to be able to form like a\c) which sounds quite hard to combine with laziness (we don't even have unions, so complements...)