[Dogfooding] If-expression in record literals

[yannham]

While dogfooding, trying to convert the IOHK mantis ops repo from CUE to Nickel, ifs were one pattern that didn't map directly from CUE to Nickel. Cue allows to have if-expression inside a record literal, to define some parts of a record conditionally, kinda Nix mkIf :

{
  foo: string | *null,
  if foo != null {
    bar: true
  }
}

It's in particular used in CUE's equivalent of contracts, to define a subcontract depending on certain fields (example). This issue gathers first thought about how to encode this in Nickel.

Case 1: non recursive

In the example above, the content of the record only depends of some tg which is in scope because it is an argument of a list comprehension. In Nickel, this is translated as a lists.map (fun tg => ...). In this case, where there's no usage of a recursive field of the same record, we can simply break the record definition in pieces and use merging and a good ol' standard if:

// In CUE
{
  bar: val1
  if condition {
    foo: val2
  }
}

// Rewrite to
{
 bar = val1,
} & (if condition then {
  foo = val2}
  else {})

// Could make it more concise with an helper:
{
  bar = val1,
} & conditionalDef condition {foo = val2}

Which is, in the end, not too bad. Here is the orignal CUE snippet from mantis once translated via merging: translation

Case 2: recursive

However, when the body of the if makes reference to recursive fields, there's currently no way to do this. Here is a simplified example:

{
  foo: int
  if condition {
    bar: foo | *null
  }
}

And here is a real-life example in mantis.

With merging

Once #330 lands, we could theoretically use merging too. But that would require to be able to merge things like { foo = 1} & {bar = foo + 1}, which hasn't been fully debated yet (the problem is that in the second record, there's no way to know where the hell is foo coming from, as it's a form of dynamic binding). Depending on our decision about this, this can make those kind of ifs with recursive fields quirkier to express. Also, in the real-life example, the condition itself depends on a recursive field, which I don't even know how to encode properly, even with a permissive overriding implementation.

Adding ifs ?

Another solution would be to have the same kind of feature as CUE in Nickel, that is ifstatements as part of record definitions. I think it would also cover the use-case of mkIf for Nix. But this is yet another syntax and magic builtin operator.

[francois-caddet]

What about something like:

{
  bar: int,
  foo = if condition then bar else |hidden,
}

It stay a recursive record so you can even have foo in the condition term I suppose. Just a supposition, I don't saw this part of the nickel code. hidden will be a special Metavalue keyword as already default is one. The typechecker will then type foo as bar and return a blame we are trying to use foo when the condition is not met.

[yannham]

Actually, adding an hidden meta annotation to show fields that are not to be serialized is something that I've been considering for a long time, and that feels natural. From this, we can indeed just push the if inside the field, and use this kind of "first-class metadata", as you suggest. We may still need to provide a value for the | hidden annotation (or not, depending on if this syntax is ambiguous), but it can very much be null.

A thing to consider is that it has a different semantics than {bar | Num} & (if condition then {foo = bar} else {}). In particular, all the primitive operations will be able to observe the presence of a field foo with your suggestion (like hasField, fieldsOf, map, and so on), while they wouldn't with the merge-based version. To avoid this, we would need force the evaluation of all the fields of a record before any of those primitive operation to see if they may be actually hidden values, which is out of the question.

[aspiwack]

I think that if you have “first class metadata“, then they need to be strict (the spine needs to be strict, actual content of the field, hidden behind a | default or | value (was it the name? I forget) will stay lazy in this scheme).

The semantics of the language gets a bit trickier to get right, probably.

On the other hand, such strict first class metadata do not handle the case that raised the issue as you can't use other fields' values within the strict part of a (recursive) record. Ugh!

This is a bit tricky. The same problem exists with a dedicated field-if syntax.

This seems to be a very unnatural feature in the context of Nickel, doesn't it?

[yannham]

I think that if you have “first class metadata“, then they need to be strict (the spine needs to be strict, actual content of the field, hidden behind a | default or | value (was it the name? I forget) will stay lazy in this scheme).

In practice I think we already kinda have "first-class metadata", as metadata can be attached to pretty much any value. Something close to what @francois-caddet wrote (modulo the as of yet non existing hidden attribute) can already be done, it's just that currently the parser refuses to accept metadata without an inner value outside of record fields, so we have to write null or whatever:

{
  bar | Num,
  foo = if condition then bar else (null | some metadata | some others),
}

This kind of things also work, for that matter:

{
  foo = if true then (fun x => x) (1 | default) else null,
}
// behave as {foo | default = 1}

Unless I'm misunderstanding what you are talking about, I don't think this requires the data structures to be strict however. Currently primitive operations that depends on meta-data (merge, query and serialization) evaluate their operands in a specific mode "evaluate until the first metadata or WHNF but do not unwrap in the inner value" when they are requested, and they handle this kind of things.

This is a bit tricky. The same problem exists with a dedicated field-if syntax.

This seems to be a very unnatural feature in the context of Nickel, doesn't it?

A field-if syntax does look trickier with respect to strictness. But it looks the same kind of chicken-and-egg problems we have with recursive records, so I imagine a field-if feature could also be implemented in Nickel's model, morally/implicitly as a fixpoint. Using representation of recursive records as functions of self:

{
  foo | if bar == 2 = "bar is 2",
  bar = 2
}
// Would be encoded as
fun self =>
  {bar = 2} & (if self.bar == 2 then {foo = "bar is 2"} else {})

[vkleen]

So the issue is about having the existence of a record field depend on the values of other fields, possibly other fields defined far away via recursive record merging. Indeed, I don't think we can currently encode this. We can have the values of fields depend on other fields defined far away by declaring what kinds of fields we expect:

{ foo = 1 } & { foo | Num, bar = foo + 1 }

is valid and makes perfect sense to me. In the same spirit, we can also do

{ foo = true } & { foo | Bool, bar = if foo then 2 else null }

However, {bar = null} and {} are different. Maybe they shouldn't be? If the semantics of setting a field to null in a record were to remove that field, we wouldn't need any new syntax.

On the other hand, if we want to keep making a distinction between a field being null and a field not existing, I personally think a metadata annotation like { foo | Bool, bar | if foo = 2 } would make the most sense. In this form, it should also play nicely with RFC005; the metadata annotation expresses a property of the record field, not of its value.

[yannham]

{bar = null} and {} should definitely be different, I think. JSON is the underlying data model for Nickel, and it does make a difference between those two values. Be it null or something else, having a special value that can unset fields sounds like Javascript's undefined, and it's a whole new can of worms, IMHO.