-
-
Notifications
You must be signed in to change notification settings - Fork 173
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add with
support for modifying Optional
values
#1254
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks great! Just some minor comments
standard/beta-normalization.md
Outdated
@@ -1441,6 +1441,43 @@ betaNormalize (Some t₀) = Some t₁ | |||
t₁ = betaNormalize t₀ | |||
``` | |||
|
|||
The `?` path componet can be used with the `with` keyword to update `Optional` values. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The `?` path componet can be used with the `with` keyword to update `Optional` values. | |
The `?` path component can be used with the `with` keyword to update `Optional` values. |
Oh, and this probably also needs a test exercising the new |
I added a section for Before that, I did notice a big flaw with the current changes: the type checking judgements don't enforce that the Edit: Actually, I think that would break the quoted label |
I think the correct way to fix this is to distinguish at the AST level the reserved In other words, currently the | With Expression (NonEmpty Text) Expression … and you would need to define a new data WithComponent = Label Text | Optional … so that the | With Expression (NonEmpty WithComponent) Expression Once you resolve that ambiguity at the level of the syntax tree then it's easier to fix the other ambiguities. For example, this expression: { x = 0 } with { ? = 1 } … would correspond to this Haskell syntax tree: With (RecordLiteral [("x", NaturalLiteral 0)]) (Optional :| []) (NaturalLiteral 1) … which would be a type error. Also, it would be distinct from this expression: { x = 0 } with { `?` = 1 } … which would correspond to this Haskell syntax tree: With (RecordLiteral [("x", NaturalLiteral 0)]) (Label "?" :| []) (NaturalLiteral 1) … which would evaluate to: { x = 0, `?` = 1 } |
Makes sense! I chose This approach also revealed a similar oversight in binary encoding/decoding. Currently,
and
have the same binary representation. I'm thinking maybe there could be a tag like |
I think it should be possible to extend the encoding for path components to include the reserved |
Got it! I'm having some trouble working inductively on the path. I initially wanted to write something like
but |
Yeah, introducing a new judgment is one way to do it, but you can also do something like this:
… and change the existing encoding judgment for
That might not be obvious, but then the corresponding Haskell code will clarify what that means |
Ah, that makes perfect sense. I did try to directly translate those judgements to Haskell, but I struggled to convince ghc that `encode` was still total. I'll leave my attempt here in case anyone can spot a way to fix it...encode (With e₀ (DescendOptional :| k₀ : ks₀) v₀)
| TList [ TInt 29, e₁, TList (k₁ : ks₁), v₁ ] <- encode (With e₀ (k₀ :| ks₀) v₀)
, let b = TList [ TInt 29, e₁, TList (TInt 0 : k₁ : ks₁), v₁ ] =
b
encode (With e₀ (DescendOptional :| []) v₀) = TList [ TInt 29, e₁, TList [ TInt 0 ], v₁ ]
where
e₁ = encode e₀
v₁ = encode v₀
encode (With e₀ ((Label k) :| k₀ : ks₀) v₀)
| TList [ TInt 29, e₁, TList (k₁ : ks₁), v₁ ] <- encode (With e₀ (k₀ :| ks₀) v₀)
, let b = TList [ TInt 29, e₁, TList (TString k : k₁ : ks₁), v₁ ] =
b
encode (With e₀ ((Label k) :| []) v₀) = TList [ TInt 29, e₁, TList [ TString k ], v₁ ]
where
e₁ = encode e₀
v₁ = encode v₀
That said, as you pointed out, it might be better to deviate from a direct translation to make the actual behavior more obvious. I've also added some tests! |
There's just one test failure to fix and then this is ready to merge: https://hydra.dhall-lang.org/log/c7fiq7f20h8cah9x0p7qdswal54ady50-test-files-lint.drv |
Fixed! |
🎉 @Gabriel439 thank you very much for all your help with this! With this done, I'm wondering if other language features could be extended to use the |
Are you expecting |
Ah, that's true! We diverged from the original idea of something like |
The main issue is that there's not a good way to type-check using It would work better if Dhall had something like polymorphic variant such as in Grace, because then the type of forall (a : Type) . < Some : a > -> a … and the type of the Some : forall (a : Type) (b : Alternatives) . a -> < Some : a | b > … so it would only work if the compiler could infer that only the |
I see. With all that said, what do you see for the future of #1141 (perhaps the discussion can continue there)? |
Oh, I misunderstood what you were asking! That would work if the result type were So in other words, you could standardize something that says that |
… as standardized in dhall-lang/dhall-lang#1254 Co-authored-by: David Richey <darichey1@gmail.com>
@darichey: Now that this is completed you can collect the $300 reward. If you submit an expense here then I'll approve it: https://opencollective.com/dhall/expenses/new |
As requested here, allow the use of the
?
label in awith
expression to updateOptional
values.Please note:
with
to parse correctly. I will need some guidance on modifying the grammar if the parentheses-less syntax is desired.with
on records, this cannot be used to modify the type of theOptional
. For example,(None Natural) with ? = "hello"
is a type error because we cannot infer the type of"hello"
to change theNone
application toNone Text
.I attempted to prototype an implementation in dhall-haskell: darichey/dhall-haskell@a476b08
I'm still very new to Dhall and working with the judgements in the standard, so it's highly likely I've forgotten something or made a mistake somewhere. Please kindly provide your feedback :)