Add constructors keyword (#199)

Fixes #163

This provides a new `constructors` keyword which can be used to create a
record of constructors from a union type literal.  The record contains
one constructor per alternative in the union type.

dhall.cabal

@@ -83,6 +83,7 @@ Extra-Source-Files:
     Prelude/Text/concatSep
     tests/parser/*.dhall
     tests/regression/*.dhall
+    tests/tutorial/*.dhall
 
 Source-Repository head
     Type: git

src/Dhall/Core.hs

@@ -325,6 +325,8 @@ data Expr s a
     -- | > Merge x y (Just t )                      ~  merge x y : t
     -- | > Merge x y  Nothing                       ~  merge x y
     | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))
+    -- | > Constructors e                           ~  constructors e
+    | Constructors (Expr s a)
     -- | > Field e x                                ~  e.x
     | Field (Expr s a) Text
     -- | > Note s x                                 ~  e
@@ -396,6 +398,7 @@ instance Monad (Expr s) where
     Combine a b      >>= k = Combine (a >>= k) (b >>= k)
     Prefer a b       >>= k = Prefer (a >>= k) (b >>= k)
     Merge a b c      >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)
+    Constructors a   >>= k = Constructors (a >>= k)
     Field a b        >>= k = Field (a >>= k) b
     Note a b         >>= k = Note a (b >>= k)
     Embed a          >>= k = k a
@@ -456,6 +459,7 @@ instance Bifunctor Expr where
     first k (Combine a b     ) = Combine (first k a) (first k b)
     first k (Prefer a b      ) = Prefer (first k a) (first k b)
     first k (Merge a b c     ) = Merge (first k a) (first k b) (fmap (first k) c)
+    first k (Constructors a  ) = Constructors (first k a)
     first k (Field a b       ) = Field (first k a) b
     first k (Note a b        ) = Note (k a) (first k b)
     first _ (Embed a         ) = Embed a
@@ -900,9 +904,10 @@ prettyExprD :: Pretty a => Expr s a -> Doc ann
 prettyExprD a0@(App _ _) =
     enclose' "" "" " " "" (fmap duplicate (reverse (docs a0)))
   where
-    docs (App  a b) = prettyExprE b : docs a
-    docs (Note _ b) = docs b
-    docs         b  = [ prettyExprE b ]
+    docs (App        a b) = prettyExprE b : docs a
+    docs (Constructors b) = [ prettyExprE b , "constructors" ]
+    docs (Note       _ b) = docs b
+    docs               b  = [ prettyExprE b ]
 prettyExprD (Note _ b) = prettyExprD b
 prettyExprD a0 =
     prettyExprE a0
@@ -1239,9 +1244,10 @@ buildExprC9  a           = buildExprD  a
 
 -- | Builder corresponding to the @exprD@ parser in "Dhall.Parser"
 buildExprD :: Buildable a => Expr s a -> Builder
-buildExprD (App  a b) = buildExprD a <> " " <> buildExprE b
-buildExprD (Note _ b) = buildExprD b
-buildExprD  a         = buildExprE a
+buildExprD (App        a b) = buildExprD a <> " " <> buildExprE b
+buildExprD (Constructors b) = "constructors " <> buildExprE b
+buildExprD (Note       _ b) = buildExprD b
+buildExprD  a               = buildExprE a
 
 -- | Builder corresponding to the @exprE@ parser in "Dhall.Parser"
 buildExprE :: Buildable a => Expr s a -> Builder
@@ -1625,6 +1631,9 @@ shift d v (Merge a b c) = Merge a' b' c'
     a' =       shift d v  a
     b' =       shift d v  b
     c' = fmap (shift d v) c
+shift d v (Constructors a) = Constructors a'
+  where
+    a' = shift d v  a
 shift d v (Field a b) = Field a' b
   where
     a' = shift d v a
@@ -1760,6 +1769,9 @@ subst x e (Merge a b c) = Merge a' b' c'
     a' =       subst x e  a
     b' =       subst x e  b
     c' = fmap (subst x e) c
+subst x e (Constructors a) = Constructors a'
+  where
+    a' = subst x e  a
 subst x e (Field a b) = Field a' b
   where
     a' = subst x e a
@@ -2151,6 +2163,18 @@ normalizeWith ctx e0 = loop (shift 0 "_" e0)
         x' =      loop x
         y' =      loop y
         t' = fmap loop t
+    Constructors t   ->
+        case t' of
+            Union kts -> RecordLit kvs
+              where
+                kvs = Data.Map.mapWithKey adapt kts
+
+                adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest)
+                  where
+                    rest = Data.Map.delete k kts
+            _ -> Constructors t'
+      where
+        t' = loop t
     Field r x        ->
         case loop r of
             RecordLit kvs ->
@@ -2361,6 +2385,10 @@ isNormalized e = case shift 0 "_" e of  -- `shift` is a hack to delete `Note`
                             Nothing -> True
                     _ -> True
             _ -> True
+    Constructors t -> isNormalized t &&
+        case t of
+            Union _ -> False
+            _       -> True
     Field r x -> isNormalized r &&
         case r of
             RecordLit kvs ->

src/Dhall/Parser.hs

@@ -511,6 +511,9 @@ _using = reserved "using"
 _merge :: Parser ()
 _merge = reserved "merge"
 
+_constructors :: Parser ()
+_constructors = reserved "constructors"
+
 _NaturalFold :: Parser ()
 _NaturalFold = reserved "Natural/fold"
 
@@ -1151,8 +1154,10 @@ notEqualExpression =
 
 applicationExpression :: Parser a -> Parser (Expr Src a)
 applicationExpression embedded = do
-    a <- some (noted (selectorExpression embedded))
-    return (foldl1 app a)
+    f <- (do _constructors; return Constructors) <|> return id
+    a <- noted (selectorExpression embedded)
+    b <- many (noted (selectorExpression embedded))
+    return (foldl app (f a) b)
   where
     app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) =
         Note (Src before after (bytesL <> bytesR)) (App nL nR)

src/Dhall/Tutorial.hs

@@ -1128,6 +1128,36 @@ import Dhall
 -- >     ,   Empty
 -- >     ]
 --
+-- ... and Dhall even provides the @constructors@ keyword to automate this
+-- common pattern:
+--
+-- >     let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } >
+-- > in  [   MyType.Empty {}
+-- >     ,   MyType.Person { name = "John", age = +23 }
+-- >     ,   MyType.Person { name = "Amy" , age = +25 }
+-- >     ]
+--
+-- The @constructors@ keyword takes a union type argument and returns a record
+-- with one field per union type constructor:
+--
+-- > $ dhall --pretty
+-- > constructors < Empty : {} | Person : { name : Text, age : Natural } >
+-- > <Ctrl-D>
+-- >
+-- > { Empty  :
+-- >     ∀(Empty : {}) → < Empty : {} | Person : { age : Natural, name : Text } >
+-- > , Person :
+-- >       ∀(Person : { age : Natural, name : Text })
+-- >     → < Empty : {} | Person : { age : Natural, name : Text } >
+-- > }
+-- >
+-- > { Empty  =
+-- >     λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } >
+-- > , Person =
+-- >       λ(Person : { age : Natural, name : Text })
+-- >     → < Person = Person | Empty : {} >
+-- > }
+--
 -- You can also extract fields during pattern matching such as in the following
 -- function which renders each value to `Text`:
 --

src/Dhall/TypeCheck.hs

@@ -637,6 +637,16 @@ typeWithA tpa = loop
                             _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))
         mapM_ process (Data.Map.toList ktsY)
         return t
+    loop ctx e@(Constructors t  ) = do
+        _ <- loop ctx t
+
+        kts <- case Dhall.Core.normalize t of
+            Union kts -> return kts
+            t'        -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t'))
+
+        let adapt k t_ = Pi k t_ (Union kts)
+
+        return (Record (Data.Map.mapWithKey adapt kts))
     loop ctx e@(Field r x       ) = do
         t <- fmap Dhall.Core.normalize (loop ctx r)
         case t of
@@ -711,6 +721,7 @@ data TypeMessage s a
     | InvalidHandlerOutputType Text (Expr s a) (Expr s a)
     | MissingMergeType
     | HandlerNotAFunction Text (Expr s a)
+    | ConstructorsRequiresAUnionType (Expr s a) (Expr s a)
     | NotARecord Text (Expr s a) (Expr s a)
     | MissingField Text (Expr s a)
     | CantAnd (Expr s a) (Expr s a)
@@ -2751,6 +2762,58 @@ prettyTypeMessage (HandlerNotAFunction k expr0) = ErrorMessages {..}
         txt0 = build k
         txt1 = build expr0
 
+prettyTypeMessage (ConstructorsRequiresAUnionType expr0 expr1) = ErrorMessages {..}
+  where
+    short = "❰constructors❱ requires a union type"
+
+    long =
+        "Explanation: You can only use the ❰constructors❱ keyword on an argument that is \n\
+        \a union type literal, like this:                                                \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌───────────────────────────────────────────────┐                           \n\
+        \    │ constructors < Left : Natural, Right : Bool > │                           \n\
+        \    └───────────────────────────────────────────────┘                           \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \... but you cannot use the ❰constructors❱ keyword on any other type of argument.\n\
+        \For example, you cannot use a variable argument:                                \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌──────────────────────────────┐                                            \n\
+        \    │ λ(t : Type) → constructors t │  Invalid: ❰t❱ might not be a union type    \n\
+        \    └──────────────────────────────┘                                            \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌─────────────────────────────────────────────────┐                         \n\
+        \    │ let t : Type = < Left : Natural, Right : Bool > │  Invalid: Type-checking \n\
+        \    │ in  constructors t                              │  precedes normalization \n\
+        \    └─────────────────────────────────────────────────┘                         \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \However, you can import the union type argument:                                \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌────────────────────────────────┐                                          \n\
+        \    │ constructors ./unionType.dhall │ Valid: Import resolution precedes        \n\
+        \    └────────────────────────────────┘ type-checking                            \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \────────────────────────────────────────────────────────────────────────────────\n\
+        \                                                                                \n\
+        \You tried to supply the following argument:                                     \n\
+        \                                                                                \n\
+        \↳ " <> txt0 <> "                                                                \n\
+        \                                                                                \n\
+        \... which normalized to:                                                        \n\
+        \                                                                                \n\
+        \↳ " <> txt1 <> "                                                                \n\
+        \                                                                                \n\
+        \... which is not a union type literal                                           \n"
+      where
+        txt0 = build expr0
+        txt1 = build expr1
+
 prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..}
   where
     short = "Not a record"

tests/Parser.hs

@@ -107,6 +107,9 @@ parserTests =
             , shouldPass
                 "merge"
                 "./tests/parser/merge.dhall"
+            , shouldPass
+                "constructors"
+                "./tests/parser/constructors.dhall"
             , shouldPass
                 "fields"
                 "./tests/parser/fields.dhall"

tests/Tutorial.hs

@@ -10,8 +10,11 @@ import qualified Test.Tasty
 import qualified Test.Tasty.HUnit
 import qualified Util
 
+import Data.Monoid ((<>))
+import Data.Text (Text)
 import Dhall (Inject)
 import GHC.Generics (Generic)
+import Numeric.Natural (Natural)
 import Test.Tasty (TestTree)
 import Test.Tasty.HUnit ((@?=))
 
@@ -27,6 +30,13 @@ tutorialTests =
             , _Functions_1
             , _Functions_2
             ]
+        , Test.Tasty.testGroup "Unions"
+            [ example 0 "./tests/tutorial/unions0A.dhall" "./tests/tutorial/unions0B.dhall"
+            , example 1 "./tests/tutorial/unions1A.dhall" "./tests/tutorial/unions1B.dhall"
+            , example 2 "./tests/tutorial/unions2A.dhall" "./tests/tutorial/unions2B.dhall"
+            , example 3 "./tests/tutorial/unions3A.dhall" "./tests/tutorial/unions3B.dhall"
+            , example 4 "./tests/tutorial/unions4A.dhall" "./tests/tutorial/unions4B.dhall"
+            ]
         ]
 
 _Interpolation_0 :: TestTree
@@ -67,3 +77,9 @@ _Functions_2 = Test.Tasty.HUnit.testCase "Example #2" (do
     f <- Dhall.input Dhall.auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar"
     f (Example0 { foo = True, bar = False }) @?= False
     f (Example0 { foo = True, bar = True  }) @?= True )
+
+example :: Natural -> Text -> Text -> TestTree
+example n text0 text1 =
+    Test.Tasty.HUnit.testCase
+        ("Example #" <> show n)
+        (Util.equivalent text0 text1)

tests/Util.hs

@@ -3,6 +3,7 @@
 module Util
     ( code
     , codeWith
+    , equivalent
     , normalize'
     , normalizeWith'
     , assertNormalizesTo
@@ -48,6 +49,12 @@ codeWith ctx strictText = do
         Right _        -> return ()
     return expr1
 
+equivalent :: Data.Text.Text -> Data.Text.Text -> IO ()
+equivalent text0 text1 = do
+    expr0 <- fmap Dhall.Core.normalize (Util.code text0) :: IO (Expr X X)
+    expr1 <- fmap Dhall.Core.normalize (Util.code text1) :: IO (Expr X X)
+    assertEqual "Expressions are not equivalent" expr0 expr1
+
 assertNormalizesTo :: Expr Src X -> Data.Text.Lazy.Text -> IO ()
 assertNormalizesTo e expected = do 
   assertBool msg (not $ Dhall.Core.isNormalized e)

tests/parser/constructors.dhall

@@ -0,0 +1 @@
+constructors < Left : Natural | Right : Bool >

tests/tutorial/process

@@ -0,0 +1,6 @@
+    λ(union : < Left : Natural | Right : Bool >)
+→   let handlers =
+            { Left  = Natural/even  -- Natural/even is a built-in function
+            , Right = λ(b : Bool) → b
+            }
+in  merge handlers union : Bool

tests/tutorial/unions0A.dhall

@@ -0,0 +1 @@
+./process < Left = +3 | Right : Bool >

tests/tutorial/unions0B.dhall

@@ -0,0 +1 @@
+False

tests/tutorial/unions1A.dhall

@@ -0,0 +1 @@
+./process < Right = True | Left : Natural >

tests/tutorial/unions1B.dhall

@@ -0,0 +1 @@
+True

tests/tutorial/unions2A.dhall

@@ -0,0 +1,8 @@
+    let Empty  = < Empty = {=} | Person : { name : Text, age : Natural } >
+in  let Person =
+        λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} >
+in  [   Empty
+    ,   Person { name = "John", age = +23 }
+    ,   Person { name = "Amy" , age = +25 }
+    ,   Empty
+    ]

tests/tutorial/unions2B.dhall

@@ -0,0 +1,5 @@
+[ < Empty = {=} | Person : { age : Natural, name : Text } >
+, < Person = { age = +23, name = "John" } | Empty : {} >
+, < Person = { age = +25, name = "Amy" } | Empty : {} >
+, < Empty = {=} | Person : { age : Natural, name : Text } >
+]

tests/tutorial/unions3A.dhall

@@ -0,0 +1,5 @@
+    let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } >
+in  [   MyType.Empty {=}
+    ,   MyType.Person { name = "John", age = +23 }
+    ,   MyType.Person { name = "Amy" , age = +25 }
+    ]

tests/tutorial/unions3B.dhall

@@ -0,0 +1,4 @@
+[ < Empty = {=} | Person : { age : Natural, name : Text } >
+, < Person = { age = +23, name = "John" } | Empty : {} >
+, < Person = { age = +25, name = "Amy" } | Empty : {} >
+]

tests/tutorial/unions4A.dhall

@@ -0,0 +1 @@
+constructors < Empty : {} | Person : { name : Text, age : Natural } >

tests/tutorial/unions4B.dhall

@@ -0,0 +1,6 @@
+{ Empty  =
+    λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } >
+, Person =
+      λ(Person : { age : Natural, name : Text })
+    → < Person = Person | Empty : {} >
+}