diff --git a/dhall-json/examples/travis.dhall b/dhall-json/examples/travis.dhall index 0fedf82..6dd8cdf 100644 --- a/dhall-json/examples/travis.dhall +++ b/dhall-json/examples/travis.dhall @@ -1,53 +1,40 @@ - let OperatingSystem = < Linux : {} | OSX : {} > +let OperatingSystem = < Linux : {} | OSX : {} > -in let Addon = { apt : { packages : List Text, sources : List Text } } +let Addon = { apt : { packages : List Text, sources : List Text } } -in let makeInclude = - λ ( args - : { ghc : - Text - , cabal : - Text - , deploy : - Bool - , os : - OperatingSystem - } - ) - → let release = - if args.deploy then " DEPLOY_GITHUB_RELEASE=TRUE" else "" - - in { env = - "CABALVER=${args.cabal} GHCVER=${args.ghc}${release}" - , compiler = - ": #GHC ${args.ghc}" - , addons = - merge - { Linux = - λ(_ : {}) - → [ { apt = - { packages = - [ "cabal-install-${args.cabal}" - , "ghc-${args.ghc}" - ] - , sources = - [ "hvr-ghc" ] - } - } - ] : Optional Addon - , OSX = - λ(_ : {}) → [] : Optional Addon - } - args.os - , os = - merge - { Linux = - λ(_ : {}) → [] : Optional Text - , OSX = - λ(_ : {}) → [ "osx" ] : Optional Text - } - args.os +let makeInclude = + λ ( args + : { ghc : Text, cabal : Text, deploy : Bool, os : OperatingSystem } + ) + → let release = if args.deploy then " DEPLOY_GITHUB_RELEASE=TRUE" else "" + + in { env = + "CABALVER=${args.cabal} GHCVER=${args.ghc}${release}" + , compiler = + ": #GHC ${args.ghc}" + , addons = + merge + { Linux = + λ(_ : {}) + → Some + { apt = + { packages = + [ "cabal-install-${args.cabal}" + , "ghc-${args.ghc}" + ] + , sources = + [ "hvr-ghc" ] + } + } + , OSX = + λ(_ : {}) → None Addon } + args.os + , os = + merge + { Linux = λ(_ : {}) → None Text, OSX = λ(_ : {}) → Some "osx" } + args.os + } in { language = "c" diff --git a/dhall-json/src/Dhall/JSON.hs b/dhall-json/src/Dhall/JSON.hs index 8035b3d..d99b0bc 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -54,15 +54,15 @@ Dhall @List@s translate to JSON lists: -> $ dhall-to-json <<< '[1, 2, 3] : List Integer' +> $ dhall-to-json <<< '[1, 2, 3] : List Natural' > [1,2,3] Dhall @Optional@ values translate to @null@ if absent and the unwrapped value otherwise: -> $ dhall-to-json <<< '[] : Optional Integer' +> $ dhall-to-json <<< 'None Natural' > null -> $ dhall-to-json <<< '[1] : Optional Integer' +> $ dhall-to-json <<< 'Some 1' > 1 Dhall records translate to JSON records: @@ -75,7 +75,7 @@ > $ dhall-to-json <<< "< Left = +2 | Right : Natural>" > 2 > $ cat config -> [ < Person = { age = +47, name = "John" } +> [ < Person = { age = 47, name = "John" } > | Place : { location : Text } > > > , < Place = { location = "North Pole" } @@ -84,7 +84,7 @@ > , < Place = { location = "Sahara Desert" } > | Person : { age : Natural, name : Text } > > -> , < Person = { age = +35, name = "Alice" } +> , < Person = { age = 35, name = "Alice" } > | Place : { location : Text } > > > ] @@ -105,9 +105,9 @@ contains a record then the name of the alternative is stored inline within the same record. For example, this code: -> let Example = < Left : { foo : Natural } | Right : { bar : Bool } > +> let Example = < Left : { foo : Natural } | Right : { bar : Bool } > > -> in let Nesting = < Inline : {} | Nested : Text > +> let Nesting = < Inline : {} | Nested : Text > > > in { field = "name" > , nesting = Nesting.Inline {=} @@ -124,9 +124,9 @@ If @nesting@ is set to @Nested nestedField@ then the union is store underneath a field named @nestedField@. For example, this code: -> let Example = < Left : { foo : Natural } | Right : { bar : Bool } > +> let Example = < Left : { foo : Natural } | Right : { bar : Bool } > > -> in let Nesting = < Inline : {} | Nested : Text > +> let Nesting = < Inline : {} | Nested : Text > > > in { field = "name" > , nesting = Nesting.Nested "value" diff --git a/dhall-nix/release.nix b/dhall-nix/release.nix index 86a23b0..c7ef991 100644 --- a/dhall-nix/release.nix +++ b/dhall-nix/release.nix @@ -175,13 +175,13 @@ in testOptionalLit = dhallToNix '' λ(b : Bool) → if b - then ([0] : Optional Natural) - else ([] : Optional Natural) + then (Some 0) + else (None Natural) ''; testOptionalFold = dhallToNix '' Optional/fold Natural - ([1] : Optional Natural) + (Some 1) Natural ''; testOptionalBuild = dhallToNix '' diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs index 93b4725..3700679 100644 --- a/dhall-nix/src/Dhall/Nix.hs +++ b/dhall-nix/src/Dhall/Nix.hs @@ -45,10 +45,10 @@ `Optional` values translate to @null@ if missing or the unwrapped value if present: -> $ dhall-to-nix <<< "[] : Optional Integer" +> $ dhall-to-nix <<< "None Natural" > null -> $ dhall-to-nix <<< "[1] : Optional Integer" +> $ dhall-to-nix <<< "Some 1" > 1 Unions are Church-encoded: diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 0f84bd3..faaa54b 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -869,8 +869,6 @@ data TypeMessage s a | MismatchedListElements Int (Expr s a) (Expr s a) (Expr s a) | InvalidListElement Int (Expr s a) (Expr s a) (Expr s a) | InvalidListType (Expr s a) - | InvalidOptionalElement (Expr s a) (Expr s a) (Expr s a) - | InvalidOptionalType (Expr s a) | InvalidSome (Expr s a) (Expr s a) (Expr s a) | InvalidPredicate (Expr s a) (Expr s a) | IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a) @@ -1989,99 +1987,6 @@ prettyTypeMessage (InvalidListElement i expr0 _expr1 expr2) = txt1 = pretty i txt3 = insert expr2 -prettyTypeMessage (InvalidOptionalType expr0) = ErrorMessages {..} - where - short = "Invalid type for ❰Optional❱ element" - - long = - "Explanation: The legacy ❰List❱-like syntax for ❰Optional❱ literals ends with a \n\ - \type annotation for the element that might be present, like this: \n\ - \ \n\ - \ \n\ - \ ┌────────────────────────┐ \n\ - \ │ [1] : Optional Natural │ An optional element that's present \n\ - \ └────────────────────────┘ \n\ - \ ⇧ \n\ - \ The type of the ❰Optional❱ element, which is an ❰Natural❱ \n\ - \ number \n\ - \ \n\ - \ \n\ - \ ┌────────────────────────┐ \n\ - \ │ [] : Optional Natural │ An optional element that's absent \n\ - \ └────────────────────────┘ \n\ - \ ⇧ \n\ - \ You still specify the type even when the element is absent \n\ - \ \n\ - \ \n\ - \The element type must be a type and not something else. For example, the \n\ - \following element types are " <> _NOT <> " valid: \n\ - \ \n\ - \ \n\ - \ ┌──────────────────┐ \n\ - \ │ ... : Optional 1 │ \n\ - \ └──────────────────┘ \n\ - \ ⇧ \n\ - \ This is a ❰Natural❱ number and not a ❰Type❱ \n\ - \ \n\ - \ \n\ - \ ┌─────────────────────┐ \n\ - \ │ ... : Optional Type │ \n\ - \ └─────────────────────┘ \n\ - \ ⇧ \n\ - \ This is a ❰Kind❱ and not a ❰Type❱ \n\ - \ \n\ - \ \n\ - \Even if the element is absent you still must specify a valid type \n\ - \ \n\ - \You declared that the ❰Optional❱ element should have type: \n\ - \ \n\ - \" <> txt0 <> "\n\ - \ \n\ - \... which is not a ❰Type❱ \n" - where - txt0 = insert expr0 - -prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..} - where - short = "❰Optional❱ element has the wrong type\n" - <> "\n" - <> Dhall.Diff.diffNormalized expr0 expr2 - - long = - "Explanation: An ❰Optional❱ element must have a type matching the type annotation\n\ - \ \n\ - \For example, this is a valid ❰Optional❱ value: \n\ - \ \n\ - \ \n\ - \ ┌────────────────────────┐ \n\ - \ │ [1] : Optional Natural │ ❰1❱ is a ❰Natural❱ number, which matches the \n\ - \ └────────────────────────┘ number \n\ - \ \n\ - \ \n\ - \... but this is " <> _NOT <> " a valid ❰Optional❱ value: \n\ - \ \n\ - \ \n\ - \ ┌────────────────────────────┐ \n\ - \ │ [\"ABC\"] : Optional Natural │ ❰\"ABC\"❱ is not a ❰Natural❱ number \n\ - \ └────────────────────────────┘ \n\ - \ \n\ - \ \n\ - \Your ❰Optional❱ element should have this type: \n\ - \ \n\ - \" <> txt0 <> "\n\ - \ \n\ - \... but the element you provided: \n\ - \ \n\ - \" <> txt1 <> "\n\ - \ \n\ - \... has this type instead: \n\ - \ \n\ - \" <> txt2 <> "\n" - where - txt0 = insert expr0 - txt1 = insert expr1 - txt2 = insert expr2 - prettyTypeMessage (InvalidSome expr0 expr1 expr2) = ErrorMessages {..} where short = "❰Some❱ argument has the wrong type" diff --git a/dhall/tests/format/unicodeA.dhall b/dhall/tests/format/unicodeA.dhall index 620e531..1b8e033 100644 --- a/dhall/tests/format/unicodeA.dhall +++ b/dhall/tests/format/unicodeA.dhall @@ -1,15 +1,15 @@ λ(isActive : Bool) → { barLeftEnd = - [ "┨" ] : Optional Text + Some "┨" , barRightEnd = - [ "┠" ] : Optional Text + Some "┠" , separator = - [ "┃" ] : Optional Text + Some "┃" , alignment = < ToTheLeft = {=} | ToTheRight : {} | Centered : {} > : ./Alignment.dhall , barWidth = - [] : Optional Natural + None Natural , barSegments = [ "index", "command", "path", "title" ] } diff --git a/dhall/tests/format/unicodeB.dhall b/dhall/tests/format/unicodeB.dhall index 41fc110..80a45be 100644 --- a/dhall/tests/format/unicodeB.dhall +++ b/dhall/tests/format/unicodeB.dhall @@ -1,15 +1,15 @@ λ(isActive : Bool) → { barLeftEnd = - [ "┨" ] : Optional Text + Some "┨" , barRightEnd = - [ "┠" ] : Optional Text + Some "┠" , separator = - [ "┃" ] : Optional Text + Some "┃" , alignment = < ToTheLeft = {=} | ToTheRight : {} | Centered : {} > : ./Alignment.dhall , barWidth = - [] : Optional Natural + None Natural , barSegments = [ "index", "command", "path", "title" ] }