Record projection by expression #499

dingxiangfei2009 · 2019-04-21T13:08:01Z

Close #183, replacing #494.

This PR extends record project by permitting expression normalising to records as the projection selector.

The highlight is that to project fields prescribed by an expression from a record, a round bracket is necessary, eg., r.(e).

dingxiangfei2009 · 2019-04-23T11:36:42Z

@Gabriel439 I noticed that #493 is quite relevant to this PR. I am thinking of expanding the scope of this work to address the requirement in that issue, though I am not sure if this is okay.

Gabriella439

There are two other things that need to be added:

How to α-normalize t.(s)
How to encode/decode t.(s) (i.e. in binary.md)

standard/semantics.md

Gabriella439 · 2019-04-23T14:03:43Z

standard/semantics.md

@@ -3894,6 +3906,16 @@ You can only select field(s) from the record if they are present:
    Γ ⊢ e.{ x } : { x : T }


+    Γ ⊢ e :⇥ { ts… } : Kind   Γ ⊢ s :⇥ { ss… } : Kind
+    ──────────────────────────────────────────────────── ; ss ⊆ ts
+    Γ ⊢ e.(s) : { ss… }


I believe that the type of e.(s) should be the normal form of s rather than the type of s. In other words:

Γ ⊢ e :⇥ { ts… } Γ ⊢ s : T s ⇥ { ss… } ─────────────────────────────────────────── ; ss ⊆ ts Γ ⊢ e.(s) : { ss… }

I also don't think you need the Kind/Sort type annotations. The type of the type of each record would be checked along the way as part of type-checking e and s

My idea is to make it explicit that, in order to type check e.(s), s should lie in a universe immediately above the one where e lives. But I am not sure how to express this constraint.

By the way, what is T in Γ ⊢ s : T ?

Think of Γ ⊢ s : T as pseudo-code for:

T <- inferTypeWithContext Γ s

In other words, Γ and s are the two inputs to the inferTypeWithContext function and T is the output of the function. In this case T is the inferred type of s

standard/semantics.md

Gabriella439 · 2019-04-23T14:10:57Z

@dingxiangfei2009: I think #493 should probably be handled as part of a separate pull request so that each change can be understood separately in the history

singpolyma · 2019-04-24T01:57:58Z

I would also request that unit test cases be added for each new rule.

dingxiangfei2009 · 2019-04-26T04:15:20Z

@Gabriel439 Speaking of adding a α-normalisation rule, though it is not immediately related, I find the deduction rules for ↑(d, x, m, ε) a bit under-specified. The deduction rules in standard/README.md never mention the situation for different values of d and m. The definition of the data in these tuples is lacking, too. Is there any literature I can refer to regarding this notation?

Nadrieril · 2019-04-26T10:34:10Z

@dingxiangfei2009 I may be wrong, but it sounds to me like you haven't seen this: https://github.com/dhall-lang/dhall-lang/blob/master/standard/shift.md . If you have, would you mind being more precise about what you find lacking ?

dingxiangfei2009 · 2019-04-26T12:54:29Z

@Nadrieril Ah, I see! It has what I want to read about.

Nadrieril · 2019-04-26T12:58:43Z

#509 should make it easier to spot which judgments are defined and where in the future.

…o selector-extension

standard/beta-normalization.md

Gabriella439 · 2019-05-06T15:08:30Z

standard/binary.md

+
+    encode(t₀) = t₁   encode(T₀) = T₁
+    ─────────────────────────────────
+    encode(t₀.(T₀)) = [ 27, t₁, T₁ ]


I suggest using 19 instead of 27, since record projection by type can survive β-normalization. For example, this is a well-typed expression that is in normal form:

λ(e : { x : Bool }) → e.({ x : Bool })

I see.

Is there any rule on how these numbers are assigned, for backward compatibility?

As mentioned here, we try to assign labels below 24 for syntactic features that survive normalization. Currently we use 0 to 18, except 13 and 17. 13 was used before so for backward-compatibility we want to reuse it as late as possible (see here). I don't know why 17 was skipped, but I'm assuming it is similar to 13. That means that the next free label is 19.

tests/parser/success/recordProjectByType.dhall

singpolyma · 2019-05-07T12:11:07Z

Why do we need a new label at all? The record projection label exists already and there will be no overlap with projection by name so I think we should just use that.

Gabriella439 · 2019-05-07T14:26:51Z

@singpolyma: Oh yeah, good point. We should probably use the same label as normal record projection

singpolyma · 2019-05-07T19:05:23Z

tests/normalization/success/unit/RecordProjectionTypeNonEmptyB.dhall

@@ -0,0 +1 @@
+{ a = 10, b = Some 10 }


missing newline

dhall format automatically removes the new line when I add it.

singpolyma · 2019-05-07T19:05:30Z

tests/normalization/success/unit/RecordProjectionTypeEmptyB.dhall

@@ -0,0 +1 @@
+{=}


missing newline

singpolyma · 2019-05-07T19:06:44Z

tests/normalization/success/unit/RecordProjectionTypeNonEmptyA.dhall

@@ -0,0 +1 @@
+{ a = 10, b = Some 10, c = [ "text" ]}.({ a : Natural, b : Optional Natural }) : { a : Natural, b : Optional Natural }


type annotation on the end here seems unneeded?

singpolyma · 2019-05-07T19:08:14Z

tests/type-inference/success/unit/RecordProjectionByType.dhall

@@ -0,0 +1 @@
+let e = { a = 10, b = "Text" } let s = { a : Natural } in e.(s) : { a : Natural }


this should be named A and have a B part with it -- the let seems like a lot of extra noise for a unit test.

Note that we should still have a test like this one, even if not necessarily for a unit test. It's important to test that type inference works when the s is an abstract type since that's a likely case that an implementation might implement incorrectly.

Gabriella439

This looks great! I think the only thing left is to see if we can have the binary encoding for e.(s) reuse the same label as for e.x like @singpolyma. Other than that I don't see anything missing

Gabriella439 · 2019-05-08T02:50:05Z

tests/type-inference/success/unit/RecordProjectionByType.dhall

@@ -0,0 +1 @@
+let e = { a = 10, b = "Text" } let s = { a : Natural } in e.(s) : { a : Natural }


Note that we should still have a test like this one, even if not necessarily for a unit test. It's important to test that type inference works when the s is an abstract type since that's a likely case that an implementation might implement incorrectly.

…o selector-extension

standard/beta-normalization.md

standard/binary.md

singpolyma · 2019-05-15T14:52:15Z

@singpolyma: Actually, I think this will lead to decoding ambiguity because now `e.(x)` and `e.{ x }` have the same encoding.

Not anymore. Variables always have their index encoded these days, not encoded as bare strings.

Gabriella439 · 2019-05-15T14:59:09Z

@singpolyma: Oh yeah, that's right. Ignore my concern, then.

Gabriella439 · 2019-05-15T15:54:52Z

I think the only thing missing is to add the expected inferred type for tests/type-inference/success/unit/RecordProjectionByType.dhall (i.e. rename it to tests/type-inference/success/unit/RecordProjectionByTypeA.dhall and add a tests/type-inference/success/unit/RecordProjectionByTypeB.dhall)

Signed-off-by: Ding Xiang Fei <dingxiangfei2009@gmail.com>

…o selector-extension

dingxiangfei2009 · 2019-05-21T04:01:02Z

Sorry for late response. Caught with some other business earlier this week. 😅

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

Gabriella439

Almost there! 🙂

I just implemented this in dhall-lang/dhall-haskell#958 and noticed a few small things along the way

standard/binary.md

Gabriella439 · 2019-05-22T02:42:48Z

standard/type-inference.md

@@ -501,6 +501,13 @@ You can only select field(s) from the record if they are present:
    Γ ⊢ e :⇥ { x : T, ts… }   Γ ⊢ { x : T, ts… } :⇥ Sort
    ────────────────────────────────────────────────────
    Γ ⊢ e.{ x } : { x : T }
+
+


Perhaps add some prose here explaining that the e.(t) syntax lets the user select record fields by type. Currently there isn't any text in the standard explaining this feature

Gabriella439 · 2019-05-22T02:55:07Z

standard/type-inference.md

@@ -501,6 +501,13 @@ You can only select field(s) from the record if they are present:
    Γ ⊢ e :⇥ { x : T, ts… }   Γ ⊢ { x : T, ts… } :⇥ Sort
    ────────────────────────────────────────────────────
    Γ ⊢ e.{ x } : { x : T }
+
+
+    Γ ⊢ e :⇥ { ts… }


This judgment needs to somehow enforce that { ts… } and { ss… } are syntactically record types. One way to do that is define the judgment via induction (i.e. define a judgment to type-check the case where the two record types are empty and then define a judgment to type-check the case where the two record types are non-empty), like this:

Γ ⊢ e :⇥ {} Γ ⊢ s : T s ⇥ {} ──────────────── Γ ⊢ e.(s) : {} Γ ⊢ e :⇥ { x : T₀, … } Γ ⊢ s : T s ⇥ { x : T₁, xs₁… } Γ ⊢ e.({ xs₁… }) : T ──────────────────────── Γ ⊢ e.(s) : { x : T₁ ,xs₁… }

@Gabriel439 For the base case, we can relax the requirement on e, since it is still sound, in the same universe, to project empty record from any record.

Also, do you think that the following induction step make sense?

Γ ⊢ e :⇥ { x : T₀, ts… } Γ ⊢ s : T₀ s ⇥ { x : T₀, ss… } Γ ⊢ e.({ ss… }) : T₁ ─────────────────────────── Γ ⊢ e.(s) : { x : T₀, ss… }

The concern is with the induction step that you suggested earlier, in which Γ ⊢ s : T and Γ ⊢ e.({ xs₁… }) : T cannot reconcile.

@Nadrieril: Oh yeah, the base case doesn't need to require that e is the empty record. That's a mistake on my part. Good catch!

Also, you're right that the two occurrences of T in the induction judgement should be distinct. That's another mistake on my part.

…o selector-extension

Gabriella439 · 2019-05-23T03:55:16Z

@singpolyma: Actually, I did run across an ambiguous encoding caught by the binary serialization round-trip property test. See:

https://hydra.dhall-lang.org/build/13281/nixlog/5

The issue is that a projection of an expression which is a built-in:

x.(Bool)

... and an expression projecting a quoted field of the same name:

x.{ `Bool` }

... share the same encoding. They are both encoded as:

[ 10, [ "x", 0 ], "Bool" ]

Technically, it's an ill-typed expression, but it still seems wrong to permit two different expressions to be encoded the same way.

It might be worth still using a different label just to avoid this potential ambiguity (and also to make it easier to write decoders).

Gabriella439 · 2019-05-23T15:00:51Z

Alternatively, we could add a "sub-label" to indicate that it's a record projection by type, perhaps by adding a null element, like this:

encode(e.(t)) = [ 10, encode(e), null, encode(t) ]

singpolyma · 2019-05-24T00:47:39Z

Hmm, ok. My initial reaction is that projection on a builtin is a crazy thing to do. But I suppose it's not impossible that a builtin that maps to a record type could ever be added to the language.

If they can't overlap, then I guess I don't feel strongly about label vs sub-label

Gabriella439 · 2019-05-24T16:00:37Z

@dingxiangfei2009: How about we do this, then: store the projection by type inside of another list so that it visually resembles the syntax:

encode(e.(t)) = [ 10, encode(e), [ encode(t) ] ]

dingxiangfei2009 · 2019-05-26T12:25:53Z

@Gabriel439 sounds like a better plan!

…o selector-extension

f-f

Looks great, thanks @dingxiangfei2009!

Gabriella439

Thank you for doing this! 🙂

Gabriella439 · 2019-05-28T03:02:21Z

I'll go ahead and merge this since you have all the approvals. Thanks again! 🙂

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

dingxiangfei2009 changed the title ~~Record projection by xpression~~ Record projection by expression Apr 21, 2019

record projection by expression

cd1e4f2

dingxiangfei2009 force-pushed the selector-extension branch from 56e6862 to cd1e4f2 Compare April 21, 2019 13:09

Gabriella439 reviewed Apr 23, 2019

View reviewed changes

f-f mentioned this pull request Apr 25, 2019

Row Type/Kind #494

Closed

dingxiangfei2009 added 4 commits May 6, 2019 21:07

Merge branch 'master' of https://github.com/dhall-lang/dhall-lang int…

db021b9

…o selector-extension

binary semantics

df19193

Merge branch 'master' of https://github.com/dhall-lang/dhall-lang int…

f5e109c

…o selector-extension

unit tests

ae4a168

Gabriella439 reviewed May 6, 2019

View reviewed changes

fix unit tests

f69e49b

singpolyma reviewed May 7, 2019

View reviewed changes

Gabriella439 reviewed May 8, 2019

View reviewed changes

switch tag from 19 to 9

6185c96

dingxiangfei2009 force-pushed the selector-extension branch from 48597d3 to 6185c96 Compare May 8, 2019 05:57

dingxiangfei2009 added 2 commits May 8, 2019 13:59

remove extraneous type annotation

4786493

Merge branch 'master' of https://github.com/dhall-lang/dhall-lang int…

8bbd6fc

…o selector-extension

philandstuff reviewed May 8, 2019

View reviewed changes

standard/beta-normalization.md Outdated Show resolved Hide resolved

remove redundant comment on record projection by type

5c92ee8

Gabriella439 reviewed May 15, 2019

View reviewed changes

standard/binary.md Outdated Show resolved Hide resolved

dingxiangfei2009 added 2 commits May 21, 2019 11:59

fix type inference unit test

e4d7928

Signed-off-by: Ding Xiang Fei <dingxiangfei2009@gmail.com>

Merge branch 'master' of https://github.com/dhall-lang/dhall-lang int…

94cf52e

…o selector-extension

singpolyma approved these changes May 22, 2019

View reviewed changes

Gabriella439 added a commit to dhall-lang/dhall-haskell that referenced this pull request May 22, 2019

Support projection by record type

c30c5cb

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

Gabriella439 mentioned this pull request May 22, 2019

Support projection by record type dhall-lang/dhall-haskell#958

Merged

Gabriella439 reviewed May 22, 2019

View reviewed changes

dingxiangfei2009 added 2 commits May 22, 2019 17:25

Merge branch 'master' of https://github.com/dhall-lang/dhall-lang int…

6f37451

…o selector-extension

decoding judgement of projection; type inference rule by induction

3d43c8a

dingxiangfei2009 added 2 commits May 26, 2019 20:28

push the type projection one level down in CBOR encoding

1c07554

Merge branch 'master' of https://github.com/dhall-lang/dhall-lang int…

0cc72ea

…o selector-extension

f-f approved these changes May 26, 2019

View reviewed changes

Gabriella439 approved these changes May 27, 2019

View reviewed changes

Merge branch 'master' into selector-extension

dedf45e

Gabriella439 merged commit 034d48a into dhall-lang:master May 28, 2019

Gabriella439 added a commit to dhall-lang/dhall-haskell that referenced this pull request May 28, 2019

Support projection by record type (#958)

3c08c62

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

philandstuff mentioned this pull request May 30, 2019

Expression for the Type/Kind of Record Type/Kind #434

Closed

Nadrieril mentioned this pull request Aug 3, 2019

Record projection by expression Nadrieril/dhall-rust#94

Closed

4 tasks

ari-becker mentioned this pull request Sep 2, 2020

Generalize record projection by expression to safe-casting #1063

Open

		@@ -0,0 +1 @@
		{ a = 10, b = Some 10, c = [ "text" ]}.({ a : Natural, b : Optional Natural }) : { a : Natural, b : Optional Natural }

		@@ -0,0 +1 @@
		let e = { a = 10, b = "Text" } let s = { a : Natural } in e.(s) : { a : Natural }

		@@ -0,0 +1 @@
		{=}

Record projection by expression #499

Record projection by expression #499

Conversation

dingxiangfei2009 commented Apr 21, 2019 • edited Loading

dingxiangfei2009 commented Apr 23, 2019

Gabriella439 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dingxiangfei2009 Apr 26, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Gabriella439 commented Apr 23, 2019

singpolyma commented Apr 24, 2019

dingxiangfei2009 commented Apr 26, 2019

Nadrieril commented Apr 26, 2019 • edited Loading

dingxiangfei2009 commented Apr 26, 2019

Nadrieril commented Apr 26, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

singpolyma commented May 7, 2019 via email

Gabriella439 commented May 7, 2019

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 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

singpolyma commented May 15, 2019 via email

Gabriella439 commented May 15, 2019

Gabriella439 commented May 15, 2019

dingxiangfei2009 commented May 21, 2019

Gabriella439 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dingxiangfei2009 May 22, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Gabriella439 May 22, 2019 • edited Loading

Choose a reason for hiding this comment

Gabriella439 commented May 23, 2019

Gabriella439 commented May 23, 2019

singpolyma commented May 24, 2019

Gabriella439 commented May 24, 2019

dingxiangfei2009 commented May 26, 2019

f-f left a comment

Choose a reason for hiding this comment

Gabriella439 left a comment

Choose a reason for hiding this comment

Gabriella439 commented May 28, 2019

dingxiangfei2009 commented Apr 21, 2019 •

edited

Loading

dingxiangfei2009 Apr 26, 2019 •

edited

Loading

Nadrieril commented Apr 26, 2019 •

edited

Loading

dingxiangfei2009 May 22, 2019 •

edited

Loading

Gabriella439 May 22, 2019 •

edited

Loading