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:

• 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

  • Normalize the inferred type of a ∧-expression

  • Generalize empty record projections

  • Clarify type inference for record literals

  • Fix type-inference rules for merge

  • Specify binary encoding of -0.0

  • Specify how to encoded union constructors

• Fixes and improvements to the standard test suite:

  • Merge typecheck and type-inference tests
  • Add failure test for toMap of record of kind Kind
  • 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

• Fixes and improvements to the Prelude:

  • Small improvements for Prelude.Natural