Skip to content

v10.0.0
Compare
Choose a tag to compare
@Gabriella439 Gabriella439 released this 06 Sep 04:05
· 366 commits to master since this release
v10.0.0
ecbf827
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

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 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:

Assets 2
Loading