New dictionary contract semantics breaks record.map with recursive dependencies

[vkleen]

The new dictionary contract semantics from #1141 seem to break record.map on records with recursive dependencies. Specifically, #1141 is the first commit to produce the following:

nickel> record.map (function.const function.id) { a = 1 }
{ a = 1 }
nickel> record.map (function.const function.id) { a = 1, b = a }
error: contract broken by a function
  ┌─ :1:36
  │
1 │ forall a b. (Str -> a -> b) -> {_: a} -> {_: b}
  │                                    - expected type of an argument of an inner call
  │
  ┌─ repl-input-5:1:47
  │
1 │ record.map (function.const function.id) { a = 1, b = a }
  │                                               ^ applied to this expression
  │
  = This error may happen in the following situation:
        1. A function `f` is bound by a contract: e.g. `(Str -> Str) -> Str)`.
        2. `f` takes another function `g` as an argument: e.g. `f = fun g => g 0`.
        3. `f` calls `g` with an argument that does not respect the contract: e.g. `g 0` while `Str -> Str` is expected.
  = Either change the contract accordingly, or call `g` with a `Str` argument.
  = Note: this is an illustrative example. The actual error may involve deeper nested functions calls.

note:
  ┌─ <stdlib/record.ncl>:3:11
  │
3 │     map : forall a b. (Str -> a -> b) -> {_: a} -> {_: b}
  │           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ bound here

note:
  ┌─ repl-input-5:1:47
  │
1 │ record.map (function.const function.id) { a = 1, b = a }
  │                                               - (1) calling <func>

Interestingly, all other ways I've tried to narrow down the issue evaluate without a hitch:

nickel> { a = 1, b = a } | { _: Num }
{ a = 1, b = 1 }

nickel> let f : forall a. {_: a} -> {_: a} = fun r => r
nickel> f { a = 1, b = a }
{ b = 1, a = 1 }

[yannham]

Reporting here our ideas/findings during the weekly meeting: the bulk of the issue is that there are somehow two different - and natural, at least each one in some situations - interpretations of what could record.map mean on a recursive record.

First interpretation: "outer" mapping

The first interpretation is a natural extension of the semantics of record mapping on non-recursive records. We mostly ignore that fields might be dependent over other fields, and just slap a function on top of each value of the record, giving:

nickel> {foo = 1, bar = foo + 1} |> record.map (fun _key => (+) 1)
{bar = 3, foo = 2}

This is the current semantics. One question is what happens if we override foo later on: should bar be updated, or not? That is, should the resulting record be recursive again, or does map "freezes" out recursive records for ever. Currently, the latter is implemented:

nickel> ({foo = 1, bar = foo + 1} |> record.map ((+) 1)) & {foo | force = 5}
{ foo = 5, bar = 3 }

We could imagine that the result would be:

nickel> ({foo = 1, bar = foo + 1} |> record.map ((+) 1)) & {foo | force = 5}
{ foo = 5, bar = 7 }

But this second question is quite orthogonal to this issue, as we'll see. The important characteristic of this first variant is that the mapping operation is applied after the fixpoint computation has taken place. It can't update the recursive occurrence of foo inside bar with a new value.

Second interpretation: "inner" mapping

If we go back to the semantics of recursive records as being functions, where we compute the fixpoint at each record operation, then let r = {foo = 1, bar = foo + 1} is represented as r ~ fun self => {foo = 1, bar = self.foo + 1}. If we consider that record operation should commute with the fixpoint, what we get is map_inner f r ~ fun self => {foo = f 1, bar = f (self.foo + 1). This is in fact equivalent, in Nickel source code, to apply a "syntactical" mapping over the record, that is:

map_inner f r := {foo = f 1, bar = f (foo + 1)}

This is semantics is different from the previous one, because f get applied to recursive occurrences of foo inside the record as well (hence "inner"):

nickel> {foo = 1, bar = foo + 1} |> map_inner (fun _key => (+) 1)
{foo = 2, bar = 4}

This second way of mapping can sound natural (when defined syntactically, or as commuting with the fixpoint function), but it has a strange behavior: it's not obviously possible to type it correctly. For example, map_inner (fun _key => builtin.to_string) {foo = 1, bar = foo + 1} would result in a dynamic type error, because bar is now "1" + 1. The type of the record should probably be understood as {foo : A, bar : A -> Num} / A := Num, and the type of the mapped function has to satisfy some constraints with respect to A (here, is has no choice but to produce a number).

That being said, this mapping seems to make sense in the case of contracts. For example, if we apply a contract on top of this record:

{ foo, bar = foo.default_value} | {foo | default = {default_value = 1}, bar}

We expect this example to work (this kind of case showed up in e.g. the tf-ncl repo) and bar to inherit the default value of foo coming from the outer contract, which is exactly the inner mapping semantics.

Discrepancy

The above issue comes from the discrepancy between the two: polymorphic sealing is done through a dictionary contract, which since recently, just acts like a lazy record contract. This applies the inner semantics, and in particular seals recursive occurrences of fields inside the record, like foo in bar = foo + 1.

Unsealing is done by applying the mapped function, but this use the outer semantics, leaving sealed terms inside the record, and causing the error.

The solution isn't totally obvious right now. Either making the contract mapping outer, or the record mapping inner, has unpleasant consequences (in each case, the current mapping semantics seem to be the one we want in practice).

We what are exploring right now, and have continued this morning, is to consider bar to be of type A -> Dyn, where A is the type/contract applied to foo, and consider the content of bar to be (fun foo => foo + 1) | A -> Dyn. Note that this A in negative position is the dual contract of A (it's the same, but with seal/unseals reverted). Following this interpretation, if we plug foo | A inside, now the sealing and unsealing magic happens. So, when cross-applying contracts to recursive occurrences of field, we shouldn't simply apply the contract A alone, but both A and its dual (for some definition of dual, that has only to do with polymorphism and flipping polarity of free type variables). In practice, we've come up with a single contract application, to avoid wastefully applying the same contracts twice, and started to prove that this transformation is correct.

This is work in progress, and will be surely extensively documented in a note, as the matter isn't trivial.

[matthew-healy]

@yannham Just to confirm, should:

We could imagine that the result would be:

nickel> ({foo = 1, bar = foo + 1} |> record.map ((+) 1)) & {foo | force = 5}
{ foo = 5, bar = 3 }

actually have bar = 7? Currently both results are the same. 😅

[yannham]

actually have bar = 7? Currently both results are the same. sweat_smile

Indeed. Fixed. Thanks!