Implement with keyword

[Gabriella439]

... as standardized in dhall-lang/dhall-lang#923

[Gabriella439]

Note that this is still missing tutorial documentation and fixes to downstream packages

[sjakobi]

I guess it would be nice if we could statically ensure that we'll never encounter a With after normalization. But of course, With is not the first constructor like that.

[Gabriella439]

@sjakobi: We actually already have a way to ensure that. The Val type from Eval.hs is the "fully normalized" type and it does not have a With constructor.

[sjakobi]

Good point @Gabriel439! Maybe we should consider using it in places where we handle normalized expressions, such as parts of dhall-json.

[Gabriella439]

@sjakobi: Yeah, that was the original intention, but we rolled it out initially in a way that minimized disruption.

Another example of where the API could offer a better type is in typeWith/typeOf, since the inferred type should be in normal form (and indeed the internal infer utility that powers both has the correct type)

[sjakobi]

Even with #1702 cherry-picked onto this branch, this error message is somewhat suboptimal:

⊢ { a = 1 } with a.b = 2

Error: You can only combine records

Explanation: You can combine records using the ❰⫽❱ operator, like this:


    ┌───────────────────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ { baz = True } │
    └───────────────────────────────────────────┘


    ┌─────────────────────────────────────────────┐
    │ λ(r : { foo : Bool }) → r ⫽ { bar = "ABC" } │
    └─────────────────────────────────────────────┘


... but you cannot combine values that are not records.

For example, the following expressions are not valid:


    ┌──────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ 1 │
    └──────────────────────────────┘
                                 ⇧
                                 Invalid: Not a record


    ┌───────────────────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ { baz : Bool } │
    └───────────────────────────────────────────┘
                                 ⇧
                                 Invalid: This is a record type and not a record


    ┌───────────────────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ < baz : Bool > │
    └───────────────────────────────────────────┘
                                 ⇧
                                 Invalid: This is a union type and not a record


You tried to combine the following value:

↳ { a = 1 }.a

... which is not a record, but is actually a:

↳ Natural

────────────────────────────────────────────────────────────────────────────────

1│ { a = 1 } with a.b = 2

(stdin):1:1

The main problem is that the error message explains the correct usage of //, which the user didn't directly use in this case.

Can we improve that error, possibly by applying a similar trick as the InvalidDuplicateField error when desugaring things to /\-expressions?

dhall-haskell/dhall/src/Dhall/TypeCheck.hs

Lines 806 to 818 in b675924

	Combine mk l r -> do
	_L' <- loop ctx l
	xLs' <- case _L' of
	VRecord xLs' -> do
	return xLs'
	_ -> do
	let _L'' = quote names _L'
	case mk of
	Nothing -> die (MustCombineARecord '∧' l _L'')
	Just t -> die (InvalidDuplicateField t l _L'')

[sjakobi]

Great progress! I have more comments though! ;)

BTW I often feel a bit bad when my review suggestions cause you so much work. Would you prefer if I'd try to address my suggestions myself? I could push directly to your branches (as you sometimes do with my PRs) or open PRs against your branch. What would you prefer?

Also please do push back when you feel that my suggestions are disproportionate or otherwise inappropriate.

[Gabriella439]

@sjakobi: There's no need to apologize! I'm happy to address review feedback and I'm not afraid to push back when appropriate

[sjakobi]

👍

I believe that errors in with-expressions will still be a challenge for users who haven't read the record desugaring spec. We'll know more when we get their feedback! :)

[sjakobi]

CI is green, code and docs look good, so I'll let mergify merge this! 🚀