Skip to content

Latest commit

 

History

History
900 lines (554 loc) · 28.1 KB

shift.md

File metadata and controls

900 lines (554 loc) · 28.1 KB

Shift

-- | Haskell implementation of shifting
module Shift
    ( -- * Shift
      shift
    ) where

import Syntax (Expression(..), Natural, Text, TextLiteral(..))

Dhall uses a shift function internally to avoid variable capture in the implementation of De Bruijn indices. This function increases or decreases the indices of free variables within an expression.

This shift function has the form:

↑(d, x, m, e₀) = e₁

... where:

  • d (an input integer) is the amount to add to the variable indices
    • d is always -1 or 1
  • x (an input variable name) is the name of the free variable(s) to shift
    • variables with a different name are unaffected by the shift function
  • m (an input natural number) is the minimum index to shift
    • m always starts out at 0
    • m increases by one when descending past a bound variable named x
    • variables with an index lower than m are unaffected by the shift function
  • e₀ (an input expression) is the expression to shift
  • e₁ (the output expression) is the shifted expression
-- | Haskell implementation of the shift function
shift
    :: Integer    -- ^ @d@, the amount to add to the variable indices
    -> Text       -- ^ @x@, the name of the free variable to shift
    -> Natural    -- ^ @m@, the minimum index to shift
    -> Expression -- ^ @e₀@, the expression to shift
    -> Expression -- ^ @e₁@, the shifted expression

Table of contents

Variables

The first rule is that the shift function will increase the index of any variable if the variable name matches and the variable's index is greater than or equal to the minimum index to shift. For example:

↑(1, x, 0, x) = x@1   ; `x = x@0` and increasing the index by 1 gives `x@1`

↑(1, x, 1, x) = x     ; No shift, because the index was below the cutoff

↑(1, x, 0, y) = y     ; No shift, because the variable name did not match

↑(-1, x, 0, x@1) = x  ; Example of negative shift

Formally, shift the variable if the name matches and the index is at least as large as the lower bound:

───────────────────────────  ; m <= n
↑(d, x, m, x@n) = x@(n + d)

shift d x m (Variable x' n) | x == x' && m <= n =
    Variable x' (n + fromInteger d)

Don't shift the index if the index falls short of the lower bound:

─────────────────────  ; m > n
↑(d, x, m, x@n) = x@n

shift _d x _m (Variable x' n) | x == x' = Variable x' n

Also, don't shift the index if the variable name does not match:

─────────────────────  ; x ≠ y
↑(d, x, m, y@n) = y@n

shift _d _x _m (Variable y n) = Variable y n

Bound variables

The shift function is designed to shift only free variables when m = 0. For example, the following shift usage has no effect because m = 0 and the expression is "closed" (i.e. no free variables):

↑(1, x, 0, λ(x : Type) → x) = λ(x : Type) → x

↑(1, x, 0, ∀(x : Type) → x) = ∀(x : Type) → x

↑(1, x, 0, let x = 1 in x) = let x = 1 in x

... whereas the following shift usage has an effect on expressions with free variables:

↑(1, x, 0, λ(y : Type) → x) = λ(y : Type) → x@1

↑(1, x, 0, ∀(y : Type) → x) = ∀(y : Type) → x@1

↑(1, x, 0, let y = 1 in x) = let y = 1 in x@1

Increment the minimum bound when descending into a λ-expression that binds a variable of the same name in order to avoid shifting the bound variable:

↑(d, x, m, A₀) = A₁   ↑(d, x, m + 1, b₀) = b₁
─────────────────────────────────────────────
↑(d, x, m, λ(x : A₀) → b₀) = λ(x : A₁) → b₁

shift d x m (Lambda x' _A₀ b₀) | x == x' = Lambda x' _A₁ b₁
  where
    _A₁ = shift d x m _A₀

    b₁ = shift d x (m + 1) b₀

Note that 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.

Descend as normal if the bound variable name does not match:

↑(d, x, m, A₀) = A₁   ↑(d, x, m, b₀) = b₁
───────────────────────────────────────────  ; x ≠ y
↑(d, x, m, λ(y : A₀) → b₀) = λ(y : A₁) → b₁

shift d x m (Lambda y _A₀ b₀) = Lambda y _A₁ b₁
  where
    _A₁ = shift d x m _A₀

    b₁ = shift d x m b₀

Function types also introduce bound variables, so increase the minimum bound when descending past such a bound variable:

↑(d, x, m, A₀) = A₁   ↑(d, x, m + 1, B₀) = B₁
─────────────────────────────────────────────
↑(d, x, m, ∀(x : A₀) → B₀) = ∀(x : A₁) → B₁

shift d x m (Forall x' _A₀ _B₀) | x == x' = Forall x' _A₁ _B₁
  where
    _A₁ = shift d x m _A₀

    _B₁ = shift d x (m + 1) _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.

Descend as normal if the bound variable name does not match:

↑(d, x, m, A₀) = A₁   ↑(d, x, m, B₀) = B₁
───────────────────────────────────────────  ; x ≠ y
↑(d, x, m, ∀(y : A₀) → B₀) = ∀(y : A₁) → B₁

shift d x m (Forall y _A₀ _B₀) = Forall y _A₁ _B₁
  where
    _A₁ = shift d x m _A₀

    _B₁ = shift d x m _B₀

let expressions also introduce bound variables, so increase the minimum bound 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, 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, let x = a₀ in b₀) = let x = a₁ in b₁

shift d x m (Let x' (Just _A₀) a₀ b₀) | x == x' = Let x' (Just _A₁) a₁ b₁
  where
    _A₁ = shift d x m _A₀

    a₁ = shift d x m a₀

    b₁ = shift d x (m + 1) b₀

shift d x m (Let x' Nothing a₀ b₀) | x == x' = Let x' Nothing a₁ b₁
  where
    a₁ = shift d x m a₀

    b₁ = shift d x (m + 1) 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.

Note that Dhall's let expressions do not allow recursive definitions so the bound variable, x, is not in scope for the right-hand side of the assignment, a₀, so do not increase the lower bound, m, when shifting the right-hand side 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, let y : A₀ = a₀ in b₀) = let y : A₁ = a₁ in 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₁

shift d x m (Let y (Just _A₀) a₀ b₀) = Let y (Just _A₁) a₁ b₁
  where
    _A₁ = shift d x m _A₀

    a₁ = shift d x m a₀

    b₁ = shift d x m b₀

shift d x m (Let y Nothing a₀ b₀) = Let y Nothing a₁ b₁
  where
    a₁ = shift d x m a₀

    b₁ = shift d x m b₀

Imports

You can shift expressions with unresolved imports because the language enforces that imported values must be closed (i.e. no free variables) and shifting a closed expression has no effect:

─────────────────────────────────
↑(d, x, m, path file) = path file


─────────────────────────────────────
↑(d, x, m, . path file) = . path file


───────────────────────────────────────
↑(d, x, m, .. path file) = .. path file


─────────────────────────────────────
↑(d, x, m, ~ path file) = ~ path file


─────────────────────────────────────────────────────────────────────
↑(d, x, m, https://authority path file) = https://authority path file


─────────────────────────
↑(d, x, m, env:x) = env:x

shift _d _x _m (Import importType importMode maybeDigest) =
    Import importType importMode maybeDigest

Other

No other Dhall expressions bind variables, so the shift function descends into sub-expressions in those cases, like this:

↑(1, x, 0, List x) = List x@1

The remaining rules are:

↑(d, x, m, t₀) = t₁   ↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
───────────────────────────────────────────────────────────────
↑(d, x, m, if t₀ then l₀ else r₀) = if t₁ then l₁ else r₁

shift d x m (If t₀ l₀ r₀) = If t₁ l₁ r₁
  where
    t₁ = shift d x m t₀

    l₁ = shift d x m l₀

    r₁ = shift d x m r₀
↑(d, x, m, t₀) = t₁   ↑(d, x, m, u₀) = u₁   ↑(d, x, m, T₀) = T₁
───────────────────────────────────────────────────────────────
↑(d, x, m, merge t₀ u₀ : T₀) = merge t₁ u₁ : T₁


↑(d, x, m, t₀) = t₁   ↑(d, x, m, u₀) = u₁
─────────────────────────────────────────
↑(d, x, m, merge t₀ u₀) = merge t₁ u₁

shift d x m (Merge t₀ u₀ (Just _T₀)) = Merge t₁ u₁ (Just _T₁)
  where
    t₁ = shift d x m t₀

    u₁ = shift d x m u₀

    _T₁ = shift d x m _T₀

shift d x m (Merge t₀ u₀ Nothing) = Merge t₁ u₁ Nothing
  where
    t₁ = shift d x m t₀

    u₁ = shift d x m u₀
↑(d, x, m, t₀) = t₁   ↑(d, x, m, T₀) = T₁
─────────────────────────────────────────
↑(d, x, m, toMap t₀ : T₀) = toMap t₁ : T₁


↑(d, x, m, t₀) = t₁
───────────────────────────────
↑(d, x, m, toMap t₀) = toMap t₁

shift d x m (ToMap t₀ (Just _T₀)) = ToMap t₁ (Just _T₁)
  where
    t₁ = shift d x m t₀

    _T₁ = shift d x m _T₀

shift d x m (ToMap t₀ Nothing) = ToMap t₁ Nothing
  where
    t₁ = shift d x m t₀
↑(d, x, m, t₀) = t₁
───────────────────────────────
↑(d, x, m, showConstructor t₀) = showConstructor t₁

shift d x m (ShowConstructor t₀) = ShowConstructor t₁
  where
    t₁ = shift d x m t₀
↑(d, x, m, T₀) = T₁
─────────────────────────────
↑(d, x, m, [] : T₀) = [] : T₁


↑(d, x, m, t₀) = t₁   ↑(d, x, m, [ ts₀… ]) = [ ts₁… ]
─────────────────────────────────────────────────────
↑(d, x, m, [ t₀, ts₀… ]) = [ t₁, ts₁… ]

shift d x m (EmptyList _T₀) = EmptyList _T₁
  where
    _T₁ = shift d x m _T₀

shift d x m (NonEmptyList ts₀) = NonEmptyList ts₁
  where
    ts₁ = fmap (shift d x m) ts₀
↑(d, x, m, t₀) = t₁   ↑(d, x, m, T₀) = T₁
─────────────────────────────────────────
↑(d, x, m, t₀ : T₀) = t₁ : T₁

shift d x m (Annotation t₀ _T₀) = Annotation t₁ _T₁
  where
    t₁ = shift d x m t₀

    _T₁ = shift d x m _T₀
↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ || r₀) = l₁ || r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ + r₀) = l₁ + r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ ++ r₀) = l₁ ++ r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ # r₀) = l₁ # r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ && r₀) = l₁ && r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ ∧ r₀) = l₁ ∧ r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ ⫽ r₀) = l₁ ⫽ r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ ⩓ r₀) = l₁ ⩓ r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ * r₀) = l₁ * r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ == r₀) = l₁ == r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ != r₀) = l₁ != r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ ? r₀) = l₁ ? r₁


↑(d, x, m, l₀) = l₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, l₀ === r₀) = l₁ === r₁

shift d x m (Operator l₀ op r₀) = Operator l₁ op r₁
  where
    l₁ = shift d x m l₀

    r₁ = shift d x m r₀
↑(d, x, m, f₀) = f₁   ↑(d, x, m, a₀) = a₁
─────────────────────────────────────────
↑(d, x, m, f₀ a₀) = f₁ a₁

shift d x m (Application f₀ a₀) = Application f₁ a₁
  where
    f₁ = shift d x m f₀

    a₁ = shift d x m a₀
↑(d, x, m, t₀) = t₁
───────────────────────
↑(d, x, m, t₀.y) = t₁.y

shift d x m (Field t₀ y) = Field t₁ y
  where
    t₁ = shift d x m t₀
↑(d, x, m, t₀) = t₁
───────────────────────────────────
↑(d, x, m, t₀.{ xs… }) = t₁.{ xs… }

shift d x m (ProjectByLabels t₀ xs) = ProjectByLabels t₁ xs
  where
    t₁ = shift d x m t₀
↑(d, x, m, t₀) = t₁ ↑(d, x, m, T₀) = T₁
───────────────────────────────────────
↑(d, x, m, t₀.(T₀) = t₁.(T₁)

shift d x m (ProjectByType t₀ _T₀) = ProjectByType t₁ _T₁
  where
    t₁ = shift d x m t₀

    _T₁ = shift d x m _T₀
↑(d, x, m, T₀) = T₁   ↑(d, x, m, r₀) = r₁
─────────────────────────────────────────
↑(d, x, m, T₀::r₀) = T₁::r₁

shift d x m (Completion _T₀ r₀) = Completion _T₁ r₁
  where
    _T₁ = shift d x m _T₀

    r₁ = shift d x m r₀
↑(d, x, m, T₀) = T₁
─────────────────────────────────────
↑(d, x, m, assert : T₀) = assert : T₁

shift d x m (Assert _T₀) = Assert _T₁
  where
    _T₁ = shift d x m _T₀
↑(d, x, m, e₀) = e₁   ↑(d, x, m, v₀) = v₁
───────────────────────────────────────────────────
↑(d, x, m, e₀ with k.ks… = v₀) = e₁ with k.ks… = v₁

shift d x m (With e₀ ks v₀) = With e₁ ks v₁
  where
    e₁ = shift d x m e₀

    v₁ = shift d x m v₀
─────────────────────
↑(d, x, m, n.n) = n.n

shift _d _x _m (DoubleLiteral n) = DoubleLiteral n
─────────────────
↑(d, x, m, n) = n

shift _d _x _m (NaturalLiteral n) = NaturalLiteral n
───────────────────
↑(d, x, m, ±n) = ±n

shift _d _x _m (IntegerLiteral n) = IntegerLiteral n
───────────────────────────────────
↑(d, x, m, YYYY-MM-DD) = YYYY-MM-DD

shift _d _x _m (DateLiteral d) = DateLiteral d
───────────────────────────────
↑(d, x, m, hh:mm:ss) = hh:mm:ss

shift _d _x _m (TimeLiteral t p) = TimeLiteral t p
───────────────────────────
↑(d, x, m, ±HH:MM) = ±HH:MM

shift _d _x _m (TimeZoneLiteral z) = TimeZoneLiteral z
─────────────────────
↑(d, x, m, "s") = "s"


↑(d, x, m, t₀) = t₁   ↑(d, x, m, "ss₀…") = "ss₁…"
─────────────────────────────────────────────────
↑(d, x, m, "s₀${t₀}ss₀…") = "s₀${t₁}ss₁…"

shift d x m (TextLiteral (Chunks xys₀ z)) = TextLiteral (Chunks xys₁ z)
  where
    xys₁ = fmap adapt xys₀

    adapt (s, t₀) = (s, t₁)
      where
        t₁ = shift d x m t₀
───────────────────
↑(d, x, m, {}) = {}


↑(d, x, m, T₀) = T₁   ↑(d, k, m, { ks₀… }) = { ks₁… }
─────────────────────────────────────────────────────
↑(d, x, m, { k : T₀, xs₀… }) = { k : T₁, ks₁… }

shift d x m (RecordType ks₀) = RecordType ks₁
  where
    ks₁ = map adapt ks₀

    adapt (k, _T₀) = (k, _T₁)
      where
        _T₁ = shift d x m _T₀
─────────────────────
↑(d, x, m, {=}) = {=}


↑(d, x, m, t₀) = t₁   ↑(d, x, m, { ks₀… }) = { ks₁… }
─────────────────────────────────────────────────────
↑(d, x, m, { k = t₀, ks₀… }) = { k = t₁, ks₁… }

shift d x m (RecordLiteral ks₀) = RecordLiteral ks₁
  where
    ks₁ = map adapt ks₀

    adapt (k, t₀) = (k, t₁)
      where
        t₁ = shift d x m t₀
───────────────────
↑(d, x, m, <>) = <>


↑(d, x, m, T₀) = T₁   ↑(d, x, m, < ks₀… >) = < ks₁… >
─────────────────────────────────────────────────────
↑(d, x, m, < k : T₀ | ks₀… >) = < k : T₁ | ks₁… >


↑(d, x, m, < ks₀… >) = < ks₁… >
─────────────────────────────────────────
↑(d, x, m, < k | ks₀… >) = < k | ks₁… >

shift d x m (UnionType ks₀) = UnionType ks₁
  where
    ks₁ = map adapt ks₀

    adapt (k, Just _T₀) = (k, Just _T₁)
      where
        _T₁ = shift d x m _T₀
    adapt (k, Nothing) = (k, Nothing)
↑(d, x, m, a₀) = a₁
─────────────────────────────
↑(d, x, m, Some a₀) = Some a₁

shift d x m (Some a₀) = Some a₁
  where
    a₁ = shift d x m a₀
───────────────────────
↑(d, x, m, None) = None


─────────────────────────────────────────
↑(d, x, m, Natural/build) = Natural/build


───────────────────────────────────────
↑(d, x, m, Natural/fold) = Natural/fold


───────────────────────────────────────────
↑(d, x, m, Natural/isZero) = Natural/isZero


───────────────────────────────────────
↑(d, x, m, Natural/even) = Natural/even


─────────────────────────────────────
↑(d, x, m, Natural/odd) = Natural/odd


─────────────────────────────────────────────────
↑(d, x, m, Natural/toInteger) = Natural/toInteger


───────────────────────────────────────────────
↑(d, x, m, Natural/subtract) = Natural/subtract


───────────────────────────────────────
↑(d, x, m, Natural/show) = Natural/show


───────────────────────────────────────────────
↑(d, x, m, Integer/toDouble) = Integer/toDouble


───────────────────────────────────────
↑(d, x, m, Integer/show) = Integer/show


───────────────────────────────────────────
↑(d, x, m, Integer/negate) = Integer/negate


─────────────────────────────────────────
↑(d, x, m, Integer/clamp) = Integer/clamp


─────────────────────────────────────
↑(d, x, m, Double/show) = Double/show


───────────────────────────────────
↑(d, x, m, List/build) = List/build


─────────────────────────────────
↑(d, x, m, List/fold) = List/fold


─────────────────────────────────────
↑(d, x, m, List/length) = List/length


─────────────────────────────────
↑(d, x, m, List/head) = List/head


─────────────────────────────────
↑(d, x, m, List/last) = List/last


───────────────────────────────────────
↑(d, x, m, List/indexed) = List/indexed


───────────────────────────────────────
↑(d, x, m, List/reverse) = List/reverse


─────────────────────────────────
↑(d, x, m, Text/show) = Text/show


───────────────────────────────────────
↑(d, x, m, Text/replace) = Text/replace


───────────────────────
↑(d, x, m, Bool) = Bool


───────────────────────────────
↑(d, x, m, Optional) = Optional


─────────────────────────────
↑(d, x, m, Natural) = Natural


─────────────────────────────
↑(d, x, m, Integer) = Integer


───────────────────────────
↑(d, x, m, Double) = Double


───────────────────────
↑(d, x, m, Text) = Text


───────────────────────
↑(d, x, m, List) = List


───────────────────────
↑(d, x, m, Date) = Date


───────────────────────
↑(d, x, m, Time) = Date


───────────────────────────────
↑(d, x, m, TimeZone) = TimeZone


───────────────────────
↑(d, x, m, True) = True


─────────────────────────
↑(d, x, m, False) = False

shift _d _x _m (Builtin b) = Builtin b
───────────────────────
↑(d, x, m, Type) = Type


───────────────────────
↑(d, x, m, Kind) = Kind


───────────────────────
↑(d, x, m, Sort) = Sort

shift _d _x _m (Constant c) = Constant c