dhall 1.0.2 → 1.1.0
raw patch · 11 files changed
+450/−305 lines, 11 filesdep +lensdep −microlensdep −microlens-mtlPVP ok
version bump matches the API change (PVP)
Dependencies added: lens
Dependencies removed: microlens, microlens-mtl
API changes (from Hackage documentation)
+ Dhall: InvalidType :: InvalidType
+ Dhall: data InvalidType
+ Dhall: instance GHC.Exception.Exception Dhall.InvalidType
+ Dhall: instance GHC.Show.Show Dhall.InvalidType
+ Dhall.Parser: exprA :: Show a => Parser a -> Parser (Expr Src a)
+ Dhall.TypeCheck: MismatchedListElements :: Int -> (Expr s X) -> (Expr s X) -> (Expr s X) -> TypeMessage s
+ Dhall.TypeCheck: MissingListType :: TypeMessage s
- Dhall.Core: ListLit :: (Expr s a) -> (Vector (Expr s a)) -> Expr s a
+ Dhall.Core: ListLit :: (Maybe (Expr s a)) -> (Vector (Expr s a)) -> Expr s a
Files
- CHANGELOG.md +24/−0
- LICENSE +1/−1
- dhall.cabal +6/−4
- exec/Main.hs +0/−2
- src/Dhall.hs +41/−11
- src/Dhall/Context.hs +6/−5
- src/Dhall/Core.hs +92/−86
- src/Dhall/Import.hs +11/−10
- src/Dhall/Parser.hs +111/−103
- src/Dhall/Tutorial.hs +55/−69
- src/Dhall/TypeCheck.hs +103/−14
+ CHANGELOG.md view
@@ -0,0 +1,24 @@+1.1.0++* BREAKING CHANGE: Non-empty lists no longer require a type annotation+ * This is a breaking change to the Haskell library, not the Dhall language+ * This change does not break existing Dhall programs+ * The `Expr` type was modified in a non-backwards-compatible way+* Add new `exprA` parser+* Add new `InvalidType` exception if `input` fails on an invalid `Type`+* Improve documentation and tutorial++1.0.2++* Add support for Nix-style "double single-quote" multi-line string literals+* Add `isNormalized`+* Improve documentation and tutorial+* Build against wider range of `http-client` versions++1.0.1++* Initial release++1.0.0++* Accidental premature upload to Hackage. This release was blacklisted
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2016 Gabriel Gonzalez+Copyright (c) 2017 Gabriel Gonzalez All rights reserved. Redistribution and use in source and binary forms, with or without modification,
dhall.cabal view
@@ -1,11 +1,11 @@ Name: dhall-Version: 1.0.2+Version: 1.1.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 7.10.2, GHC == 8.0.1 License: BSD3 License-File: LICENSE-Copyright: 2016 Gabriel Gonzalez+Copyright: 2017 Gabriel Gonzalez Author: Gabriel Gonzalez Maintainer: Gabriel439@gmail.com Bug-Reports: https://github.com/Gabriel439/Haskell-Dhall-Library/issues@@ -22,6 +22,7 @@ . Read "Dhall.Tutorial" to learn how to use this library Category: Compiler+Extra-Source-Files: CHANGELOG.md Source-Repository head Type: git Location: https://github.com/Gabriel439/Haskell-Dhall-Library@@ -35,8 +36,7 @@ containers >= 0.5.0.0 && < 0.6 , http-client >= 0.4.30 && < 0.6 , http-client-tls >= 0.2.0 && < 0.4 ,- microlens >= 0.2.0.0 && < 0.5 ,- microlens-mtl >= 0.1.3.1 && < 0.2 ,+ lens >= 2.4 && < 4.16, neat-interpolation >= 0.3.2.1 && < 0.4 , parsers >= 0.12.4 && < 0.13, system-filepath >= 0.3.1 && < 0.5 ,@@ -55,6 +55,7 @@ Dhall.Parser, Dhall.Tutorial, Dhall.TypeCheck+ GHC-Options: -Wall Executable dhall Hs-Source-Dirs: exec@@ -65,3 +66,4 @@ optparse-generic >= 1.1.1 && < 1.2, trifecta >= 1.6 && < 1.7, text >= 0.11.1.0 && < 1.3+ GHC-Options: -Wall
exec/Main.hs view
@@ -8,7 +8,6 @@ import Control.Exception (SomeException) import Data.Monoid (mempty)-import Data.Traversable import Dhall.Core (pretty, normalize) import Dhall.Import (Imported(..), load) import Dhall.Parser (Src, exprFromText)@@ -22,7 +21,6 @@ import qualified Data.Text.Lazy.IO import qualified Dhall.TypeCheck import qualified Options.Generic-import qualified System.Exit import qualified System.IO data Mode = Default | Resolve | TypeCheck | Normalize
src/Dhall.hs view
@@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-}@@ -20,6 +21,7 @@ -- * Types , Type , Interpret(..)+ , InvalidType(..) , bool , natural , integer@@ -54,6 +56,7 @@ import qualified Control.Exception import qualified Data.ByteString.Lazy import qualified Data.Map+import qualified Data.Text import qualified Data.Text.Lazy import qualified Data.Text.Lazy.Builder import qualified Data.Text.Lazy.Encoding@@ -62,19 +65,41 @@ import qualified Dhall.Import import qualified Dhall.Parser import qualified Dhall.TypeCheck-import qualified GHC.Generics+import qualified NeatInterpolation throws :: Exception e => Either e a -> IO a throws (Left e) = Control.Exception.throwIO e throws (Right r) = return r +{-| Every `Type` must obey the contract that if an expression's type matches the+ the `expected` type then the `extract` function must succeed. If not, then+ this exception is thrown++ This exception indicates that an invalid `Type` was provided to the `input`+ function+-}+data InvalidType = InvalidType deriving (Typeable)++_ERROR :: Data.Text.Text+_ERROR = "\ESC[1;31mError\ESC[0m"++instance Show InvalidType where+ show InvalidType = Data.Text.unpack [NeatInterpolation.text|+$_ERROR: Invalid Dhall.Type++Every Type must provide an extract function that succeeds if an expression+matches the expected type. You provided a Type that disobeys this contract+|]++instance Exception InvalidType+ {-| Type-check and evaluate a Dhall program, decoding the result into Haskell The first argument determines the type of value that you decode: >>> input integer "2" 2->>> input (vector double) "[ 1.0, 2.0 ] : List Bool"+>>> input (vector double) "[1.0, 2.0]" [1.0,2.0] Use `auto` to automatically select which type to decode based on the@@ -90,10 +115,10 @@ -- ^ The Dhall program -> IO a -- ^ The decoded value in Haskell-input (Type {..}) text = do+input (Type {..}) txt = do let delta = Directed "(input)" 0 0 0 0- expr <- throws (Dhall.Parser.exprFromText delta text)- expr' <- Dhall.Import.load expr+ expr <- throws (Dhall.Parser.exprFromText delta txt)+ expr' <- Dhall.Import.load expr let suffix = ( Data.ByteString.Lazy.toStrict . Data.Text.Lazy.Encoding.encodeUtf8@@ -107,10 +132,10 @@ bytes' = bytes <> " : " <> suffix _ -> Annot expr' expected- typeExpr <- throws (Dhall.TypeCheck.typeOf annot)+ _ <- throws (Dhall.TypeCheck.typeOf annot) case extract (Dhall.Core.normalize expr') of Just x -> return x- Nothing -> fail "input: malformed `Type`"+ Nothing -> Control.Exception.throwIO InvalidType {-| Use this to provide more detailed error messages @@ -326,30 +351,32 @@ extractOut (OptionalLit _ es) = traverse extractIn es' where es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es)+ extractOut _ = Nothing expectedOut = App Optional expectedIn {-| Decode a `Vector` ->>> input (vector integer) "[ 1, 2, 3 ] : List Integer"+>>> input (vector integer) "[1, 2, 3]" [1,2,3] -} vector :: Type a -> Type (Vector a) vector (Type extractIn expectedIn) = Type extractOut expectedOut where extractOut (ListLit _ es) = traverse extractIn es+ extractOut _ = Nothing expectedOut = App List expectedIn {-| Any value that implements `Interpret` can be automatically decoded based on the inferred return type of `input` ->>> input auto "[1, 2, 3 ] : List Integer" :: IO (Vector Integer)+>>> input auto "[1, 2, 3]" :: IO (Vector Integer) [1,2,3] This class auto-generates a default implementation for records that- implement `Generic`. This does not auto-generate an instance for sum types- nor recursive types.+ implement `Generic`. This does not auto-generate an instance for recursive+ types. -} class Interpret a where auto :: Type a@@ -406,6 +433,7 @@ | name == nameL = fmap (L1 . M1) (extractL e) | name == nameR = fmap (R1 . M1) (extractR e) | otherwise = Nothing+ extract _ = Nothing expected = Union (Data.Map.fromList [(nameL, expectedL), (nameR, expectedR)])@@ -424,6 +452,7 @@ extract u@(UnionLit name' e _) | name == name' = fmap (R1 . M1) (extractR e) | otherwise = fmap L1 (extractL u)+ extract _ = Nothing expected = Union (Data.Map.insert name expectedR expectedL) @@ -441,6 +470,7 @@ extract u@(UnionLit name' e _) | name == name' = fmap (L1 . M1) (extractL e) | otherwise = fmap R1 (extractR u)+ extract _ = Nothing expected = Union (Data.Map.insert name expectedL expectedR)
src/Dhall/Context.hs view
@@ -16,7 +16,8 @@ import Data.Text.Lazy (Text) import Prelude hiding (lookup) -{-| A @(Context a)@ associates `Text` labels with values of type @a@+{-| A @(Context a)@ associates `Text` labels with values of type @a@. Each+ `Text` label can correspond to multiple values of type @a@ The `Context` is used for type-checking when @(a = Expr X)@ @@ -24,9 +25,9 @@ * You transform a `Context` using `fmap` * You consume a `Context` using `lookup` and `toList` - The difference between a `Context` and a `Map` is that a `Context` lets you- have multiple ordered occurrences of the same key and you can query for the- @n@th occurrence of a given key.+ The difference between a `Context` and a `Data.Map.Map` is that a `Context`+ lets you have multiple ordered occurrences of the same key and you can+ query for the @n@th occurrence of a given key. -} newtype Context a = Context { getContext :: [(Text, a)] } deriving (Functor)@@ -44,7 +45,7 @@ > lookup _ _ empty = Nothing > lookup k 0 (insert k v c) = Just v-> lookup k n (insert k v c) = lookup k (n - 1) c -- 1 <= n+> lookup k n (insert k v c) = lookup k (n - 1) c > lookup k n (insert j v c) = lookup k n c -- k /= j -} lookup :: Text -> Integer -> Context a -> Maybe a
src/Dhall/Core.hs view
@@ -112,25 +112,25 @@ nearest bound variable and the index increases by one for each bound variable of the same name going outward. The following diagram may help: -> +---refers to--+-> | |-> v |-> \(x : Type) -> \(y : Type) -> \(x : Type) -> x@0+> ┌──refers to──┐+> │ │+> v │+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0 >-> +------------------refers to-----------------+-> | |-> v |-> \(x : Type) -> \(y : Type) -> \(x : Type) -> x@1+> ┌─────────────────refers to─────────────────┐+> │ │+> v │+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1 This `Int` behaves like a De Bruijn index in the special case where all variables have the same name. You can optionally omit the index if it is @0@: -> +refers to+-> | |-> v |-> \(x : *) -> \(y : *) -> \(x : *) -> x+> ┌─refers to─┐+> │ │+> v │+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x Zero indices are omitted when pretty-printing `Var`s and non-zero indices appear as a numeric suffix.@@ -158,8 +158,8 @@ | Pi Text (Expr s a) (Expr s a) -- | > App f a ~ f a | App (Expr s a) (Expr s a)- -- | > Let x Nothing r e ~ let x = r in e- -- > Let x (Just t) r e ~ let x : t = r in e+ -- | > Let x Nothing r e ~ let x = r in e+ -- > Let x (Just t) r e ~ let x : t = r in e | Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a) -- | > Annot x t ~ x : t | Annot (Expr s a) (Expr s a)@@ -211,8 +211,9 @@ | TextAppend (Expr s a) (Expr s a) -- | > List ~ List | List- -- | > ListLit t [x, y, z] ~ [x, y, z] : List t- | ListLit (Expr s a) (Vector (Expr s a))+ -- | > ListLit (Just t ) [x, y, z] ~ [x, y, z] : List t+ -- > ListLit Nothing [x, y, z] ~ [x, y, z]+ | ListLit (Maybe (Expr s a)) (Vector (Expr s a)) -- | > ListBuild ~ List/build | ListBuild -- | > ListFold ~ List/fold@@ -238,9 +239,9 @@ | Record (Map Text (Expr s a)) -- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 } | RecordLit (Map Text (Expr s a))- -- | > Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >+ -- | > Union [(k1, t1), (k2, t2)] ~ < k1 : t1 | k2 : t2 > | Union (Map Text (Expr s a))- -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 > + -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1 | k2 : t2 | k3 : t3 > | UnionLit Text (Expr s a) (Map Text (Expr s a)) -- | > Combine x y ~ x ∧ y | Combine (Expr s a) (Expr s a)@@ -262,57 +263,57 @@ instance Monad (Expr s) where return = pure - Const c >>= _ = Const c- Var v >>= _ = Var v- Lam x _A b >>= k = Lam x (_A >>= k) ( b >>= k)- Pi x _A _B >>= k = Pi x (_A >>= k) (_B >>= k)- App f a >>= k = App (f >>= k) (a >>= k)- Let f mt r e >>= k = Let f (fmap (>>= k) mt) (r >>= k) (e >>= k)- Annot x t >>= k = Annot (x >>= k) (t >>= k)- Bool >>= _ = Bool- BoolLit b >>= _ = BoolLit b- BoolAnd l r >>= k = BoolAnd (l >>= k) (r >>= k)- BoolOr l r >>= k = BoolOr (l >>= k) (r >>= k)- BoolEQ l r >>= k = BoolEQ (l >>= k) (r >>= k)- BoolNE l r >>= k = BoolNE (l >>= k) (r >>= k)- BoolIf x y z >>= k = BoolIf (x >>= k) (y >>= k) (z >>= k)- Natural >>= _ = Natural- NaturalLit n >>= _ = NaturalLit n- NaturalFold >>= _ = NaturalFold- NaturalBuild >>= _ = NaturalBuild- NaturalIsZero >>= _ = NaturalIsZero- NaturalEven >>= _ = NaturalEven- NaturalOdd >>= _ = NaturalOdd- NaturalPlus l r >>= k = NaturalPlus (l >>= k) (r >>= k)- NaturalTimes l r >>= k = NaturalTimes (l >>= k) (r >>= k)- Integer >>= _ = Integer- IntegerLit n >>= _ = IntegerLit n- Double >>= _ = Double- DoubleLit n >>= _ = DoubleLit n- Text >>= _ = Text- TextLit t >>= _ = TextLit t- TextAppend l r >>= k = TextAppend (l >>= k) (r >>= k)- List >>= _ = List- ListLit t es >>= k = ListLit (t >>= k) (fmap (>>= k) es)- ListBuild >>= _ = ListBuild- ListFold >>= _ = ListFold- ListLength >>= _ = ListLength- ListHead >>= _ = ListHead- ListLast >>= _ = ListLast- ListIndexed >>= _ = ListIndexed- ListReverse >>= _ = ListReverse- Optional >>= _ = Optional- OptionalLit t es >>= k = OptionalLit (t >>= k) (fmap (>>= k) es)- OptionalFold >>= _ = OptionalFold- Record kts >>= k = Record (fmap (>>= k) kts)- RecordLit kvs >>= k = RecordLit (fmap (>>= k) kvs)- Union kts >>= k = Union (fmap (>>= k) kts)- UnionLit k' v kts >>= k = UnionLit k' (v >>= k) (fmap (>>= k) kts)- Combine x y >>= k = Combine (x >>= k) (y >>= k)- Merge x y t >>= k = Merge (x >>= k) (y >>= k) (t >>= k)- Field r x >>= k = Field (r >>= k) x- Note a b >>= k = Note a (b >>= k)- Embed r >>= k = k r+ Const a >>= _ = Const a+ Var a >>= _ = Var a+ Lam a b c >>= k = Lam a (b >>= k) (c >>= k)+ Pi a b c >>= k = Pi a (b >>= k) (c >>= k)+ App a b >>= k = App (a >>= k) (b >>= k)+ Let a b c d >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k)+ Annot a b >>= k = Annot (a >>= k) (b >>= k)+ Bool >>= _ = Bool+ BoolLit a >>= _ = BoolLit a+ BoolAnd a b >>= k = BoolAnd (a >>= k) (b >>= k)+ BoolOr a b >>= k = BoolOr (a >>= k) (b >>= k)+ BoolEQ a b >>= k = BoolEQ (a >>= k) (b >>= k)+ BoolNE a b >>= k = BoolNE (a >>= k) (b >>= k)+ BoolIf a b c >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k)+ Natural >>= _ = Natural+ NaturalLit a >>= _ = NaturalLit a+ NaturalFold >>= _ = NaturalFold+ NaturalBuild >>= _ = NaturalBuild+ NaturalIsZero >>= _ = NaturalIsZero+ NaturalEven >>= _ = NaturalEven+ NaturalOdd >>= _ = NaturalOdd+ NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k)+ NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k)+ Integer >>= _ = Integer+ IntegerLit a >>= _ = IntegerLit a+ Double >>= _ = Double+ DoubleLit a >>= _ = DoubleLit a+ Text >>= _ = Text+ TextLit a >>= _ = TextLit a+ TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k)+ List >>= _ = List+ ListLit a b >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)+ ListBuild >>= _ = ListBuild+ ListFold >>= _ = ListFold+ ListLength >>= _ = ListLength+ ListHead >>= _ = ListHead+ ListLast >>= _ = ListLast+ ListIndexed >>= _ = ListIndexed+ ListReverse >>= _ = ListReverse+ Optional >>= _ = Optional+ OptionalLit a b >>= k = OptionalLit (a >>= k) (fmap (>>= k) b)+ OptionalFold >>= _ = OptionalFold+ Record a >>= k = Record (fmap (>>= k) a)+ RecordLit a >>= k = RecordLit (fmap (>>= k) a)+ Union a >>= k = Union (fmap (>>= k) a)+ UnionLit a b c >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)+ Combine a b >>= k = Combine (a >>= k) (b >>= k)+ Merge a b c >>= k = Merge (a >>= k) (b >>= k) (c >>= k)+ Field a b >>= k = Field (a >>= k) b+ Note a b >>= k = Note a (b >>= k)+ Embed a >>= k = k a instance Bifunctor Expr where first _ (Const a ) = Const a@@ -346,7 +347,7 @@ first _ (TextLit a ) = TextLit a first k (TextAppend a b ) = TextAppend (first k a) (first k b) first _ List = List- first k (ListLit a b ) = ListLit (first k a) (fmap (first k) b)+ first k (ListLit a b ) = ListLit (fmap (first k) a) (fmap (first k) b) first _ ListBuild = ListBuild first _ ListFold = ListFold first _ ListLength = ListLength@@ -369,8 +370,7 @@ second = fmap -instance IsString (Expr s a)- where+instance IsString (Expr s a) where fromString str = Var (fromString str) {- There is a one-to-one correspondence between the builders in this section@@ -461,7 +461,9 @@ <> buildExprA c <> " in " <> buildExprB d-buildExprB (ListLit a b) =+buildExprB (ListLit Nothing b) =+ "[" <> buildElems (Data.Vector.toList b) <> "]"+buildExprB (ListLit (Just a) b) = "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExprE a buildExprB (OptionalLit a b) = "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExprE a@@ -680,7 +682,8 @@ buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExprA b -- | Builder corresponding to the @unionLit@ parser in "Dhall.Parser"-buildUnionLit :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder+buildUnionLit+ :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder buildUnionLit a b c | Data.Map.null c = "< "@@ -847,7 +850,7 @@ shift _ _ List = List shift d v (ListLit a b) = ListLit a' b' where- a' = shift d v a+ a' = fmap (shift d v) a b' = fmap (shift d v) b shift _ _ ListBuild = ListBuild shift _ _ ListFold = ListFold@@ -978,7 +981,7 @@ subst _ _ List = List subst x e (ListLit a b) = ListLit a' b' where- a' = subst x e a+ a' = fmap (subst x e) a b' = fmap (subst x e) b subst _ _ ListBuild = ListBuild subst _ _ ListFold = ListFold@@ -1078,7 +1081,7 @@ App NaturalEven (NaturalLit n) -> BoolLit (even n) App NaturalOdd (NaturalLit n) -> BoolLit (odd n) App (App ListBuild t) k- | check -> ListLit t (buildVector k')+ | check -> ListLit (Just t) (buildVector k') | otherwise -> App f' a' where labeled =@@ -1100,16 +1103,16 @@ cons' y ys = App (App cons y) ys App (App ListLength _) (ListLit _ ys) -> NaturalLit (fromIntegral (Data.Vector.length ys))- App (App ListHead _) (ListLit t ys) ->+ App (App ListHead t) (ListLit _ ys) -> normalize (OptionalLit t (Data.Vector.take 1 ys))- App (App ListLast _) (ListLit t ys) ->+ App (App ListLast t) (ListLit _ ys) -> normalize (OptionalLit t y) where y = if Data.Vector.null ys then Data.Vector.empty else Data.Vector.singleton (Data.Vector.last ys)- App (App ListIndexed _) (ListLit t xs) ->- normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))+ App (App ListIndexed t) (ListLit _ xs) ->+ normalize (ListLit (Just t') (fmap adapt (Data.Vector.indexed xs))) where t' = Record (Data.Map.fromList kts) where@@ -1121,8 +1124,8 @@ kvs = [ ("index", NaturalLit (fromIntegral n)) , ("value", x) ]- App (App ListReverse _) (ListLit t xs) ->- normalize (ListLit t (Data.Vector.reverse xs))+ App (App ListReverse t) (ListLit _ xs) ->+ normalize (ListLit (Just t) (Data.Vector.reverse xs)) App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing -> normalize (maybe nothing just' (toMaybe xs)) where@@ -1232,7 +1235,7 @@ List -> List ListLit t es -> ListLit t' es' where- t' = normalize t+ t' = fmap normalize t es' = fmap normalize es ListBuild -> ListBuild ListFold -> ListFold@@ -1421,7 +1424,7 @@ _ -> True _ -> True List -> True- ListLit t es -> isNormalized t && all isNormalized es+ ListLit t es -> all isNormalized t && all isNormalized es ListBuild -> True ListFold -> True ListLength -> True@@ -1463,12 +1466,15 @@ Note _ e' -> isNormalized e' Embed _ -> True +_ERROR :: Data.Text.Text+_ERROR = "\ESC[1;31mError\ESC[0m"+ {-| Utility function used to throw internal errors that should never happen (in theory) but that are not enforced by the type system -} internalError :: Data.Text.Text -> forall b . b internalError text = error (Data.Text.unpack [NeatInterpolation.text|-Error: Compiler bug+$_ERROR: Compiler bug Explanation: This error message means that there is a bug in the Dhall compiler. You didn't do anything wrong, but if you would like to see this problem fixed
src/Dhall/Import.hs view
@@ -75,6 +75,7 @@ import Control.Exception (Exception, IOException, SomeException, catch, onException, throwIO)+import Control.Lens (Lens', zoom) import Control.Monad (join) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT)@@ -90,13 +91,12 @@ #endif import Data.Typeable (Typeable) import Filesystem.Path ((</>), FilePath)-import Lens.Micro (Lens')-import Lens.Micro.Mtl (zoom) import Dhall.Core (Expr, Path(..)) import Dhall.Parser (Parser(..), ParseError(..), Src) import Dhall.TypeCheck (X(..)) #if MIN_VERSION_http_client(0,5,0)-import Network.HTTP.Client (HttpException(..), HttpExceptionContent(..), Manager)+import Network.HTTP.Client+ (HttpException(..), HttpExceptionContent(..), Manager) #else import Network.HTTP.Client (HttpException(..), Manager) #endif@@ -142,7 +142,7 @@ To be precise, a strong interpretaton of referential transparency means that if you compiled a URL you could replace the expression hosted at that URL- with the compiled result. Let's term this \"static linking\". Dhall (very+ with the compiled result. Let's call this \"static linking\". Dhall (very intentionally) does not satisfy this stronger interpretation of referential transparency since \"statically linking\" an expression (i.e. permanently resolving all imports) means that the expression will no longer update if@@ -183,9 +183,11 @@ instance Show e => Show (Imported e) where show (Imported paths e) = (case paths of [] -> ""; _ -> "\n")- ++ unlines (map (\(n, path) -> take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)) paths')+ ++ unlines (map indent paths') ++ show e where+ indent (n, path) =+ take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path) -- Canonicalize all paths paths' = zip [0..] (drop 1 (reverse (canonicalizeAll paths))) @@ -295,7 +297,7 @@ if you navigate to any downstream relative paths * Removing spurious @.@s and @..@s from the path - Also, there are way too many `reverse`s in the URL-handling cod For now I+ Also, there are way too many `reverse`s in the URL-handling code For now I don't mind, but if were to really do this correctly we'd store the URLs as `Text` for O(1) access to the end of the string. The only reason we use `String` at all is for consistency with the @http-client@ library.@@ -369,10 +371,9 @@ exprFromFile path = do let string = Filesystem.Path.CurrentOS.encodeString path - -- Unfortunately, GHC throws an `InappropriateType`- -- exception when trying to read a directory, but does not- -- export the exception, so I must resort to a more- -- heavy-handed `catch`+ -- Unfortunately, GHC throws an `InappropriateType` exception when trying to+ -- to read a directory, but does not export the exception, so I must resort+ -- to a more heavy-handed `catch` let handler :: IOException -> IO (Result (Expr Src Path)) handler e = do let string' = Filesystem.Path.CurrentOS.encodeString (path </> "@")
src/Dhall/Parser.hs view
@@ -9,7 +9,7 @@ exprFromText -- * Parsers- , expr+ , expr, exprA -- * Types , Src(..)@@ -34,10 +34,8 @@ import Prelude hiding (FilePath, const, pi) import Text.PrettyPrint.ANSI.Leijen (Doc) import Text.Parser.Combinators (choice, try, (<?>))-import Text.Parser.Expression (Assoc(..), Operator(..)) import Text.Parser.Token (IdentifierStyle(..), TokenParsing(..)) import Text.Parser.Token.Highlight (Highlight(..))-import Text.Parser.Token.Style (CommentStyle(..)) import Text.Trifecta (CharParsing, DeltaParsing, MarkParsing, Parsing, Result(..)) import Text.Trifecta.Delta (Delta)@@ -45,7 +43,6 @@ import qualified Data.Char import qualified Data.HashSet import qualified Data.Map-import qualified Data.ByteString import qualified Data.ByteString.Lazy import qualified Data.List import qualified Data.Sequence@@ -58,13 +55,10 @@ import qualified Filesystem.Path.CurrentOS import qualified Text.Parser.Char import qualified Text.Parser.Combinators-import qualified Text.Parser.Expression import qualified Text.Parser.Token import qualified Text.Parser.Token.Style import qualified Text.PrettyPrint.ANSI.Leijen import qualified Text.Trifecta-import qualified Text.Trifecta.Combinators-import qualified Text.Trifecta.Delta -- | Source code extract data Src = Src Delta Delta ByteString deriving (Show)@@ -160,10 +154,10 @@ noted :: Parser (Expr Src a) -> Parser (Expr Src a) noted parser = do- before <- Text.Trifecta.position- (expr, bytes) <- Text.Trifecta.slicedWith (,) parser- after <- Text.Trifecta.position- return (Note (Src before after bytes) expr)+ before <- Text.Trifecta.position+ (e, bytes) <- Text.Trifecta.slicedWith (,) parser+ after <- Text.Trifecta.position+ return (Note (Src before after bytes) e) toMap :: [(Text, a)] -> Parser (Map Text a) toMap kvs = do@@ -219,18 +213,18 @@ _ -> minimum (map indentLength nonEmptyLines) p0 = do- Text.Parser.Char.string "''"+ _ <- Text.Parser.Char.string "''" p1 p1 = p2 <|> p3 <|> p4 <|> p5 p2 = do- Text.Parser.Char.text "'''"+ _ <- Text.Parser.Char.text "'''" s1 <- p1 return ("''" <> s1) p3 = do- Text.Parser.Char.text "''"+ _ <- Text.Parser.Char.text "''" return "" p4 = do@@ -260,28 +254,30 @@ -- | Parser for a top-level Dhall expression expr :: Parser (Expr Src Path)-expr = exprA+expr = exprA import_ -exprA :: Parser (Expr Src Path)-exprA = do- a <- exprB+-- | Parser for a top-level Dhall expression. The expression is parameterized+-- over any parseable type, allowing the language to be extended as needed.+exprA :: Show a => Parser a -> Parser (Expr Src a)+exprA embedded = noted (do+ a <- exprB embedded let exprA0 = do symbol ":"- b <- exprA+ b <- exprA embedded return (Annot a b) let exprA1 = pure a - exprA0 <|> exprA1+ exprA0 <|> exprA1 ) -exprB :: Parser (Expr Src Path)-exprB = choice+exprB :: Show a => Parser a -> Parser (Expr Src a)+exprB embedded = choice [ noted exprB0 , noted exprB1 , noted exprB3 , noted exprB5- , noted exprB6+ , noted (try exprB6) , noted exprB7 , noted (try exprB2) , exprB8@@ -292,25 +288,25 @@ symbol "(" a <- label symbol ":"- b <- exprA+ b <- exprA embedded symbol ")" arrow- c <- exprB+ c <- exprB embedded return (Lam a b c) exprB1 = do reserve "if"- a <- exprA+ a <- exprA embedded reserve "then"- b <- exprB+ b <- exprB embedded reserve "else"- c <- exprC+ c <- exprC embedded return (BoolIf a b c) exprB2 = do- a <- exprC+ a <- exprC embedded arrow- b <- exprB+ b <- exprB embedded return (Pi "_" a b) exprB3 = do@@ -318,10 +314,10 @@ symbol "(" a <- label symbol ":"- b <- exprA+ b <- exprA embedded symbol ")" arrow- c <- exprB+ c <- exprB embedded return (Pi a b c) exprB5 = do@@ -329,33 +325,33 @@ a <- label b <- optional (do symbol ":"- exprA )+ exprA embedded ) symbol "="- c <- exprA+ c <- exprA embedded reserve "in"- d <- exprB+ d <- exprB embedded return (Let a b c d) exprB6 = do symbol "["- a <- elems+ a <- elems embedded symbol "]" symbol ":" b <- listLike- c <- exprE- return (b c (Data.Vector.fromList a))+ c <- exprE embedded+ return (b c a) exprB7 = do reserve "merge"- a <- exprE- b <- exprE+ a <- exprE embedded+ b <- exprE embedded symbol ":"- c <- exprD+ c <- exprD embedded return (Merge a b c) - exprB8 = exprC+ exprB8 = exprC embedded -listLike :: Parser (Expr Src Path -> Vector (Expr Src Path) -> Expr Src Path)+listLike :: Parser (Expr Src a -> Vector (Expr Src a) -> Expr Src a) listLike = ( listLike0 <|> listLike1@@ -363,18 +359,18 @@ where listLike0 = do reserve "List"- return ListLit+ return (\a b -> ListLit (Just a) b) listLike1 = do reserve "Optional" return OptionalLit -exprC :: Parser (Expr Src Path)-exprC = exprC0+exprC :: Show a => Parser a -> Parser (Expr Src a)+exprC embedded = exprC0 where chain pA pOp op pB = noted (do a <- pA- try (do pOp <?> "operator"; b <- pB; return (op a b)) <|> pure a )+ try (do _ <- pOp <?> "operator"; b <- pB; return (op a b)) <|> pure a ) exprC0 = chain exprC1 (symbol "||") BoolOr exprC0 exprC2 = chain exprC3 (symbol "++") TextAppend exprC2@@ -383,7 +379,7 @@ exprC4 = chain exprC5 combine Combine exprC4 exprC5 = chain exprC6 (symbol "*" ) NaturalTimes exprC5 exprC6 = chain exprC7 (symbol "==") BoolEQ exprC6- exprC7 = chain exprD (symbol "!=") BoolNE exprC7+ exprC7 = chain (exprD embedded) (symbol "!=") BoolNE exprC7 -- We can't use left-recursion to define `exprD` otherwise the parser will -- loop infinitely. However, I'd still like to use left-recursion in the@@ -393,25 +389,25 @@ -- * First, parse to count how many arguments the function is applied to -- * Second, restart the parse using left recursion bounded by the number of -- arguments-exprD :: Parser (Expr Src Path)-exprD = do- es <- some (noted (try exprE))- let app nL@(Note (Src before _ bytesL) eL) nR@(Note (Src _ after bytesR) eR) =+exprD :: Show a => Parser a -> Parser (Expr Src a)+exprD embedded = do+ es <- some (noted (try (exprE embedded)))+ let app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) = Note (Src before after (bytesL <> bytesR)) (App nL nR) app _ _ = Dhall.Core.internalError ("Dhall.Parser.exprD: foldl1 app (" <> Data.Text.pack (show es) <> ")") return (Data.List.foldl1 app es) -exprE :: Parser (Expr Src Path)-exprE = noted (do- a <- exprF+exprE :: Show a => Parser a -> Parser (Expr Src a)+exprE embedded = noted (do+ a <- exprF embedded b <- many (try (do symbol "." label )) return (Data.List.foldl Field a b) ) -exprF :: Parser (Expr Src Path)-exprF = choice+exprF :: Show a => Parser a -> Parser (Expr Src a)+exprF embedded = choice [ noted (try exprF26) , noted (try exprF25) , noted exprF24@@ -421,6 +417,7 @@ , noted (try exprF30) , noted exprF31 , noted exprF32+ , noted exprF33 , (choice [ noted exprF03 , noted exprF04@@ -448,7 +445,7 @@ ] ) <?> "built-in value" , noted exprF00- , exprF33+ , exprF34 ] where exprF00 = do@@ -552,7 +549,7 @@ return (IntegerLit a) exprF25 = (do- Text.Parser.Char.char '+'+ _ <- Text.Parser.Char.char '+' a <- Text.Parser.Token.natural return (NaturalLit (fromIntegral a)) ) <?> "natural" @@ -567,21 +564,23 @@ a <- stringLiteral return (TextLit a) - exprF28 = record <?> "record type"+ exprF28 = record embedded <?> "record type" - exprF29 = recordLit <?> "record literal"+ exprF29 = recordLit embedded <?> "record literal" - exprF30 = union <?> "union type"+ exprF30 = union embedded <?> "union type" - exprF31 = unionLit <?> "union literal"+ exprF31 = unionLit embedded <?> "union literal" - exprF32 = do- a <- import_ <?> "import"- return (Embed a)+ exprF32 = listLit embedded <?> "list literal" exprF33 = do+ a <- embedded <?> "import"+ return (Embed a)++ exprF34 = do symbol "("- a <- exprA+ a <- exprA embedded symbol ")" return a @@ -604,15 +603,17 @@ symbol "@" Text.Parser.Token.natural ) let b = case m of- Just b -> b+ Just r -> r Nothing -> 0 return (V a b) -elems :: Parser [Expr Src Path]-elems = Text.Parser.Combinators.sepBy exprA (symbol ",")+elems :: Show a => Parser a -> Parser (Vector (Expr Src a))+elems embedded = do+ a <- Text.Parser.Combinators.sepBy (exprA embedded) (symbol ",")+ return (Data.Vector.fromList a) -recordLit :: Parser (Expr Src Path)-recordLit =+recordLit :: Show a => Parser a -> Parser (Expr Src a)+recordLit embedded = recordLit0 <|> recordLit1 where@@ -622,62 +623,62 @@ recordLit1 = do symbol "{"- a <- fieldValues+ a <- fieldValues embedded b <- toMap a symbol "}" return (RecordLit b) -fieldValues :: Parser [(Text, Expr Src Path)]-fieldValues =- Text.Parser.Combinators.sepBy1 fieldValue (symbol ",")+fieldValues :: Show a => Parser a -> Parser [(Text, Expr Src a)]+fieldValues embedded =+ Text.Parser.Combinators.sepBy1 (fieldValue embedded) (symbol ",") -fieldValue :: Parser (Text, Expr Src Path)-fieldValue = do+fieldValue :: Show a => Parser a -> Parser (Text, Expr Src a)+fieldValue embedded = do a <- label symbol "="- b <- exprA+ b <- exprA embedded return (a, b) -record :: Parser (Expr Src Path)-record = do+record :: Show a => Parser a -> Parser (Expr Src a)+record embedded = do symbol "{"- a <- fieldTypes+ a <- fieldTypes embedded b <- toMap a symbol "}" return (Record b) -fieldTypes :: Parser [(Text, Expr Src Path)]-fieldTypes =- Text.Parser.Combinators.sepBy fieldType (symbol ",")+fieldTypes :: Show a => Parser a -> Parser [(Text, Expr Src a)]+fieldTypes embedded =+ Text.Parser.Combinators.sepBy (fieldType embedded) (symbol ",") -fieldType :: Parser (Text, Expr Src Path)-fieldType = do+fieldType :: Show a => Parser a -> Parser (Text, Expr Src a)+fieldType embedded = do a <- label symbol ":"- b <- exprA+ b <- exprA embedded return (a, b) -union :: Parser (Expr Src Path)-union = do+union :: Show a => Parser a -> Parser (Expr Src a)+union embedded = do symbol "<"- a <- alternativeTypes+ a <- alternativeTypes embedded b <- toMap a symbol ">" return (Union b) -alternativeTypes :: Parser [(Text, Expr Src Path)]-alternativeTypes =- Text.Parser.Combinators.sepBy alternativeType (symbol "|")+alternativeTypes :: Show a => Parser a -> Parser [(Text, Expr Src a)]+alternativeTypes embedded =+ Text.Parser.Combinators.sepBy (alternativeType embedded) (symbol "|") -alternativeType :: Parser (Text, Expr Src Path)-alternativeType = do+alternativeType :: Show a => Parser a -> Parser (Text, Expr Src a)+alternativeType embedded = do a <- label symbol ":"- b <- exprA+ b <- exprA embedded return (a, b) -unionLit :: Parser (Expr Src Path)-unionLit =+unionLit :: Show a => Parser a -> Parser (Expr Src a)+unionLit embedded = try unionLit0 <|> unionLit1 where@@ -685,7 +686,7 @@ symbol "<" a <- label symbol "="- b <- exprA+ b <- exprA embedded symbol ">" return (UnionLit a b Data.Map.empty) @@ -693,13 +694,20 @@ symbol "<" a <- label symbol "="- b <- exprA+ b <- exprA embedded symbol "|"- c <- alternativeTypes+ c <- alternativeTypes embedded d <- toMap c symbol ">" return (UnionLit a b d) +listLit :: Show a => Parser a -> Parser (Expr Src a)+listLit embedded = do+ symbol "["+ a <- elems embedded+ symbol "]"+ return (ListLit Nothing a)+ import_ :: Parser Path import_ = do a <- import0 <|> import1@@ -769,7 +777,7 @@ parser = unParser (do Text.Parser.Token.whiteSpace- r <- exprA+ r <- expr Text.Parser.Combinators.eof return r )
src/Dhall/Tutorial.hs view
@@ -18,7 +18,7 @@ -- $lists -- * Optional values- -- $optional+ -- $optional0 -- * Records -- $records@@ -132,7 +132,7 @@ -- $listReverse -- ** @Optional@- -- $optional+ -- $optional1 -- *** @Optional/fold@ -- $optionalFold@@ -148,7 +148,7 @@ ) where import Data.Vector (Vector)-import Dhall (Interpret(..), Type, detailed, input)+import Dhall -- $introduction --@@ -158,7 +158,7 @@ -- -- > $ cat ./config -- > { foo = 1--- > , bar = [3.0, 4.0, 5.0] : List Double+-- > , bar = [3.0, 4.0, 5.0] -- > } -- -- You can read the above configuration file into Haskell using the following@@ -241,13 +241,13 @@ -- Therefore, since we can decode a @Bool@, we must also be able to decode a -- @List@ of @Bool@s, like this: ----- > >>> input auto "[True, False] : List Bool" :: IO (Vector Bool)+-- > >>> input auto "[True, False]" :: IO (Vector Bool) -- > [True,False] -- -- We could also specify what type to decode by providing an explicit `Type` -- instead of using `auto` with a type annotation: ----- > >>> input (vector bool) "[True, False] : List Bool"+-- > >>> input (vector bool) "[True, False]" -- > [True, False] -- -- __Exercise:__ Create a @./config@ file that the following program can decode:@@ -358,7 +358,7 @@ -- -- ... and read in all three files in a single expression: -- --- > >>> input auto "[ ./bool1 , ./bool2 , ./both ] : List Bool" :: IO (Vector Bool)+-- > >>> input auto "[ ./bool1 , ./bool2 , ./both ]" :: IO (Vector Bool) -- > [True,False,False] -- -- Each file path is replaced with the Dhall expression contained within that@@ -375,7 +375,7 @@ -- > } -- > EOF ----- > $ echo "[ 3.0, 4.0, 5.0 ] : List Double" > ./bar+-- > $ echo "[3.0, 4.0, 5.0]" > ./bar -- -- > $ ./example -- > Example {foo = 1, bar = [3.0,4.0,5.0]}@@ -419,7 +419,7 @@ -- -- You can import types, too. For example, we can change our @./bar@ file to: ----- > $ echo "[ 3.0, 4.0, 5.0 ] : List ./type" > ./bar+-- > $ echo "[3.0, 4.0, 5.0] : List ./type" > ./bar -- -- ... then specify the @./type@ in a separate file: --@@ -464,35 +464,39 @@ -- -- You can store 0 or more values of the same type in a list, like this: ----- > [1, 2, 3] : List Integer+-- > [1, 2, 3] ----- Every list must be followed by the type of the list. The type annotation is--- not optional and you will get an error if you omit the annotation:+-- Every list can be followed by the type of the list. The type annotation is+-- required for empty lists but optional for non-empty lists. You will get a+-- type error if you provide an empty list without a type annotation: ----- > >>> input auto "[1, 2, 3]" :: IO (Vector Integer)--- > *** Exception: (input):1:10: error: unexpected--- > EOF, expected: ":"--- > [1, 2, 3]<EOF> --- > ^ +-- > >>> input auto "[]" :: IO (Vector Integer)+-- > *** Exception: +-- > Error: Empty lists need a type annotation+-- > +-- > []+-- > +-- > (input):1:1+-- > >>> input auto "[] : List Integer" :: IO (Vector Integer)+-- > [] ----- Also, list elements must all have the same type which must match the declared--- type of the list. You will get an error if you try to store any other type--- of element:+-- Also, list elements must all have the same type. You will get an error if+-- you try to store elements of different types in a list: ----- > input auto "[1, True, 3] : List Integer" :: IO (Vector Integer)+-- > >>> input auto "[1, True, 3]" :: IO (Vector Integer) -- > *** Exception: --- > Error: List element has the wrong type+-- > Error: List elements should have the same type -- > --- > [1, True, 3] : List Integer+-- > [1, True, 3] -- > -- > (input):1:1 ----- __Exercise:__ Create a @./config@ file that decodes to the following result:+-- __Exercise:__ What is the shortest @./config@ file that you can decode using+-- this command: -- -- > >>> input auto "./config" :: IO (Vector (Vector Integer))--- > [[1,2,3],[4,5,6]] --- $optional+-- $optional0 -- -- @Optional@ values are exactly like lists except they can only hold 0 or 1 -- elements. They cannot hold 2 or more elements:@@ -514,6 +518,9 @@ -- > >>> input auto "[] : Optional Integer" :: IO (Maybe Integer) -- > Nothing --+-- You cannot omit the type annotation for @Optional@ values. The type+-- annotation is mandatory+-- -- __Exercise:__ What is the shortest possible @./config@ file that you can decode -- like this: --@@ -591,7 +598,7 @@ -- -- > $ cat > makeBools -- > \(n : Bool) ->--- > [ n && True, n && False, n || True, n || False ] : List Bool+-- > [ n && True, n && False, n || True, n || False ] -- > <Ctrl-D> -- -- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB)@@ -600,7 +607,7 @@ -- -- > $ cat > makeBools -- > λ(n : Bool) →--- > [ n && True, n && False, n || True, n || False ] : List Bool+-- > [ n && True, n && False, n || True, n || False ] -- > <Ctrl-D> -- -- You can read this as a function of one argument named @n@ that has type@@ -622,7 +629,7 @@ -- > <Ctrl-D> -- > ∀(n : Bool) → List Bool -- > --- > λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool+-- > λ(n : Bool) → [n && True, n && False, n || True, n || False] -- -- The first line says that @makeBools@ is a function of one argument named @n@ -- that has type @Bool@ and the function returns a @List@ of @Bool@s. The @∀@@@ -645,7 +652,7 @@ -- -- The second line of Dhall's output is our program's normal form: ----- > λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool+-- > λ(n : Bool) → [n && True, n && False, n || True, n || False] -- -- ... which in this case happens to be identical to our original program. --@@ -663,17 +670,17 @@ -- > <Ctrl-D> -- > List Bool -- > --- > [True, False, True, True] : List Bool+-- > [True, False, True, True] -- -- Remember that file paths are synonymous with their contents, so the above -- code is exactly equivalent to: -- -- > $ dhall--- > (λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool) True+-- > (λ(n : Bool) → [n && True, n && False, n || True, n || False]) True -- > <Ctrl-D> -- > List Bool -- > --- > [True, False, True, True] : List Bool+-- > [True, False, True, True] -- -- When you apply an anonymous function to an argument, you substitute the -- \"bound variable" with the function's argument:@@ -688,13 +695,13 @@ -- like this: -- -- > -- If we replace all of these `n`s with `True` ...--- > [n && True, n && False, n || True, n || False] : List Bool+-- > [n && True, n && False, n || True, n || False] -- > -- > -- ... then we get this:--- > [True && True, True && False, True || True, True || False] : List Bool+-- > [True && True, True && False, True || True, True || False] -- > -- > -- ... which reduces to the following normal form:--- > [True, False, True, True] : List Bool+-- > [True, False, True, True] -- -- Now that we've verified that our function type checks and works, we can use -- the same function within Haskell:@@ -999,7 +1006,7 @@ -- Notice that each handler has to return the same type of result (@Bool@ in -- this case) which must also match the declared result type of the @merge@. ----- __Exercise__: Create a list of the following type with at least one element:+-- __Exercise__: Create a list of the following type with at least one element -- per alternative: -- -- > List < Left : Integer | Right : Double >@@ -1112,7 +1119,7 @@ -- ... and the second argument is the list to reverse: -- -- > $ dhall--- > List/reverse Bool ([True, False] : List Bool)+-- > List/reverse Bool [True, False] -- > <Ctrl-D> -- > List Bool -- > @@ -1170,7 +1177,7 @@ -- -- > $ dhall -- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map--- > in λ(f : Integer → Integer) → List/map Integer Integer f ([1, 2, 3] : List Integer)+-- > in λ(f : Integer → Integer) → List/map Integer Integer f [1, 2, 3] -- > <Ctrl-D> -- > ∀(f : Integer → Integer) → List Integer -- > @@ -1734,7 +1741,7 @@ -- Example: -- -- > $ dhall--- > List/fold Bool ([True, False, True] : List Bool) Bool (λ(x : Bool) → λ(y : Bool) → x && y) True+-- > List/fold Bool [True, False, True] Bool (λ(x : Bool) → λ(y : Bool) → x && y) True -- > <Ctrl-D> -- > Bool -- > @@ -1783,7 +1790,7 @@ -- Example: -- -- > $ dhall--- > List/length Integer ([1, 2, 3] : List Integer)+-- > List/length Integer [1, 2, 3] -- > <Ctrl-D> -- > Natural -- > @@ -1803,7 +1810,7 @@ -- Example: -- -- > $ dhall--- > List/head Integer ([1, 2, 3] : List Integer)+-- > List/head Integer [1, 2, 3] -- > <Ctrl-D> -- > Optional Integer -- > @@ -1834,7 +1841,7 @@ -- Example: -- -- > $ dhall--- > List/last Integer ([1, 2, 3] : List Integer)+-- > List/last Integer [1, 2, 3] -- > <Ctrl-D> -- > Optional Integer -- > @@ -1865,7 +1872,7 @@ -- Example -- -- > $ dhall--- > List/indexed Text (["ABC", "DEF", "GHI"] : List Text)+-- > List/indexed Text ["ABC", "DEF", "GHI"] -- > <Ctrl-D> -- > List { index : Natural, value : Text } -- > @@ -1890,7 +1897,7 @@ -- Example: -- -- > $ dhall--- > List/reverse Integer ([1, 2, 3] : List Integer)+-- > List/reverse Integer [1, 2, 3] -- > <Ctrl-D> -- > List Integer -- > @@ -1917,9 +1924,9 @@ -- > -- > List/reverse a ([x, y] : List a) = [y, x] : List a --- $optional+-- $optional1 ----- Dhall @Optional@ literals are a 0 or 1 values inside of brackets:+-- Dhall @Optional@ literals are 0 or 1 values inside of brackets: -- -- > Γ ⊢ t : Type Γ ⊢ x : t -- > ────────────────────────@@ -2132,13 +2139,7 @@ -- $faq ----- * Why do lists require a type annotation?------ Dhall requires type annotations on lists in order to gracefully deal with--- empty lists. Without a type annotation the compiler would not be able to--- infer the type of an empty list expression:------ > []+-- * Why do empty lists require a type annotation? -- -- Unlike Haskell, Dhall cannot infer a polymorphic type for the empty list -- because Dhall represents polymorphic values as functions of types, like this:@@ -2149,18 +2150,3 @@ -- the above polymorphic function then you'd get the unexpected behavior where -- a list literal is a function if the list has 0 elements but not a function -- otherwise.------ * Why do lists require a type annotation when using `input`, like this:--- --- > >>> input (list bool) "[True, False] : List Bool"------ The type annotation on a list is not a real type annotation. Instead, the--- annotation on a list is part of the mandatory syntax for lists. This is why--- you get a parse error instead of a type error if you omit the annotation:------ > dhall--- > [1, 2]--- > (stdin):2:1: error: unexpected--- > EOF, expected: ":"--- > <EOF> --- > ^
src/Dhall/TypeCheck.hs view
@@ -117,11 +117,11 @@ go _ _ = return False {-| Type-check an expression and return the expression's type if type-checking- suceeds or an error if type-checking fails+ succeeds or an error if type-checking fails `typeWith` does not necessarily normalize the type since full normalization is not necessary for just type-checking. If you actually care about the- returned type then you may want to `normalize` it afterwards.+ returned type then you may want to `Dhall.Core.normalize` it afterwards. -} typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s) (Expr s X) typeWith _ (Const c ) = do@@ -355,7 +355,26 @@ return Text typeWith _ List = do return (Pi "_" (Const Type) (Const Type))-typeWith ctx e@(ListLit t xs ) = do+typeWith ctx e@(ListLit Nothing xs) = do+ if Data.Vector.null xs+ then Left (TypeError ctx e MissingListType)+ else do+ t <- typeWith ctx (Data.Vector.head xs)+ s <- fmap Dhall.Core.normalize (typeWith ctx t)+ case s of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (InvalidListType t))+ flip Data.Vector.imapM_ xs (\i x -> do+ t' <- typeWith ctx x+ if propEqual t t'+ then return ()+ else do+ let nf_t = Dhall.Core.normalize t+ let nf_t' = Dhall.Core.normalize t'+ let err = MismatchedListElements i nf_t x nf_t'+ Left (TypeError ctx e err) )+ return (App List t)+typeWith ctx e@(ListLit (Just t ) xs) = do s <- fmap Dhall.Core.normalize (typeWith ctx t) case s of Const Type -> return ()@@ -562,6 +581,8 @@ | TypeMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X) | AnnotMismatch (Expr s X) (Expr s X) (Expr s X) | Untyped+ | MissingListType+ | MismatchedListElements Int (Expr s X) (Expr s X) (Expr s X) | InvalidListElement Int (Expr s X) (Expr s X) (Expr s X) | InvalidListType (Expr s X) | InvalidOptionalElement (Expr s X) (Expr s X) (Expr s X)@@ -1121,9 +1142,9 @@ ● You omit a function argument by mistake: - ┌────────────────────────────────────────┐- │ List/head ([1, 2, 3] : List Integer) │- └────────────────────────────────────────┘+ ┌───────────────────────┐+ │ List/head [1, 2, 3] │+ └───────────────────────┘ ⇧ ❰List/head❱ is missing the first argument, which should be: ❰Integer❱@@ -1510,8 +1531,8 @@ long = Builder.fromText [NeatInterpolation.text|-Explanation: Every ❰List❱ documents the type of its elements with a type-annotation, like this:+Explanation: ❰List❱s can optionally document the type of their elements with a+type annotation, like this: ┌──────────────────────────┐@@ -1525,7 +1546,7 @@ │ [] : List Integer │ An empty ❰List❱ └───────────────────┘ ⇧- You still specify the type even when the ❰List❱ is empty+ You must specify the type when the ❰List❱ is empty The element type must be a type and not something else. For example, the@@ -1546,8 +1567,6 @@ This is a ❰Kind❱ and not a ❰Type❱ -Even if the ❰List❱ is empty you still must specify a valid type- You declared that the ❰List❱'s elements should have type: ↳ $txt0@@ -1557,6 +1576,76 @@ where txt0 = Text.toStrict (Dhall.Core.pretty expr0) +prettyTypeMessage MissingListType = do+ ErrorMessages {..}+ where+ short = "Empty lists need a type annotation"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Lists do not require a type annotation if they have at least one+element:+++ ┌───────────┐+ │ [1, 2, 3] │ The compiler can infer that this list has type ❰List Integer❱+ └───────────┘+++However, empty lists still require a type annotation:+++ ┌───────────────────┐+ │ [] : List Integer │ This type annotation is mandatory+ └───────────────────┘+++You cannot supply an empty list without a type annotation+|]++prettyTypeMessage (MismatchedListElements i expr0 expr1 expr2) =+ ErrorMessages {..}+ where+ short = "List elements should have the same type"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every element in a list must have the same type++For example, this is a valid ❰List❱:+++ ┌───────────┐+ │ [1, 2, 3] │ Every element in this ❰List❱ is an ❰Integer❱+ └───────────┘+++.. but this is $_NOT a valid ❰List❱:+++ ┌───────────────┐+ │ [1, "ABC", 3] │ The first and second element have different types+ └───────────────┘+++Your first ❰List❱ elements has this type:++↳ $txt0++... but the following element at index $txt1:++↳ $txt2++... has this type instead:++↳ $txt3+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty i )+ txt2 = Text.toStrict (Dhall.Core.pretty expr1)+ txt3 = Text.toStrict (Dhall.Core.pretty expr2)+ prettyTypeMessage (InvalidListElement i expr0 expr1 expr2) = ErrorMessages {..} where@@ -2597,9 +2686,9 @@ ● You might have thought that ❰++❱ was the operator to combine two lists: - ┌───────────────────────────────────────────────────────────┐- │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │ Not valid- └───────────────────────────────────────────────────────────┘+ ┌────────────────────────┐+ │ [1, 2, 3] ++ [4, 5, 6] │ Not valid+ └────────────────────────┘ The Dhall programming language does not provide a built-in operator for combining two lists