Beta-normalization: Sort the fields of a record projection #625
Conversation
|
I tried to follow the other examples of sorting judgments in the document. Not sure whether I got it right… |
| @@ -0,0 +1 @@ | |||
| λ(x : { a : Bool, b : Bool, c : Bool }) → x.{ a, c } | |||
|
I hope this makes more sense! |
standard/beta-normalization.md
Outdated
| t₀.{ x } ⇥ t₁.{ x } | ||
|
|
||
|
|
||
| t₀.{ xs₀… } ⇥ t₁.{ x₀, xs₁… } |
There was a problem hiding this comment.
I don't think you need to do this by induction, because there is nothing to normalize in the set of fields (since they are keys, not Dhall expressions). Rather than these two judgments, I think you only need something like this:
t₀ ⇥ t₁ sort(xs₀) = xs₁
─────────────────────────
t₀.{ xs₀ } ⇥ t₁.{ xs₁ }
There was a problem hiding this comment.
Thanks, that's much better! Should we change the keys operator used below to be similarly abstract? (And use = instead of ⇥?)
There was a problem hiding this comment.
The keys function expects a record as its argument, whereas the set used for projection is not a record.
It's not clear where you want to use = instead of ⇥
There was a problem hiding this comment.
It's not clear where you want to use
=instead of⇥
In keys(ss…) ⇥ ss₁…, ss₁… isn't an expression so maybe it would be better to write keys(ss…) = ss₁….
There was a problem hiding this comment.
@sjakobi: Oh yeah, the keys function should be using just =
There was a problem hiding this comment.
I have opened #642 to fix the keys usage.
…as standardized in dhall-lang/dhall-lang#625.
…as standardized in dhall-lang/dhall-lang#625.
Closes #622.