All notable changes to the Dhall language standard will be documented in this file.
For more info about our versioning policy, see versioning.md.
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.