Record projection by expression

standard/alpha-normalization.md

@@ -322,6 +322,11 @@ sub-expressions for the remaining rules:
     { x = t₀, xs₀… } ↦ { x = t₁, xs₁… }
 
 
+    s₀ ↦ s₁   t₀ ↦ t₁
+    ────────────────
+    s₀.(t₀) ↦ s₁.(t₁)
+
+
     ───────
     <> ↦ <>
 

standard/beta-normalization.md

@@ -933,6 +933,24 @@ You can also project out more than one field into a new record:
     t.{ x, xs… } ⇥ { x = v, ys… }
 
 
+    s ⇥ {}
+    ──────────
+    t.(s) ⇥ {=}
+
+
+    t ⇥ { x = v, ts₀… }
+    s ⇥ { x : T, ts₀… }
+    t.({ ss… }) ⇥ { ts₁… }
+    ───────────────────────
+    t.(s) ⇥ { x = v, ts₁… }
+
+
+    t₀ ⇥ t₁
+    s₀ ⇥ s₁
+    ─────────────────  ; If no other rule matches
+    t₀.(s₀) ⇥ t₁.(s₁)
+
+
 The type system ensures that the selected field(s) must be present.
 
 Otherwise, normalize the argument:

standard/binary.md

@@ -508,6 +508,14 @@ Field access:
     encode(t₀.{ x, y, … }) = [ 10, t₁, "x", "y", … ]
 
 
+Record projection by type is encoded as follows:
+
+
+    encode(t₀) = t₁   encode(T₀) = T₁
+    ─────────────────────────────────
+    encode(t₀.(T₀)) = [ 19, t₁, T₁ ]
+
+
 ### Unions
 
 Dhall union types translate to CBOR maps:
@@ -1199,6 +1207,14 @@ Decode a CBOR array beginning with a `10` as a record projection:
     decode([ 10, t₁, "x", "y", … ]) = t₀.{ x, y, … }
 
 
+Similarly, decode a CBOR array beginning with a `` as a record projection by type:
+
+
+    decode(t₁) = t₀   decode(T₁) = T₀
+    ─────────────────────────────────
+    decode([ 19, t₁, T₁]) = t₀.(T₀)
+
+
 A decoder MUST NOT attempt to enforce uniqueness of keys.  That is the
 responsibility of the type-checking phase.
 

standard/dhall.abnf

@@ -407,7 +407,7 @@ natural-literal = 1*DIGIT
 integer-literal = ( "+" / "-" ) natural-literal
 
 ; If the identifier matches one of the names in the `builtin` rule, then it is a
-; builtin, and should be treated as the curresponding item in the list of
+; builtin, and should be treated as the corresponding item in the list of
 ; "Reserved identifiers for builtins" specified in the `semantics.md` document.
 ; It is a syntax error to specify a de Bruijn index in this case.
 ; Otherwise, this is a variable with name and index matching the label and index.
@@ -717,10 +717,11 @@ import-expression = import / selector-expression
 ; the function `foo` to the relative path `./bar`)
 selector-expression = primitive-expression *(whsp "." whsp selector)
 
-selector = any-label / labels
+selector = any-label / labels / type-selector
 
 labels = "{" whsp [ any-label whsp *("," whsp any-label whsp) ] "}"
 
+type-selector = "(" whsp expression whsp ")"
 ; NOTE: Backtrack when parsing the first three alternatives (i.e. the numeric
 ; literals).  This is because they share leading characters in common
 primitive-expression =

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… }
+    Γ ⊢ s : T
+    s ⇥ { ss… }
+    ───────────────────────────────────────────  ; ss ⊆ ts
+    Γ ⊢ e.(s) : { ss… }
 
 
     Γ ⊢ e :⇥ { x : T, ts₀… }   Γ ⊢ e.{ xs… } :⇥ { ts₁… }

tests/normalization/success/unit/RecordProjectionTypeEmptyA.dhall

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

tests/normalization/success/unit/RecordProjectionTypeEmptyB.dhall

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

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 }

tests/normalization/success/unit/RecordProjectionTypeNonEmptyB.dhall

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

tests/parser/success/RecordProjectionByType.dhall

@@ -0,0 +1,15 @@
+let example1 = λ(A : Type) → λ(B : Type) → λ(C : { x : A, y : B }) → C.({ x : A }) : { x : A }
+
+let example2 =
+	  λ(A : Type)
+	→ λ(B : Type)
+	→ λ(C : { p : A, q : B })
+	→ C.(let r = { p : A } in r) : { p : A }
+
+let A = Natural
+
+let B = Text
+
+in
+
+(example1 A B { x = 10, y = "Text" }) ∧ (example2 A B { p = 10, q = "Text" }) : { x : A, p : A }

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 }