From 022105eefee605f6e5b862b9d7816862b9db73e2 Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Mon, 5 Nov 2018 21:34:39 -0800 Subject: [PATCH] Add support for `let` expressions with multiple `let` bindings Fixes #260 In other words, this is now legal: ```haskell let x = 1 let y = 2 in x + y ``` --- standard/dhall.abnf | 3 +- standard/semantics.md | 169 +++++++++++++++++++++++++++++++++++++++--- 2 files changed, 161 insertions(+), 11 deletions(-) diff --git a/standard/dhall.abnf b/standard/dhall.abnf index 153257669..4eecdf4a6 100644 --- a/standard/dhall.abnf +++ b/standard/dhall.abnf @@ -578,7 +578,8 @@ expression = ; "let x : t = e1 in e2" ; "let x = e1 in e2" - / let label [ colon expression ] equal expression in expression + ; "let x = e1 let y = e2 in e3" + / 1*(let label [ colon expression ] equal expression) in expression ; "forall (x : a) -> b" / forall open-parens label colon expression close-parens arrow expression diff --git a/standard/semantics.md b/standard/semantics.md index 1168803d7..9328406a5 100644 --- a/standard/semantics.md +++ b/standard/semantics.md @@ -262,6 +262,10 @@ t : Naked label which could be any type of expression. pairs. The specified alternative is named `x₀ with value of `t₀`. At least one alternative is named `x₁` with a type of `T₁`. + + +let xs… in b : A `let` definition with at least one bindings +let x : A = a let xs… in b : A `let` definition with at least two bindings ``` You will see this notation in judgments that perform induction on lists, @@ -435,16 +439,32 @@ Descend as normal if the bound variable name does not match: when descending past such a bound variable: - ↑(d, x, m, A₀) = A₁ ↑(d, x, m, a₀) = a₁ ↑(d, x, m + 1, b₀) = b₁ - ─────────────────────────────────────────────────────────────────── + ↑(d, x, m, A₀) = A₁ + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m + 1, b₀) = b₁ + ───────────────────────────────────────────────────────── ↑(d, x, m, let x : A₀ = a₀ in b₀) = let x : A₁ = a₁ in b₁ - ↑(d, x, m, a₀) = a₁ ↑(d, x, m + 1, b₀) = b₁ + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m + 1, b₀) = b₁ ─────────────────────────────────────────────── ↑(d, x, m, let x = a₀ in b₀) = let x = a₁ in b₁ + ↑(d, x, m, A₀) = A₁ + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m + 1, let xs₀… in b₀) = let xs₁… in b₁ + ─────────────────────────────────────────────────────────────────────────── + ↑(d, x, m, let x : A₀ = a₀ let xs₀… in b₀) = let x : A₁ = a₁ let xs₁… in b₁ + + + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m + 1, let xs₀… in b₀) = let xs₁… in b₁ + ───────────────────────────────────────────────────────────────── + ↑(d, x, m, let x = a₀ let xs₀… in b₀) = let x = a₁ let xs₁… in b₁ + + Again, the bound variable, `x`, is not in scope for its own type, `A₀`, so do not increase the lower bound, `m`, when shifting the bound variable's type. @@ -456,16 +476,33 @@ of the assignment. Descend as normal if the bound variable name does not match: - ↑(d, x, m, A₀) = A₁ ↑(d, x, m, a₀) = a₁ ↑(d, x, m, b₀) = b₁ - ─────────────────────────────────────────────────────────────── ; x ≠ y + ↑(d, x, m, A₀) = A₁ + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m, b₀) = b₁ + ───────────────────────────────────────────────────────── ; x ≠ y ↑(d, x, m, let y : A₀ = a₀ in b₀) = let y : A₁ = a₁ in b₁ - ↑(d, x, m, a₀) = a₁ ↑(d, x, m, b₀) = b₁ + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m, b₀) = b₁ ─────────────────────────────────────────────── ; x ≠ y ↑(d, x, m, let y = a₀ in b₀) = let y = a₁ in b₁ + ↑(d, x, m, A₀) = A₁ + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m, let ys₀… in b₀) = let ys₁… in b₁ + ─────────────────────────────────────────────────────────────────────────── ; x ≠ y + ↑(d, x, m, let y : A₀ = a₀ let ys₀… in b₀) = let y : A₁ = a₁ let ys₁… in b₁ + + + ↑(d, x, m, a₀) = a₁ + ↑(d, x, m, b₀) = b₁ + ↑(d, x, m, let ys₀… in b₀) = let ys₁… in b₁ + ───────────────────────────────────────────────────────────────── ; x ≠ y + ↑(d, x, m, let y = a₀ let ys₀… in b₀) = let y = a₁ let ys₁… in b₁ + + ### Imports You can shift expressions with unresolved imports because the language enforces @@ -968,16 +1005,50 @@ All of the following rules cover expressions that can bind variables: (let y : A₀ = a₀ in b₀)[x@n ≔ e₀] = let y : A₁ = a₁ in b₁ - a₀[x@n ≔ e₀] = a₁ ↑(1, x, 0, e₀) = e₁ b₀[x@(1 + n) ≔ e₁] = b₁ - ───────────────────────────────────────────────────────────────── + a₀[x@n ≔ e₀] = a₁ + ↑(1, x, 0, e₀) = e₁ + b₀[x@(1 + n) ≔ e₁] = b₁ + ─────────────────────────────────────────────── (let x = a₀ in b₀)[x@n ≔ e₀] = let x = a₁ in b₁ - a₀[x@n ≔ e₀] = a₁ ↑(1, y, 0, e₀) = e₁ b₀[x@n ≔ e₁] = b₁ - ─────────────────────────────────────────────────────────── ; x ≠ y + a₀[x@n ≔ e₀] = a₁ + ↑(1, y, 0, e₀) = e₁ + b₀[x@n ≔ e₁] = b₁ + ────────────────────────────────────────────── ; x ≠ y (let y = a₀ in b₀)[x@n ≔ e₀] = let y = a₁ in b₁ + A₀[x@n ≔ e₀] = A₁ + a₀[x@n ≔ e₀] = a₁ + ↑(1, x, 0, e₀) = e₁ + (let xs₀… in b₀)[x@(1 + n) ≔ e₁] = let xs₁… in b₁ + ─────────────────────────────────────────────────────────────────────────── + (let x : A₀ = a₀ let xs₀… in b₀)[x@n ≔ e₀] = let x : A₁ = a₁ let xs₁… in b₁ + + + A₀[x@n ≔ e₀] = A₁ + a₀[x@n ≔ e₀] = a₁ + ↑(1, y, 0, e₀) = e₁ + (let xs₀… in b₀)[x@n ≔ e₁] = let xs₁… in b₁ + ─────────────────────────────────────────────────────────────────────────── ; x ≠ y + (let y : A₀ = a₀ let ys₀… in b₀)[x@n ≔ e₀] = let y : A₁ = a₁ let ys₁… in b₁ + + + a₀[x@n ≔ e₀] = a₁ + ↑(1, x, 0, e₀) = e₁ + (let xs₀… in b₀)[x@(1 + n) ≔ e₁] = let xs₁… in b₁ + ───────────────────────────────────────────────────────────────── + (let x = a₀ let xs₀… in b₀)[x@n ≔ e₀] = let x = a₁ let xs₁… in b₁ + + + a₀[x@n ≔ e₀] = a₁ + ↑(1, y, 0, e₀) = e₁ + (let ys₀… in b₀)[x@n ≔ e₁] = let ys₁… in b₁ + ───────────────────────────────────────────────────────────────── ; x ≠ y + (let y = a₀ let ys₀… in b₀)[x@n ≔ e₀] = let y = a₁ let ys₁… in b₁ + + ### Imports You can substitute expressions with unresolved imports because the language @@ -1435,6 +1506,38 @@ capture: let x = a₀ in b₀ ↦ let _ = a₁ in b₄ + a₀ ↦ a₁ + A₀ ↦ A₁ + let xs₀… in b₀ ↦ let xs₁… in b₁ + ─────────────────────────────────────────────────────────────── + let _ = a₀ : A₀ let xs₀… in b₀ ↦ let _ = a₁ : A₁ let xs₁… in b₁ + + + a₀ ↦ a₁ + A₀ ↦ A₁ + ↑(1, _, 0, b₀) = b₁ + b₁[x ≔ _] = b₂ + ↑(-1, x, 0, b₂) = b₃ + let xs₀… in b₃ ↦ let xs₁… in b₄ + ─────────────────────────────────────────────────────────────── x ≠ _ + let x = a₀ : A₀ let xs₀… in b₀ ↦ let _ = a₁ : A₁ let xs₁… in b₄ + + + a₀ ↦ a₁ + let xs₀… in b₀ ↦ let xs₁… in b₁ + ───────────────────────────────────────────────────── + let _ = a₀ let xs₀… in b₀ ↦ let _ = a₁ let xs₁… in b₁ + + + a₀ ↦ a₁ + ↑(1, _, 0, b₀) = b₁ + b₁[x ≔ _] = b₂ + ↑(-1, x, 0, b₂) = b₃ + let xs₀… in b₃ ↦ let xs₁… in b₄ + ───────────────────────────────────────────────────── x ≠ _ + let x = a₀ let xs₀… in b₀ ↦ let _ = a₁ let xs₁… in b₄ + + ### Variables Variables are already in α-normal form: @@ -2981,6 +3084,26 @@ equivalence: let x = a₀ in b₀ ⇥ b₃ +A `let` expression with multiple `let` bindings is equivalent to nested `let` +expressions: + + + ↑(1, x, 0, a₀) = a₁ + (let xs… in b₀)[x ≔ a₁] = b₁ + ↑(-1, x, 0, b₁) = b₂ + b₂ ⇥ b₃ + ───────────────────────────────── + let x : A = a₀ let xs… in b₀ ⇥ b₃ + + + ↑(1, x, 0, a₀) = a₁ + (let xs… in b₀)[x ≔ a₁] = b₁ + ↑(-1, x, 0, b₁) = b₂ + b₂ ⇥ b₃ + ───────────────────────────── + let x = a₀ let xs… in b₀ ⇥ b₃ + + ### Type annotations Simplify a type annotation by removing the annotation: @@ -4136,6 +4259,32 @@ expression would be well-typed. If the `let` expression has a type annotation that doesn't match the type of the right-hand side of the assignment then that is a type error. +A `let` expression with multiple `let` bindings is equivalent to nested `let` +expressions: + + + Γ ⊢ a₀ : A₁ + Γ ⊢ A₀ : i + A₀ ≡ A₁ + a₀ ⇥ a₁ + ↑(1, x, 0, a₁) = a₂ + (let xs… in b₀)[x ≔ a₂] = b₁ + ↑(-1, x, 0, b₁) = b₂ + Γ ⊢ b₂ : B + ───────────────────────────────────── + Γ ⊢ let x : A₀ = a₀ let xs… in b₀ : B + + + Γ ⊢ a₀ : A + a₀ ⇥ a₁ + ↑(1, x, 0, a₁) = a₂ + (let xs… in b₀)[x ≔ a₂] = b₁ + ↑(-1, x, 0, b₁) = b₂ + Γ ⊢ b₂ : B + ──────────────────────────────── + Γ ⊢ let x = a₀ let xs… in b₀ : B + + ### Type annotations The inferred type of a type annotation is the annotation. Type-checking also