Standardize records of mixed kinds #689

ocharles · 2019-08-02T14:22:15Z

No description provided.

ocharles · 2019-08-02T14:22:57Z

This currently contains the changes to tests as a result of the changes in dhall-lang/dhall-haskell#1173.

Before I write the prose according to this, could I get a sanity check that these tests changes look good?

sjakobi · 2019-08-02T14:34:19Z

LGTM so far. I'm missing a few tests though:

{ a = Kind} should not typecheck (per Restore support for records containing both types and terms dhall-haskell#1173 (comment))
a test for //\\
{ a = 0} // { a = Bool } (same field)

ocharles · 2019-08-02T14:44:10Z

{ a = Kind} should not typecheck

Done

a test for //\

There is tests/typecheck/success/simple/combineMixedRecords, which tests:

{ foo = 1 } ∧ { bar = Text } : { foo : Natural, bar : Type }

Do you have something else in mind?

{ a = 0} // { a = Bool }

Done

sjakobi · 2019-08-02T14:46:05Z

a test for //\

There is tests/typecheck/success/simple/combineMixedRecords, which tests:
{ foo = 1 } ∧ { bar = Text } : { foo : Natural, bar : Type }
Do you have something else in mind?

That's a test for /\, not //\\.

ocharles · 2019-08-02T14:46:55Z

🤦‍♂️

Thanks

ocharles · 2019-08-02T14:53:26Z

How about tests/type-inference/success/unit/RecursiveRecordMergeBoolTypeA.dhall Is that what you have in mind?

sjakobi · 2019-08-02T14:59:00Z

How about tests/type-inference/success/unit/RecursiveRecordMergeBoolTypeA.dhall Is that what you have in mind?

Cheers! :)

I noticed this though:

⊢ {a : Kind} //\\ {b : Kind}

Error: ❰Sort❱ has no type, kind, or sort

It seems unrelated, but shouldn't it be allowed?

ocharles · 2019-08-02T15:06:33Z

I think there might be some kind of bug with the repl:

[nix-shell:~/work/dhall-haskell/dhall]$ cabal new-run exe:dhall -- repl
Up to date
⊢ { a : Kind }

{ a : Kind }

⊢ :t { a : Kind }

Error: ❰Sort❱ has no type, kind, or sort


⊢ 
Goodbye.

[nix-shell:~/work/dhall-haskell/dhall]$ cabal new-run exe:dhall -- repl
Up to date
⊢ :t { a : Kind }

Sort
⊢ 
⊢ 
Goodbye.

[nix-shell:~/work/dhall-haskell/dhall]$ cabal new-run exe:dhall -- repl
Up to date
⊢ {a : Kind} //\\ {b : Kind}

{ a : Kind, b : Kind }

I have no idea what's going on there!

I think when it = { a : Kind } makes it into the history, the history has to be type checked, and something goes wrong... somewhere 🤷‍♂️

sjakobi · 2019-08-02T15:09:22Z

Yeah, it's confusing and should be fixed. I seem to remember that the repl keeps a history, and tries to typecheck previous results, which doesn't always work.

ocharles · 2019-08-02T15:14:10Z

Yea, that seems to be an existing bug - I've reported dhall-lang/dhall-haskell#1193 as a minimal repro (which happens regardless of my work).

With regards to your comment, that is permitted. If you have a fresh REPL session:

⊢ {a : Kind} //\\ {b : Kind}

{ a : Kind, b : Kind }

As expected.

ocharles · 2019-08-07T20:19:03Z

How do people feel about 59aa4ee as a first stab? I need to define what the ⋁ judgement is, but that's trivial. Alternatively, rather than mentioning how to cons a Type, Kind or Sort on, I could just say T : S and then S ⋁ t or something

sjakobi · 2019-08-07T20:34:22Z

Looks pretty good to me so far! I believe the judgments for the operations (selection, projection, merges, possibly merge and toMap) need work too, though.

ocharles · 2019-08-07T20:40:27Z

Oh sure, plenty more work - just taking it one step at a time.

Nadrieril · 2019-08-07T20:50:47Z

Alternatively, rather than mentioning how to cons a Type, Kind or Sort on, I could just say T : S and then S ⋁ t or something

That would be nice. I think we'd need something like a const(S) predicate, that holds only for Type, Kind and Sort; that'd allow simplifying the various record-merging operations as well.

Nadrieril · 2019-08-07T20:53:48Z

I believe that

    Γ ⊢ T :⇥ Sort
    ────────────────────
    Γ ⊢ { x : T } : Sort

is now redundant, since it's a special case of

    Γ ⊢ T :⇥ Sort   Γ ⊢ { xs… } :⇥ t
    ────────────────────────────────  ; x ∉ { xs… }
    Γ ⊢ { x : T, xs… } : Sort ⋁ t

when xs is empty.
Same thing with the similar rule with Kind.

ocharles · 2019-08-07T20:54:30Z

I think we'd need something like a const(S)

That, or s \elem {Type, Kind Sort}. const may be a better judgement.

Gabriella439

Looks great so far!

standard/type-inference.md

ocharles · 2019-08-08T08:40:12Z

Ok, I've now added ⋁ to function-check.md as a judgement, and I think this really tidies things up. Let me know what you think. Perhaps there is a better way of defining ⋁, but I went for what I thought was the clearest definition.

ocharles · 2019-08-08T08:54:07Z

Ok, I've tried to update the record merge type inference rules too.

ocharles · 2019-08-08T08:56:36Z

standard/type-inference.md



    Γ ⊢ l :⇥ { ls… }
-    { ls… } :⇥ Type
+    { ls… } :⇥ t


Do I need to say t \elem { Type, Kind, Sort }? This comment applies to various other places where I've replaced Type with a metavariable.

Here you don't, because a record type can only have type Type, Kind or Sort

ocharles · 2019-08-08T16:41:08Z

Ok, I think I've addressed those comments. Let me know if I've gone too far with some of the deletions...

Gabriella439

Looks great! Thank you for doing this 🙂

One thing we should do (which can be a follow-up change) is to update the Prelude to take advantage of this

ocharles · 2019-08-09T17:09:15Z

Yea, I think the Prelude is a separate PR. I like to keep changes in PRs be "required to change" rather than "could now be changed".

ocharles · 2019-08-09T17:10:45Z

To clarify, do I need to wait 3 days now? Or does mergify take care of waiting for 3 days? If we have to wait, I'll just merge on Monday.

sjakobi · 2019-08-09T17:38:51Z

To clarify, do I need to wait 3 days now?

In https://github.com/dhall-lang/dhall-lang/blob/master/.github/CONTRIBUTING.md#how-do-changes-get-approved we have

If the change is approved quickly, there is still a minimum 3-day waiting period before merging for changes to the standard.

My interpretation is that a PR should be merged no earlier than 3 days after the last change to the patch.

Or does mergify take care of waiting for 3 days?

Mergify is only enabled for the dhall-haskell repo, not this one. @Gabriel439 is becoming quite the Mergify-expert though, so maybe that will change. :)

Gabriella439 · 2019-08-09T17:41:56Z

@ocharles: The full rules are here:

https://github.com/dhall-lang/dhall-lang/blob/master/.github/CONTRIBUTING.md#how-do-changes-get-approved

This repository is not Mergify-enabled, so you just have to know how long to wait according to those rules.

We don't have clear rules around when the "clock" begins for draft pull requests. My rough rule is to reset the clock after each change, meaning:

If I updated the standard/Prelude and I already have all three approvals, wait up to 3 more days before merging
If I updated the standard/Prelude and I don't have all three approvals, wait up to 7 more days before merging

If you get all three approvals in the interim, then only wait up to 3 days
If I only updated tests, and I have all three approvals, wait just 1 more day before merging

Given that we only have one approval so far, we should wait up to 7 days to give the other two approvers a chance to comment. If they don't comment then it's an implicit approval and then you can merge. If they both approve then you can merge after just a 3-day wait.

ocharles · 2019-08-09T17:47:32Z

Super, thanks for the info.

ocharles · 2019-08-09T18:00:07Z

I've created a new label "Voting Open" just to indicate that the author deems the work finished and is now looking for votes.

sjakobi

I have a few inline comments.

Also: Can you check the rules for field selection? I believe they can be relaxed. If so, please add tests for them.

And does your branch for dhall-haskell already pass all the acceptance tests?

standard/function-check.md

sjakobi · 2019-08-09T17:46:49Z

standard/function-check.md

+
+
+... where `t₀` and `t₁` are either `Type`, `Kind`, or `Sort` (though they may
+differ).


though they may differ

Should that mean that t₀ and t₁ don't have to be the same?

Would

... where t₀ and t₁ each are either Type, Kind, or Sort.

be clearer?!

I was trying to emphasize that t₀ = Type and t₁ = Sort is valid. I may have made things more confusing, but I don't have a better suggestion. I'm open to changes here, if anyone wants to suggest anything! Happen to use your wording @sjakobi if it's clearer.

standard/type-inference.md

standard/function-check.md

Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>

f-f

Thank you for doing this! 🙂

philandstuff

Looks great from an admittedly superficial skim. I spotted a minor presentation fix but nothing else.

standard/type-inference.md

Co-Authored-By: Philip Potter <philip.g.potter@gmail.com>

ocharles · 2019-08-15T10:33:40Z

@sjakobi dhall-lang/dhall-haskell#1173 passes all the tests added here, but fails due to some unrelated changes. Am I good to merge this PR (the standard change)?

sjakobi

Cheers! Sorry for the delay!

ocharles · 2019-08-16T08:40:36Z

And we're done! Thanks for the help, all!

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

Standardize records of mixed kinds

cbcfa37

Undo a move

695d44f

ocharles added 2 commits August 2, 2019 15:40

Check { a = Kind } does not type check

a1795eb

Test { a = 0} // { a = Bool } : { a : Type }

760debb

Test recursive record type merges of mixed kinds

7db2ed3

ocharles added 2 commits August 5, 2019 12:55

Merge branch 'master' into mixed-records

332583a

First stab at standardising mixed record types

59aa4ee

Gabriella439 reviewed Aug 8, 2019

View reviewed changes

standard/type-inference.md Outdated Show resolved Hide resolved

standard/type-inference.md Outdated Show resolved Hide resolved

Add ⋁ judgement

34098e5

ocharles added 2 commits August 8, 2019 09:40

Typo

9d8488c

Update record merge rules

5c92a13

ocharles commented Aug 8, 2019

View reviewed changes

Gabriella439 approved these changes Aug 9, 2019

View reviewed changes

ocharles changed the title ~~Standardize records of mixed kinds (wip)~~ Standardize records of mixed kinds Aug 9, 2019

ocharles mentioned this pull request Aug 9, 2019

Restore support for records containing both types and terms dhall-lang/dhall-haskell#1173

Merged

ocharles added the Voting Open label Aug 9, 2019

sjakobi reviewed Aug 9, 2019

View reviewed changes

ocharles and others added 2 commits August 9, 2019 19:54

Update standard/function-check.md

8871425

Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>

Update standard/type-inference.md

2d10378

Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>

f-f approved these changes Aug 9, 2019

View reviewed changes

philandstuff approved these changes Aug 11, 2019

View reviewed changes

standard/type-inference.md Outdated Show resolved Hide resolved

ocharles and others added 3 commits August 12, 2019 12:49

Use ALLCAPS when you spell the (type) name

b6d8721

Update standard/type-inference.md

9f3ced1

Co-Authored-By: Philip Potter <philip.g.potter@gmail.com>

Merge branch 'master' into mixed-records

cec99d6

singpolyma approved these changes Aug 15, 2019

View reviewed changes

Merge branch 'master' into mixed-records

3014d90

ocharles added a commit to circuithub/dhall-haskell that referenced this pull request Aug 15, 2019

Use latest commit from dhall-lang/dhall-lang#689

ae90df3

sjakobi approved these changes Aug 15, 2019

View reviewed changes

Merge branch 'master' into mixed-records

caa3a5b

ocharles merged commit 0c335d3 into master Aug 16, 2019

ocharles deleted the mixed-records branch August 16, 2019 08:40

sjakobi mentioned this pull request Aug 19, 2019

Mixed records of values and types #658

Closed

Gabriella439 pushed a commit to dhall-lang/dhall-haskell that referenced this pull request Aug 31, 2019

Restore support for records containing both types and terms (#1173)

2877525

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



		... where `t₀` and `t₁` are either `Type`, `Kind`, or `Sort` (though they may
		differ).

Standardize records of mixed kinds #689

Standardize records of mixed kinds #689

Conversation

ocharles commented Aug 2, 2019

ocharles commented Aug 2, 2019

sjakobi commented Aug 2, 2019 • edited Loading

ocharles commented Aug 2, 2019 • edited Loading

sjakobi commented Aug 2, 2019

ocharles commented Aug 2, 2019

ocharles commented Aug 2, 2019

sjakobi commented Aug 2, 2019 • edited Loading

ocharles commented Aug 2, 2019 • edited Loading

sjakobi commented Aug 2, 2019

ocharles commented Aug 2, 2019

ocharles commented Aug 7, 2019 • edited Loading

sjakobi commented Aug 7, 2019

ocharles commented Aug 7, 2019

Nadrieril commented Aug 7, 2019 • edited Loading

Nadrieril commented Aug 7, 2019

ocharles commented Aug 7, 2019

Gabriella439 left a comment

Choose a reason for hiding this comment

ocharles commented Aug 8, 2019

ocharles commented Aug 8, 2019

ocharles Aug 8, 2019 • edited Loading

Choose a reason for hiding this comment

Nadrieril Aug 8, 2019

Choose a reason for hiding this comment

ocharles commented Aug 8, 2019

Gabriella439 left a comment

Choose a reason for hiding this comment

ocharles commented Aug 9, 2019

ocharles commented Aug 9, 2019

sjakobi commented Aug 9, 2019

Gabriella439 commented Aug 9, 2019

ocharles commented Aug 9, 2019

ocharles commented Aug 9, 2019

sjakobi left a comment

Choose a reason for hiding this comment

sjakobi Aug 9, 2019

Choose a reason for hiding this comment

ocharles Aug 9, 2019

Choose a reason for hiding this comment

f-f left a comment

Choose a reason for hiding this comment

philandstuff left a comment

Choose a reason for hiding this comment

ocharles commented Aug 15, 2019

sjakobi left a comment

Choose a reason for hiding this comment

ocharles commented Aug 16, 2019

sjakobi commented Aug 2, 2019 •

edited

Loading

ocharles commented Aug 2, 2019 •

edited

Loading

sjakobi commented Aug 2, 2019 •

edited

Loading

ocharles commented Aug 2, 2019 •

edited

Loading

ocharles commented Aug 7, 2019 •

edited

Loading

Nadrieril commented Aug 7, 2019 •

edited

Loading

ocharles Aug 8, 2019 •

edited

Loading