Restore support for records containing both types and terms #1173

ocharles · 2019-07-30T11:34:19Z

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

sjakobi · 2019-07-30T13:16:42Z

This makes sense to me so far – but I don't know much about these things.

I think you should probably also adjust the typechecking for /\, // (and probably //\\ too?). In both cases we currently check that the two records have the same kind, which I assume we don't want to check anymore. That would allow something like

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

ocharles · 2019-07-30T13:23:00Z

Thanks @sjakobi - I wasn't sure if that was explicitly checked in the type checker. I'll have a look and update that.

Gabriella439

This looks good so far, just one comment

dhall/src/Dhall/TypeCheck.hs

…tore-mixed-records

ocharles · 2019-07-31T11:29:45Z

This is getting there, but I'm stuck on what to do with one test case. The test input is:

{ x = Type, y = Kind }

Which does have a type - it has type

{ x : Kind, y : Sort }

However, the current test harness can't actually verify this, because the expected type is itself type checked, and { x : Kind, y : Sort } does not have a type (because Sort doesn't have a type).

Should I reject RecordLits that contain Kinds?

Gabriella439 · 2019-07-31T15:56:12Z

@ocharles: Yes, I believe you would need to reject records that contain fields set to Kind. This is actually not a consequence of the test harness limitations but rather a consequence of the rule that record literal's inferred type must itself type-check, and a record type with a Sort in it is not valid.

ocharles · 2019-07-31T16:49:36Z

Thanks for the clarification - I'll see what I can do.

…tore-mixed-records

MonoidMusician · 2019-08-06T16:02:23Z

Nice! Did you see this issue: dhall-lang/dhall-lang#558 ? It might be nice to put it in with this change, but we can always take care of it in a separate PR too – up to you.

…tore-mixed-records

…askell into restore-mixed-records

sjakobi

Can you make sure the full acceptance testsuite passes, before you merge dhall-lang/dhall-lang#689?

dhall/src/Dhall/TypeCheck.hs

sjakobi · 2019-08-19T15:20:53Z

dhall/src/Dhall/TypeCheck.hs


-                kts <- Dhall.Map.unorderedTraverseWithKey process kvs'
+        _ <- loop ctx recordType


Why is this check necessary? If it is necessary, do we have a test for it?

It's required by the standard, but it might be redundant now that we permit mixed records. In other words, this additional check required by the standard might not actually catch anything that the other checks do so there wouldn't be a differentiating test, but the standard would need to be fixed.

Either way I'll remove it as I'm reasonably sure it's no longer necessary and the standard change can follow

dhall/src/Dhall/TypeCheck.hs

sjakobi · 2019-08-19T15:23:33Z

dhall/src/Dhall/TypeCheck.hs

@@ -546,19 +527,15 @@ typeWithA tpa = loop
            _          -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY))

        ttKvsX <- fmap Dhall.Core.normalize (loop ctx tKvsX)
-        constX <- case ttKvsX of
+        _      <- case ttKvsX of
            Const constX -> return constX


Just return ().

Or is this check necessary at all?

It is not necessary any longer, so I'll remove it. One invariant of the type system is that the type of the type of something will always be a type-checking constant (i.e. Const) so if we don't care about the specific constant then we no longer need to check this

sjakobi · 2019-08-19T15:23:40Z

dhall/src/Dhall/TypeCheck.hs

            Const constX -> return constX
            _            -> Left (TypeError ctx e (MustCombineARecord '∧' kvsX tKvsX))

        ttKvsY <- fmap Dhall.Core.normalize (loop ctx tKvsY)
-        constY <- case ttKvsY of
+        _      <- case ttKvsY of
            Const constY -> return constY


dhall/src/Dhall/TypeCheck.hs

sjakobi · 2019-08-19T15:32:23Z

dhall/src/Dhall/TypeCheck.hs

@@ -621,19 +590,15 @@ typeWithA tpa = loop
            _          -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY))

        ttKvsX <- fmap Dhall.Core.normalize (loop ctx tKvsX)
-        constX <- case ttKvsX of
+        _      <- case ttKvsX of
            Const constX -> return constX


Same comments as for Combine.

…/dhall-haskell into circuithub-restore-mixed-records

@sjakobi

... as suggested by @sjakobi

@sjakobi

... as caught by @sjakobi I will also upstream this into the standard

@sjakobi

... as caught by @sjakobi

@sjakobi

... as caught by @sjakobi

Gabriella439 · 2019-08-31T16:36:34Z

@ocharles: I opened a pull request against your branch to fix the test failure and address the review feedback: circuithub#1

Address review feedback for mixed records pull request

ocharles · 2019-08-31T17:13:59Z

Thanks for that! It was a little hard to do the review but I trust you and am not too invested in how this work is done - the standard and understanding the changes was more important to me. As such, I've just gone ahead and merged your PR. Also, I'm not sure if you're aware but GitHub will let you push changes directly to my branch, so feel free to push more fixes directly here. I will also try and help next week to push this over the line. Cheers!

…

On Sat, 31 Aug 2019, 5:36 pm Gabriel Gonzalez, ***@***.***> wrote: @ocharles <https://github.com/ocharles>: I opened a pull request against your branch to fix the test failure and address the review feedback: circuithub#1 <circuithub#1> — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1173?email_source=notifications&email_token=AAAFDDUTLJNR2XIWNLJ5DNTQHKMZHA5CNFSM4IH3K7SKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD5TQKIQ#issuecomment-526845218>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAAFDDXDCE25FR2ILQV7IGLQHKMZHANCNFSM4IH3K7SA> .

Restore support for records containing both types and terms

15b31b3

ocharles added the wip Work in progress - the author is not yet asking for reviews label Jul 30, 2019

ocharles mentioned this pull request Jul 30, 2019

Mixed records of values and types dhall-lang/dhall-lang#658

Closed

ocharles added 2 commits July 30, 2019 18:17

Permit Combine to have different record types

60c3044

CombineTypes with types and kinds

8653e2f

Gabriella439 reviewed Jul 31, 2019

View reviewed changes

dhall/src/Dhall/TypeCheck.hs Show resolved Hide resolved

sjakobi reviewed Jul 31, 2019

View reviewed changes

dhall/src/Dhall/TypeCheck.hs Show resolved Hide resolved

ocharles added 7 commits July 31, 2019 11:14

Remove RecordMismatch from Prefer

0c52120

Type check the type of RecordLit Records

b56a358

Update dhall-lang

418464b

Warnings

f3e6c9a

Only allow toMap on records of terms

cffb50d

Merge branch 'master' of github.com:dhall-lang/dhall-haskell into res…

b3683a8

…tore-mixed-records

Update tests

4d032c9

ocharles added 2 commits August 2, 2019 14:48

Merge branch 'master' of github.com:dhall-lang/dhall-haskell into res…

15726a8

…tore-mixed-records

Correct dhall-lang commit

2e4c0d4

ocharles mentioned this pull request Aug 2, 2019

Standardize records of mixed kinds dhall-lang/dhall-lang#689

Merged

Remove an unnecessary change

919e8e3

Merge branch 'master' of github.com:dhall-lang/dhall-haskell into res…

4ff1f5e

…tore-mixed-records

ocharles removed the wip Work in progress - the author is not yet asking for reviews label Aug 9, 2019

ocharles changed the title ~~Restore support for records containing both types and terms (WIP)~~ Restore support for records containing both types and terms Aug 9, 2019

Merge branch 'restore-mixed-records' of github.com:circuithub/dhall-h…

155852c

…askell into restore-mixed-records

sjakobi reviewed Aug 10, 2019

View reviewed changes

Merge branch 'master' into restore-mixed-records

2dc8fe3

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

ae90df3

ocharles mentioned this pull request Aug 19, 2019

Update dhall-lang submodule, skip test failures #1240

Merged

sjakobi requested changes Aug 19, 2019

View reviewed changes

Gabriella439 added 7 commits August 31, 2019 09:09

Merge branch 'restore-mixed-records' of https://github.com/circuithub…

2d02c2f

…/dhall-haskell into circuithub-restore-mixed-records

Restore tests that are now fixed

4099483

Remove unused FieldAnnotationMismatch constructor

9ff1ed3

... as suggested by @sjakobi

Remove superfluous check of the derived record type

3735cc8

... as caught by @sjakobi I will also upstream this into the standard

Remove unused FieldMismatch constructor

3ffb5d2

... as caught by @sjakobi

Remove obsolete type checks

e7eb73f

... as caught by @sjakobi

Remove unused RecordMismatch constructor

29b5152

Merge pull request #1 from dhall-lang/circuithub-restore-mixed-records

226fb81

Address review feedback for mixed records pull request

Merge branch 'master' into restore-mixed-records

e996ca9

sjakobi approved these changes Aug 31, 2019

View reviewed changes

Add missing test files to dhall.cabal

fa2dd41

Gabriella439 merged commit 2877525 into dhall-lang:master Aug 31, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Restore support for records containing both types and terms #1173

Restore support for records containing both types and terms #1173

ocharles commented Jul 30, 2019 •

edited

Loading

sjakobi commented Jul 30, 2019

ocharles commented Jul 30, 2019

Gabriella439 left a comment

ocharles commented Jul 31, 2019

Gabriella439 commented Jul 31, 2019 •

edited

Loading

ocharles commented Jul 31, 2019

MonoidMusician commented Aug 6, 2019

sjakobi left a comment

sjakobi Aug 19, 2019

Gabriella439 Aug 31, 2019

Gabriella439 Aug 31, 2019

sjakobi Aug 19, 2019

sjakobi Aug 19, 2019

Gabriella439 Aug 31, 2019

sjakobi Aug 19, 2019

sjakobi Aug 19, 2019

Gabriella439 commented Aug 31, 2019

ocharles commented Aug 31, 2019 via email


		kts <- Dhall.Map.unorderedTraverseWithKey process kvs'
		_ <- loop ctx recordType

Restore support for records containing both types and terms #1173

Restore support for records containing both types and terms #1173

Conversation

ocharles commented Jul 30, 2019 • edited Loading

sjakobi commented Jul 30, 2019

ocharles commented Jul 30, 2019

Gabriella439 left a comment

Choose a reason for hiding this comment

ocharles commented Jul 31, 2019

Gabriella439 commented Jul 31, 2019 • edited Loading

ocharles commented Jul 31, 2019

MonoidMusician commented Aug 6, 2019

sjakobi left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Gabriella439 commented Aug 31, 2019

ocharles commented Aug 31, 2019 via email

ocharles commented Jul 30, 2019 •

edited

Loading

Gabriella439 commented Jul 31, 2019 •

edited

Loading