diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,24 @@ +Copyright (c) 2016 Gabriel Gonzalez +All rights reserved. + +Redistribution and use in source and binary forms, with or without modification, +are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + * Neither the name of Gabriel Gonzalez nor the names of other contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR +ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON +ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/dhall.cabal b/dhall.cabal new file mode 100644 --- /dev/null +++ b/dhall.cabal @@ -0,0 +1,74 @@ +Name: dhall +Version: 1.0.0 +Cabal-Version: >=1.8.0.2 +Build-Type: Simple +Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2, GHC == 8.0.1 +License: BSD3 +License-File: LICENSE +Copyright: 2016 Gabriel Gonzalez +Author: Gabriel Gonzalez +Maintainer: Gabriel439@gmail.com +Bug-Reports: https://github.com/Gabriel439/Haskell-Dhall-Library/issues +Synopsis: A configuration language guaranteed to terminate +Description: + Dhall is an explicitly typed configuration language that is not Turing + complete. Despite being Turing incomplete, Dhall is a real programming + language with a type-checker and evaluator. + . + Use this library to parse, type-check, evaluate, and pretty-print the Dhall + configuration language. This package also includes an executable which + type-checks a Dhall file and reduces the file to a fully evaluated normal + form. + . + "Dhall.Core" contains the core syntax tree and evaluator + . + "Dhall.Import" contains logic for resolving remote file and URL references + . + "Dhall.TypeChecker" contains the type-checker + . + "Dhall.Parser" contains the parser + . + Read "Dhall.Tutorial" to learn how to use this library +Category: Compiler +Source-Repository head + Type: git + Location: https://github.com/Gabriel439/Haskell-Dhall-Library + +Library + Hs-Source-Dirs: src + Build-Depends: + base >= 4 && < 5 , + ansi-wl-pprint < 0.7 , + bytestring < 0.11, + containers >= 0.5.0.0 && < 0.6 , + http-client >= 0.4.0 && < 0.5 , + http-client-tls >= 0.2.0 && < 0.3 , + microlens >= 0.2.0.0 && < 0.5 , + microlens-mtl >= 0.1.3.1 && < 0.2 , + neat-interpolation >= 0.3.2.1 && < 0.4 , + parsers >= 0.12.4 && < 0.13, + system-filepath >= 0.3.1 && < 0.5 , + system-fileio >= 0.2.1 && < 0.4 , + text >= 0.11.1.0 && < 1.3 , + text-format < 0.4 , + transformers >= 0.2.0.0 && < 0.6 , + trifecta >= 1.6 && < 1.7 , + unordered-containers >= 0.1.3.0 && < 0.3 , + vector >= 0.11.0.0 && < 0.12 + Exposed-Modules: + Dhall, + Dhall.Context, + Dhall.Core, + Dhall.Import, + Dhall.Parser, + Dhall.TypeCheck + +Executable dhall + Hs-Source-Dirs: exec + Main-Is: Main.hs + Build-Depends: + base >= 4 && < 5 , + dhall , + optparse-generic >= 1.1.1 && < 1.2, + trifecta >= 1.6 && < 1.7, + text >= 0.11.1.0 && < 1.3 diff --git a/exec/Main.hs b/exec/Main.hs new file mode 100644 --- /dev/null +++ b/exec/Main.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeOperators #-} + +module Main where + +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) +import Dhall.TypeCheck (DetailedTypeError(..), TypeError) +import Options.Generic (Generic, ParseRecord, type ()(..)) +import System.IO (stderr) +import System.Exit (exitFailure) +import Text.Trifecta.Delta (Delta(..)) + +import qualified Control.Exception +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 + +data Options = Options + { explain :: Bool "Explain error messages in more detail" + } deriving (Generic) + +instance ParseRecord Options + +main :: IO () +main = do + options <- Options.Generic.getRecord "Compiler for the Dhall language" + + let handle = + Control.Exception.handle handler2 + . Control.Exception.handle handler1 + . Control.Exception.handle handler0 + where + handler0 e = do + let _ = e :: TypeError Src + System.IO.hPutStrLn stderr "" + if unHelpful (explain options) + then Control.Exception.throwIO (DetailedTypeError e) + else do + Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" + Control.Exception.throwIO e + + handler1 (Imported ps e) = do + let _ = e :: TypeError Src + System.IO.hPutStrLn stderr "" + if unHelpful (explain options) + then Control.Exception.throwIO (Imported ps (DetailedTypeError e)) + else do + Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" + Control.Exception.throwIO (Imported ps e) + + handler2 e = do + let _ = e :: SomeException + System.IO.hPutStrLn stderr "" + System.IO.hPrint stderr e + System.Exit.exitFailure + + handle (do + inText <- Data.Text.Lazy.IO.getContents + + expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + + expr' <- load Nothing expr + + typeExpr <- case Dhall.TypeCheck.typeOf expr' of + Left err -> Control.Exception.throwIO err + Right typeExpr -> return typeExpr + Data.Text.Lazy.IO.hPutStrLn stderr (pretty (normalize typeExpr)) + Data.Text.Lazy.IO.hPutStrLn stderr mempty + Data.Text.Lazy.IO.putStrLn (pretty (normalize expr')) ) diff --git a/src/Dhall.hs b/src/Dhall.hs new file mode 100644 --- /dev/null +++ b/src/Dhall.hs @@ -0,0 +1,618 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +-- | Dhall is a programming language specialized for configuration files. +-- +-- The simplest possible way to use Dhall is to ignore the programming language +-- features and use it as a strongly typed configuration format. For example, +-- suppose that you have the following configuration file: +-- +-- > $ cat config +-- > < Example = +-- > { foo = 1 +-- > , bar = [3.0, 4.0, 5.0] : List Double +-- > } +-- > > +-- +-- You can read the above configuration file into Haskell using the following +-- code: +-- +-- > $ cat example.hs +-- > {-# LANGUAGE DeriveGeneric #-} +-- > {-# LANGUAGE OverloadedStrings #-} +-- > +-- > import Dhall +-- > +-- > data Example = Example { foo :: Integer , bar :: Vector Double } +-- > deriving (Generic, Show) +-- > +-- > instance Interpret Example +-- > +-- > main :: IO () +-- > main = do +-- > x <- input auto "./config" +-- > print (x :: Example) +-- +-- If you compile and run the above program, the program prints the +-- corresponding Haskell record: +-- +-- > $ ./example +-- > Example {foo = 1, bar = [3.0,4.0,5.0]} +-- +-- In the above code, the @Example@ Haskell type represents the schema for our +-- configuration file. Suppose that we modify our configuration file to no +-- longer match the schema, like this: +-- +-- > $ echo "1" > config +-- +-- This then throws an exception when we try to load the configuration file: +-- +-- > $ ./example +-- > example: +-- > Expression: 1 : { bar : List Double, foo : Integer } +-- > +-- > Error: Expression's inferred type does not match annotated type +-- > +-- > Explanation: You can annotate the type or kind of an expression like this: +-- > +-- > x : t -- `x` is the expression and `t` is the annotated type or kind of `x` +-- > +-- > Annotations are introduced in one of two ways: +-- > +-- > * You can manually annotate expressions to declare the type or kind you expect +-- > * The interpreter also implicitly inserts a top-level type annotation +-- > +-- > Annotations are optional because the compiler can infer the type of all +-- > expressions. However, if you or the interpreter inserts an annotation and the +-- > inferred type or kind does not match the annotation then type-checking fails. +-- > +-- > You or the interpreter annotated this expression: +-- > ↳ 1 +-- > ... with this type or kind: +-- > ↳ { bar : List Double, foo : Integer } +-- > ... but the inferred type of the expression is actually this type or kind: +-- > ↳ Integer +-- +-- The Dhall programming language is a statically typed language and the +-- above error message is the output of the language's type-checker. Every +-- expression we read into Haskell is type-checked against the expected schema. +-- +-- The above error message says that the type-checker expected a record with +-- two fields: a field named @bar@ that is a `Vector` of `Double`s, and a +-- field named @foo@ that is an `Integer`. However, the type-checker found an +-- expression whose inferred type was an `Integer`. Since an `Integer` is not +-- the same thing as a record the type-checking step fails and Dhall does not +-- bother to marshal the configuration into Haskell. +-- +-- Dhall is also a heavily restricted programming language. For example, we can +-- define a configuration file that is an anonymous function: +-- +-- > $ cat > makeBools +-- > \(n : Bool) -> +-- > [ n && True, n && False, n || True, n || False ] : List Bool +-- > +-- +-- You can read this as a function of one argument named @n@ of type `Bool` +-- that returns a `Vector` of `Bool`s. Each element of the `Vector` depends +-- on the input argument. +-- +-- This library comes with a command-line compiler named @dhall@ that you can +-- use to type-check configuration files and convert them to a normal form. For +-- example, we can ask the compiler what the type of our @makeBools@ file +-- is: +-- +-- > $ dhall typecheck < makeBools +-- > ∀(n : Bool) → List Bool +-- +-- This says that @makeBools@ is a function of one argument named @n@ of type +-- `Bool` that returns a `Vector` of `Bool`s. +-- +-- We can apply our file to a `Bool` argument as if it were an ordinary +-- function, like this: +-- +-- > {-# LANGUAGE OverloadedStrings #-} +-- > +-- > import Dhall +-- > +-- > main :: IO () +-- > main = do +-- > x <- input auto "./makeBools True" +-- > print (x :: Vector Bool) +-- +-- This produces the following output: +-- +-- > $ ./example +-- > [True,False,True,True] +-- +-- Notice how we can decode into some types \"out-of-the-box\" without declaring +-- a Haskell record to store the output. In the above example we marshalled +-- the result directly into a `Vector` of `Bool`s. The instances for the +-- `Interpret` class list all types that are automatically supported. +-- +-- We can also test functions directly on the command line using the @dhall@ +-- compiler. For example: +-- +-- > $ dhall +-- > ./makeBools False +-- > +-- > List Bool +-- > +-- > [False, False, True, False] : List Bool +-- +-- The @dhall@ compiler with no arguments produces two output lines: +-- +-- * The first output line is the type of the result +-- * The second output line is the normal form of the expression that we input +-- +-- In the above example the type of the result is a `Vector` of `Bool`s and the +-- normal form of the expression just evaluates all functions. +-- +-- You can also use the Dhall compiler to evaluate expressions which have no +-- file references. For example: +-- +-- > $ dhall +-- > "Hello, " <> "world!" +-- > +-- > Text +-- > +-- > "Hello, world!" +-- +-- > $ dhall +-- > +10 * +10 +-- > Natural +-- > +-- > +100 +-- +-- Dhall is a very restricted programming language that only supports simple +-- operations. For example, Dhall only support addition and subtraction on +-- `Natural` numbers (i.e. non-negative numbers), which are not the same type of +-- number as `Integer`s (which can be negative). A `Natural` number is a number +-- prefixed with the @+@ symbol. If you try to add or multiply two `Integer`s +-- (without the @+@ prefix) you will get a type error: +-- +-- > $ dhall +-- > 2 + 2 +-- > +-- > dhall: +-- > Expression: 2 + 2 +-- > +-- > Error: Cannot use `(+)` on a value that's not a `Natural` +-- > +-- > Explanation: The `(+)` operator expects two arguments of type `Natural` +-- > +-- > You provided this argument: +-- > +-- > 2 + ... +-- > +-- > ... whose type is not `Natural`. The type is actually: +-- > ↳ Integer +-- > +-- > An `Integer` is not the same thing as a `Natural` number. They are distinct +-- > types: `Integer`s can be negative, but `Natural` numbers must be non-negative +-- > +-- > You can prefix an `Integer` literal with a `+` to create a `Natural` literal +-- > +-- > Example: +-- > +-- > +2 + ... +-- +-- The Dhall language doesn't just type-check the final schema; the language +-- also ensures that every expression is internally consistent. For example, +-- suppose that we call @./makeBools@ on a non-`Bool` argument: +-- +-- +-- > $ dhall +-- > ./makeBools "ABC" +-- > dhall: +-- > Expression: (λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool) "ABC" +-- > +-- > Error: Function applied to the wrong type or kind of argument +-- > +-- > Explanation: Every function declares what type or kind of argument to accept +-- > +-- > λ(x : Bool) → x -- Anonymous function which only accepts `Bool` arguments +-- > +-- > let f (x : Bool) = x -- Named function which only accepts `Bool` arguments +-- > in f True +-- > +-- > λ(a : Type) → a -- Anonymous function which only accepts `Type` arguments +-- > +-- > You *cannot* apply a function to the wrong type or kind of argument: +-- > +-- > (λ(x : Bool) → x) "A" -- "A" is `Text`, but the function expects a `Bool` +-- > +-- > You tried to invoke a function which expects an argument of type or kind: +-- > ↳ Bool +-- > ... on an argument of type or kind: +-- > ↳ Text +-- +-- We get a type error saying that our function expects a `Bool` argument, but +-- we supplied an argument of type `Text` instead. +-- +-- Our `input` function also doesn't need to reference any files at all: +-- +-- >>> input auto "True && False" :: IO Bool +-- False +-- +-- Reading from an external configuration file is just a special case of Dhall's +-- support for embedding files as expressions. There's no limit to how many +-- files-as-expressions that you can nest this way. For example, we can define +-- one file that is a Dhall expression that in turn depends on another file +-- which is also a Dhall expression: +-- +-- > $ echo './bool1 && ./bool2' > both +-- > $ echo 'True' > bool1 +-- > $ echo 'False' > bool2 +-- > $ dhall +-- > [ ./bool1 , ./bool2 , ./both ] : List Bool +-- > +-- > List Bool +-- > +-- > [ True, False, False ] : List Bool +-- +-- The only restriction is that the Dhall language will forbid cycles in these +-- file references: +-- +-- > $ echo './bar' > foo +-- > $ echo './foo' > bar +-- > $ dhall < ./foo +-- > dhall: +-- > ⤷ ./bar +-- > ⤷ ./foo +-- > Cyclic import: ./bar +-- +-- Dhall is a total programming language, which means that Dhall is not +-- Turing-complete and evaluation of every Dhall program is guaranteed to +-- eventually halt. There is no upper bound on how long the program might take +-- to evaluate, but the program is guaranteed to terminate in a finite amount of +-- time and not hang forever. +-- +-- This guarantees that all Dhall programs can be safely reduced to a normal +-- form where all functions have been evaluated. In fact, Dhall expressions can +-- be evaluated even if all function arguments haven't been fully applied. For +-- example, the following program is an anonymous function: +-- +-- > $ dhall +-- > \(n : Bool) -> +10 * +10 +-- > +-- > ∀(n : Bool) → Natural +-- > +-- > λ(n : Bool) → +100 +-- +-- ... and even though the function is still missing the first argument named +-- @n@ the compiler is smart enough to evaluate the body of the anonymous +-- function ahead of time before the function has even been invoked. +-- +-- Similarly, you can use this normalization process to remove indirection +-- introduced by well-meaning software engineers over-architecting the +-- configuration file. + +module Dhall + ( + -- * Input + input + + -- * Types + , Type + , Interpret(..) + , bool + , natural + , integer + , double + , text + , maybe + , vector + + -- * Re-exports + , Text + , Vector + , Generic + ) where + +import Control.Applicative (empty, liftA2, (<|>)) +import Control.Exception (Exception) +import Data.Monoid ((<>)) +import Data.Text.Lazy (Text) +import Data.Vector (Vector) +import Dhall.Core (Expr(..)) +import Dhall.Parser (Src(..)) +import Dhall.TypeCheck (X) +import GHC.Generics +import Numeric.Natural (Natural) +import Prelude hiding (maybe) +import Text.Trifecta.Delta (Delta(..)) + +import qualified Control.Exception +import qualified Data.ByteString.Lazy +import qualified Data.Map +import qualified Data.Text.Lazy +import qualified Data.Text.Lazy.Builder +import qualified Data.Text.Lazy.Encoding +import qualified Data.Vector +import qualified Dhall.Core +import qualified Dhall.Import +import qualified Dhall.Parser +import qualified Dhall.TypeCheck +import qualified GHC.Generics + +throws :: Exception e => Either e a -> IO a +throws (Left e) = Control.Exception.throwIO e +throws (Right r) = return r + +{-| 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" +[1.0,2.0] + + Use `auto` to automatically select which type to decode based on the + inferred return type: + +>>> input auto "True" :: IO Bool +True +-} +input + :: Type a + -- ^ The type of value to decode from Dhall to Haskell + -> Text + -- ^ The Dhall program + -> IO a + -- ^ The decoded value in Haskell +input (Type {..}) text = do + let delta = Directed "(input)" 0 0 0 0 + expr <- throws (Dhall.Parser.exprFromText delta text) + expr' <- Dhall.Import.load Nothing expr + let suffix = + ( Data.ByteString.Lazy.toStrict + . Data.Text.Lazy.Encoding.encodeUtf8 + . Data.Text.Lazy.Builder.toLazyText + . Dhall.Core.buildExpr0 + ) expected + let annot = case expr' of + Note (Src begin end bytes) _ -> + Note (Src begin end bytes') (Annot expr' expected) + where + bytes' = bytes <> " : " <> suffix + _ -> + Annot expr' expected + typeExpr <- throws (Dhall.TypeCheck.typeOf annot) + case extract (Dhall.Core.normalize expr') of + Just x -> return x + Nothing -> fail "input: malformed `Type`" + +{-| A @(Type a)@ represents a way to marshal a value of type @\'a\'@ from Dhall + into Haskell + + You can produce `Type`s either explicitly: + +> example :: Type (Vector Text) +> example = vector text + + ... or implicitly using `auto`: + +> example :: Type (Vector Text) +> example = auto + + You can consume `Type`s using the `input` function: + +> input :: Type a -> Text -> IO a +-} +data Type a = Type + { extract :: Expr X X -> Maybe a + , expected :: Expr Src X + } + deriving (Functor) + +{-| Decode a `Bool` + +>>> input bool "True" +True +-} +bool :: Type Bool +bool = Type {..} + where + extract (BoolLit b) = pure b + extract _ = Nothing + + expected = Bool + +{-| Decode a `Natural` + +>>> input natural "+42" +42 +-} +natural :: Type Natural +natural = Type {..} + where + extract (NaturalLit n) = pure n + extract _ = empty + + expected = Natural + +{-| Decode an `Integer` + +>>> input integer "42" +42 +-} +integer :: Type Integer +integer = Type {..} + where + extract (IntegerLit n) = pure n + extract _ = empty + + expected = Integer + +{-| Decode a `Double` + +>>> input double "42.0" +42.0 +-} +double :: Type Double +double = Type {..} + where + extract (DoubleLit n) = pure n + extract _ = empty + + expected = Double + +{-| Decode `Text` + +>>> input text "\"Test\"" +"Test" +-} +text :: Type Text +text = Type {..} + where + extract (TextLit t) = pure (Data.Text.Lazy.Builder.toLazyText t) + extract _ = empty + + expected = Text + +{-| Decode a `Maybe` + +>>> input (maybe integer) "[] : Maybe Integer" +Nothing +-} +maybe :: Type a -> Type (Maybe a) +maybe (Type extractIn expectedIn) = Type extractOut expectedOut + where + extractOut (OptionalLit _ es) = traverse extractIn es' + where + es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es) + + expectedOut = App Optional expectedIn + +{-| Decode a `Vector` + +>>> input (vector integer) "[ 1, 2, 3 ] : List Integer" +[1,2,3] +-} +vector :: Type a -> Type (Vector a) +vector (Type extractIn expectedIn) = Type extractOut expectedOut + where + extractOut (ListLit _ es) = traverse extractIn es + + 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) +[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. +-} +class Interpret a where + auto :: Type a + default auto :: (Generic a, GenericInterpret (Rep a)) => Type a + auto = fmap GHC.Generics.to genericAuto + +instance Interpret Bool where + auto = bool + +instance Interpret Natural where + auto = natural + +instance Interpret Integer where + auto = integer + +instance Interpret Double where + auto = double + +instance Interpret Text where + auto = text + +instance Interpret a => Interpret (Maybe a) where + auto = maybe auto + +instance Interpret a => Interpret (Vector a) where + auto = vector auto + +class GenericInterpret f where + genericAuto :: Type (f a) + +instance GenericInterpret f => GenericInterpret (M1 D d f) where + genericAuto = fmap M1 genericAuto + +instance GenericInterpret V1 where + genericAuto = Type {..} + where + extract _ = Nothing + + expected = Union Data.Map.empty + +instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :+: g) where + genericAuto = Type {..} + where + extract e = fmap L1 (extractL e) <|> fmap R1 (extractR e) + + expected = Union (Data.Map.union expectedL expectedR) + + Type extractL (Union expectedL) = genericAuto + Type extractR (Union expectedR) = genericAuto + +instance (Constructor c, GenericInterpret f) => GenericInterpret (M1 C c f) where + genericAuto = Type {..} + where + n :: M1 i c f a + n = undefined + + name = Data.Text.Lazy.pack (conName n) + + extract (UnionLit name' e _) + | name == name' = fmap M1 (extract' e) + | otherwise = Nothing + + expected = Union (Data.Map.singleton name expected') + + Type extract' expected' = genericAuto + +instance GenericInterpret U1 where + genericAuto = Type {..} + where + extract _ = Just U1 + + expected = Record (Data.Map.fromList []) + +instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :*: g) where + genericAuto = Type {..} + where + extract = liftA2 (liftA2 (:*:)) extractL extractR + + expected = Record (Data.Map.union ktsL ktsR) + where + Record ktsL = expectedL + Record ktsR = expectedR + Type extractL expectedL = genericAuto + Type extractR expectedR = genericAuto + +instance (Selector s, Interpret a) => GenericInterpret (M1 S s (K1 i a)) where + genericAuto = Type {..} + where + n :: M1 i s f a + n = undefined + + extract (RecordLit m) = do + case selName n of + "" -> Nothing + name -> do + e <- Data.Map.lookup (Data.Text.Lazy.pack name) m + fmap (M1 . K1) (extract' e) + extract _ = Nothing + + expected = Record (Data.Map.fromList [(key, expected')]) + where + key = Data.Text.Lazy.pack (selName n) + + Type extract' expected' = auto diff --git a/src/Dhall/Context.hs b/src/Dhall/Context.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Context.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE DeriveFunctor #-} + +-- | All `Context`-related operations + +module Dhall.Context ( + -- * Context + Context + , empty + , insert + , lookup + , toList + ) where + +import Data.Text.Lazy (Text) +import Prelude hiding (lookup) + +{-| A @(Context a)@ associates `Text` labels with values of type @a@ + + The `Context` is used for type-checking when @(a = Expr X)@ + + * You create a `Context` using `empty` and `insert` + * 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 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) + +-- | An empty context with no key-value pairs +empty :: Context a +empty = Context [] + +-- | Add a key-value pair to the `Context` +insert :: Text -> a -> Context a -> Context a +insert k v (Context kvs) = Context ((k, v) : kvs) +{-# INLINABLE insert #-} + +{-| Look up a key by name and index + +> 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 j v c) = lookup k n c -- k /= j +-} +lookup :: Text -> Integer -> Context a -> Maybe a +lookup _ !_ (Context [] ) = + Nothing +lookup x !n (Context ((k, v):kvs)) = + if x == k + then if n == 0 + then Just v + else lookup x (n - 1) (Context kvs) + else lookup x n (Context kvs) +{-# INLINABLE lookup #-} + +{-| Return all key-value associations as a list + +> toList empty = [] +> toList (insert k v ctx) = (k, v) : toList ctx +-} +toList :: Context a -> [(Text, a)] +toList = getContext +{-# INLINABLE toList #-} diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Core.hs @@ -0,0 +1,1321 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE RankNTypes #-} +{-# OPTIONS_GHC -Wall #-} + +-- | This module contains the core calculus for the Dhall language. + +module Dhall.Core ( + -- * Syntax + Const(..) + , Path(..) + , Var(..) + , Expr(..) + + -- * Normalization + , normalize + , subst + , shift + + -- * Builders + -- $builders + , pretty + , buildExpr0 + , buildExpr1 + , buildExpr2 + , buildExpr3 + , buildExpr4 + , buildExpr5 + , buildExpr6 + , buildConst + , buildVar + , buildElems + , buildRecordLit + , buildFieldValues + , buildFieldValue + , buildRecord + , buildFieldTypes + , buildFieldType + , buildUnion + , buildAlternativeTypes + , buildAlternativeType + , buildUnionLit + + -- * Miscellaneous + , internalError + ) where + +#if MIN_VERSION_base(4,8,0) +#else +import Control.Applicative (Applicative(..), (<$>)) +#endif +import Data.Bifunctor (Bifunctor(..)) +import Data.Foldable +import Data.Map (Map) +import Data.Monoid ((<>)) +import Data.String (IsString(..)) +import Data.Text.Buildable (Buildable(..)) +import Data.Text.Lazy (Text) +import Data.Text.Lazy.Builder (Builder) +import Data.Traversable +import Data.Vector (Vector) +import Filesystem.Path.CurrentOS (FilePath) +import Numeric.Natural (Natural) +import Prelude hiding (FilePath) + +import qualified Control.Monad +import qualified Data.Map +import qualified Data.Maybe +import qualified Data.Text +import qualified Data.Text.Lazy as Text +import qualified Data.Text.Lazy.Builder as Builder +import qualified Data.Vector +import qualified Data.Vector.Mutable +import qualified Filesystem.Path.CurrentOS as Filesystem +import qualified NeatInterpolation + +{-| Constants for a pure type system + + The only axiom is: + +> ⊦ Type : Kind + + ... and the valid rule pairs are: + +> ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions) +> ⊦ Kind ↝ Type : Type -- Functions from types to terms (polymorphic functions) +> ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type constructors) + + These are the same rule pairs as System Fω + + Note that Dhall does not support functions from terms to types and therefore + Dhall is not a dependently typed language +-} +data Const = Type | Kind deriving (Show, Bounded, Enum) + +instance Buildable Const where + build = buildConst + +-- | Path to an external resource +data Path + = File FilePath + | URL Text + deriving (Eq, Ord, Show) + +instance Buildable Path where + build (File file) + | Text.isPrefixOf "./" txt + || Text.isPrefixOf "/" txt + || Text.isPrefixOf "../" txt + = build txt <> " " + | otherwise + = "./" <> build txt <> " " + where + txt = Text.fromStrict (either id id (Filesystem.toText file)) + build (URL str ) = build str <> " " + +{-| Label for a bound variable + + The `Text` field is the variable's name (i.e. \"@x@\"). + + The `Int` field disambiguates variables with the same name if there are + multiple bound variables of the same name in scope. Zero refers to the + 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 : *) -> \(y : *) -> \(x : *) -> x@0 +> +> +-------------refers to-------------+ +> | | +> v | +> \(x : *) -> \(y : *) -> \(x : *) -> 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 + + Zero indices are omitted when pretty-printing `Var`s and non-zero indices + appear as a numeric suffix. +-} +data Var = V Text !Integer + deriving (Eq, Show) + +instance IsString Var where + fromString str = V (fromString str) 0 + +instance Buildable Var where + build = buildVar + +-- | Syntax tree for expressions +data Expr s a + -- | > Const c ~ c + = Const Const + -- | > Var (V x 0) ~ x + -- > Var (V x n) ~ x@n + | Var Var + -- | > Lam x A b ~ λ(x : A) -> b + | Lam Text (Expr s a) (Expr s a) + -- | > Pi "_" A B ~ A -> B + -- > Pi x A B ~ ∀(x : A) -> B + | 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 Text (Maybe (Expr s a)) (Expr s a) (Expr s a) + -- | > Annot x t ~ x : t + | Annot (Expr s a) (Expr s a) + -- | > Bool ~ Bool + | Bool + -- | > BoolLit b ~ b + | BoolLit Bool + -- | > BoolAnd x y ~ x && y + | BoolAnd (Expr s a) (Expr s a) + -- | > BoolOr x y ~ x || y + | BoolOr (Expr s a) (Expr s a) + -- | > BoolEQ x y ~ x == y + | BoolEQ (Expr s a) (Expr s a) + -- | > BoolNE x y ~ x /= y + | BoolNE (Expr s a) (Expr s a) + -- | > BoolIf x y z ~ if x then y else z + | BoolIf (Expr s a) (Expr s a) (Expr s a) + -- | > Natural ~ Natural + | Natural + -- | > NaturalLit n ~ +n + | NaturalLit Natural + -- | > NaturalFold ~ Natural/fold + | NaturalFold + -- | > NaturalBuild ~ Natural/build + | NaturalBuild + -- | > NaturalIsZero ~ Natural/isZero + | NaturalIsZero + -- | > NaturalEven ~ Natural/even + | NaturalEven + -- | > NaturalOdd ~ Natural/odd + | NaturalOdd + -- | > NaturalPlus x y ~ x + y + | NaturalPlus (Expr s a) (Expr s a) + -- | > NaturalTimes x y ~ x * y + | NaturalTimes (Expr s a) (Expr s a) + -- | > Integer ~ Integer + | Integer + -- | > IntegerLit n ~ n + | IntegerLit Integer + -- | > Double ~ Double + | Double + -- | > DoubleLit n ~ n + | DoubleLit Double + -- | > Text ~ Text + | Text + -- | > TextLit t ~ t + | TextLit Builder + -- | > TextAppend x y ~ x ++ y + | 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)) + -- | > ListBuild ~ List/build + | ListBuild + -- | > ListFold ~ List/fold + | ListFold + -- | > ListLength ~ List/length + | ListLength + -- | > ListHead ~ List/head + | ListHead + -- | > ListLast ~ List/last + | ListLast + -- | > ListIndexed ~ List/indexed + | ListIndexed + -- | > ListReverse ~ List/reverse + | ListReverse + -- | > Optional ~ Optional + | Optional + -- | > OptionalLit t [e] ~ [e] : Optional t + -- > OptionalLit t [] ~ [] : Optional t + | OptionalLit (Expr s a) (Vector (Expr s a)) + -- | > OptionalFold ~ Optional/fold + | OptionalFold + -- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 } + | 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 (Map Text (Expr s a)) + -- | > 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) + -- | > Merge x y t ~ merge x y : t + | Merge (Expr s a) (Expr s a) (Expr s a) + -- | > Field e x ~ e.x + | Field (Expr s a) Text + -- | > Note s x ~ e + | Note s (Expr s a) + -- | > Embed path ~ path + | Embed a + deriving (Functor, Foldable, Traversable, Show) + +instance Applicative (Expr s) where + pure = Embed + + (<*>) = Control.Monad.ap + +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 + +instance Bifunctor Expr where + first _ (Const a ) = Const a + first _ (Var a ) = Var a + first k (Lam a b c ) = Lam a (first k b) (first k c) + first k (Pi a b c ) = Pi a (first k b) (first k c) + first k (App a b ) = App (first k a) (first k b) + first k (Let a b c d ) = Let a (fmap (first k) b) (first k c) (first k d) + first k (Annot a b ) = Annot (first k a) (first k b) + first _ Bool = Bool + first _ (BoolLit a ) = BoolLit a + first k (BoolAnd a b ) = BoolAnd (first k a) (first k b) + first k (BoolOr a b ) = BoolOr (first k a) (first k b) + first k (BoolEQ a b ) = BoolEQ (first k a) (first k b) + first k (BoolNE a b ) = BoolNE (first k a) (first k b) + first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c) + first _ Natural = Natural + first _ (NaturalLit a ) = NaturalLit a + first _ NaturalFold = NaturalFold + first _ NaturalBuild = NaturalBuild + first _ NaturalIsZero = NaturalIsZero + first _ NaturalEven = NaturalEven + first _ NaturalOdd = NaturalOdd + first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b) + first k (NaturalTimes a b) = NaturalTimes (first k a) (first k b) + first _ Integer = Integer + first _ (IntegerLit a ) = IntegerLit a + first _ Double = Double + first _ (DoubleLit a ) = DoubleLit a + first _ Text = Text + 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 _ ListBuild = ListBuild + first _ ListFold = ListFold + first _ ListLength = ListLength + first _ ListHead = ListHead + first _ ListLast = ListLast + first _ ListIndexed = ListIndexed + first _ ListReverse = ListReverse + first _ Optional = Optional + first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b) + first _ OptionalFold = OptionalFold + first k (Record a ) = Record (fmap (first k) a) + first k (RecordLit a ) = RecordLit (fmap (first k) a) + first k (Union a ) = Union (fmap (first k) a) + first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c) + first k (Combine a b ) = Combine (first k a) (first k b) + first k (Merge a b c ) = Merge (first k a) (first k b) (first k c) + 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 + + second = fmap + +instance IsString (Expr s a) + where + fromString str = Var (fromString str) + +{- $builders + There is a one-to-one correspondence between the builders in this section + and the sub-parsers in "Dhall.Parser". Each builder is named after the + corresponding parser and the relationship between builders exactly matches + the relationship between parsers. This leads to the nice emergent property + of automatically getting all the parentheses and precedences right. + + This approach has one major disadvantage: you can get an infinite loop if + you add a new constructor to the syntax tree without adding a matching + case the corresponding builder. +-} + +-- | Pretty-print a value +pretty :: Buildable a => a -> Text +pretty = Builder.toLazyText . build + +-- | Builder corresponding to the @label@ token in "Dhall.Parser" +buildLabel :: Text -> Builder +buildLabel = build + +-- | Builder corresponding to the @number@ token in "Dhall.Parser" +buildNumber :: Integer -> Builder +buildNumber a = build (show a) + +-- | Builder corresponding to the @natural@ token in "Dhall.Parser" +buildNatural :: Natural -> Builder +buildNatural a = build (show a) + +-- | Builder corresponding to the @double@ token in "Dhall.Parser" +buildDouble :: Double -> Builder +buildDouble a = build (show a) + +-- | Builder corresponding to the @text@ token in "Dhall.Parser" +buildText :: Builder -> Builder +buildText a = build (show a) + +-- | Builder corresponding to the @Expr0@ parser in "Dhall.Parser" +buildExpr0 :: Buildable a => Expr s a -> Builder +buildExpr0 (Annot a b) = buildExpr1 a <> " : " <> buildExpr0 b +buildExpr0 (Note _ b) = buildExpr0 b +buildExpr0 a = buildExpr1 a + +-- | Builder corresponding to the @Expr1@ parser in "Dhall.Parser" +buildExpr1 :: Buildable a => Expr s a -> Builder +buildExpr1 (Lam a b c) = + "λ(" + <> buildLabel a + <> " : " + <> buildExpr0 b + <> ") → " + <> buildExpr1 c +buildExpr1 (BoolIf a b c) = + "if " + <> buildExpr0 a + <> " then " + <> buildExpr1 b + <> " else " + <> buildExpr1 c +buildExpr1 (Pi "_" b c) = + buildExpr2 b + <> " → " + <> buildExpr1 c +buildExpr1 (Pi a b c) = + "∀(" + <> buildLabel a + <> " : " + <> buildExpr0 b + <> ") → " + <> buildExpr1 c +buildExpr1 (Let a Nothing c d) = + "let " + <> buildLabel a + <> " = " + <> buildExpr0 c + <> " in " + <> buildExpr1 d +buildExpr1 (Let a (Just b) c d) = + "let " + <> buildLabel a + <> " : " + <> buildExpr0 b + <> " = " + <> buildExpr0 c + <> " in " + <> buildExpr1 d +buildExpr1 (ListLit a b) = + "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExpr6 a +buildExpr1 (OptionalLit a b) = + "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExpr6 a +buildExpr1 (Merge a b c) = + "merge " <> buildExpr6 a <> " " <> buildExpr6 b <> " : " <> buildExpr5 c +buildExpr1 (Note _ b) = + buildExpr1 b +buildExpr1 a = + buildExpr2 a + +-- | Builder corresponding to the @Expr2@ parser in "Dhall.Parser" +buildExpr2 :: Buildable a => Expr s a -> Builder +buildExpr2 (BoolEQ a b) = buildExpr2 a <> " == " <> buildExpr2 b +buildExpr2 (BoolNE a b) = buildExpr2 a <> " /= " <> buildExpr2 b +buildExpr2 (Note _ b) = buildExpr2 b +buildExpr2 a = buildExpr3 a + +-- | Builder corresponding to the @Expr3@ parser in "Dhall.Parser" +buildExpr3 :: Buildable a => Expr s a -> Builder +buildExpr3 (BoolOr a b) = buildExpr3 a <> " || " <> buildExpr3 b +buildExpr3 (NaturalPlus a b) = buildExpr3 a <> " + " <> buildExpr3 b +buildExpr3 (TextAppend a b) = buildExpr3 a <> " ++ " <> buildExpr3 b +buildExpr3 (Note _ b) = buildExpr3 b +buildExpr3 a = buildExpr4 a + +-- | Builder corresponding to the @Expr4@ parser in "Dhall.Parser" +buildExpr4 :: Buildable a => Expr s a -> Builder +buildExpr4 (BoolAnd a b) = buildExpr4 a <> " && " <> buildExpr4 b +buildExpr4 (NaturalTimes a b) = buildExpr4 a <> " * " <> buildExpr4 b +buildExpr4 (Combine a b) = buildExpr4 a <> " ∧ " <> buildExpr4 b +buildExpr4 (Note _ b) = buildExpr4 b +buildExpr4 a = buildExpr5 a + +-- | Builder corresponding to the @Expr5@ parser in "Dhall.Parser" +buildExpr5 :: Buildable a => Expr s a -> Builder +buildExpr5 (App a b) = buildExpr5 a <> " " <> buildExpr6 b +buildExpr5 (Note _ b) = buildExpr5 b +buildExpr5 a = buildExpr6 a + +-- | Builder corresponding to the @Expr6@ parser in "Dhall.Parser" +buildExpr6 :: Buildable a => Expr s a -> Builder +buildExpr6 (Var a) = + buildVar a +buildExpr6 (Const k) = + buildConst k +buildExpr6 Bool = + "Bool" +buildExpr6 Natural = + "Natural" +buildExpr6 NaturalFold = + "Natural/fold" +buildExpr6 NaturalBuild = + "Natural/build" +buildExpr6 NaturalIsZero = + "Natural/isZero" +buildExpr6 NaturalEven = + "Natural/even" +buildExpr6 NaturalOdd = + "Natural/odd" +buildExpr6 Integer = + "Integer" +buildExpr6 Double = + "Double" +buildExpr6 Text = + "Text" +buildExpr6 List = + "List" +buildExpr6 ListBuild = + "List/build" +buildExpr6 ListFold = + "List/fold" +buildExpr6 ListLength = + "List/length" +buildExpr6 ListHead = + "List/head" +buildExpr6 ListLast = + "List/last" +buildExpr6 ListIndexed = + "List/indexed" +buildExpr6 ListReverse = + "List/reverse" +buildExpr6 Optional = + "Optional" +buildExpr6 OptionalFold = + "Optional/fold" +buildExpr6 (BoolLit True) = + "True" +buildExpr6 (BoolLit False) = + "False" +buildExpr6 (IntegerLit a) = + buildNumber a +buildExpr6 (NaturalLit a) = + "+" <> buildNatural a +buildExpr6 (DoubleLit a) = + buildDouble a +buildExpr6 (TextLit a) = + buildText a +buildExpr6 (Record a) = + buildRecord a +buildExpr6 (RecordLit a) = + buildRecordLit a +buildExpr6 (Union a) = + buildUnion a +buildExpr6 (UnionLit a b c) = + buildUnionLit a b c +buildExpr6 (Embed a) = + build a +buildExpr6 (Field a b) = + buildExpr6 a <> "." <> buildLabel b +buildExpr6 (Note _ b) = + buildExpr6 b +buildExpr6 a = + "(" <> buildExpr0 a <> ")" + +-- | Builder corresponding to the @Const@ parser in "Dhall.Parser" +buildConst :: Const -> Builder +buildConst Type = "Type" +buildConst Kind = "Kind" + +-- | Builder corresponding to the @Var@ parser in "Dhall.Parser" +buildVar :: Var -> Builder +buildVar (V x 0) = buildLabel x +buildVar (V x n) = buildLabel x <> "@" <> buildNumber n + +-- | Builder corresponding to the @Elems@ parser in "Dhall.Parser" +buildElems :: Buildable a => [Expr s a] -> Builder +buildElems [] = "" +buildElems [a] = buildExpr0 a +buildElems (a:bs) = buildExpr0 a <> ", " <> buildElems bs + +-- | Builder corresponding to the @RecordLit@ parser in "Dhall.Parser" +buildRecordLit :: Buildable a => Map Text (Expr s a) -> Builder +buildRecordLit a | Data.Map.null a = + "{=}" +buildRecordLit a = + "{ " <> buildFieldValues (Data.Map.toList a) <> " }" + +-- | Builder corresponding to the @FieldValues@ parser in "Dhall.Parser" +buildFieldValues :: Buildable a => [(Text, Expr s a)] -> Builder +buildFieldValues [] = "" +buildFieldValues [a] = buildFieldValue a +buildFieldValues (a:bs) = buildFieldValue a <> ", " <> buildFieldValues bs + +-- | Builder corresponding to the @FieldValue@ parser in "Dhall.Parser" +buildFieldValue :: Buildable a => (Text, Expr s a) -> Builder +buildFieldValue (a, b) = buildLabel a <> " = " <> buildExpr0 b + +-- | Builder corresponding to the @Record@ parser in "Dhall.Parser" +buildRecord :: Buildable a => Map Text (Expr s a) -> Builder +buildRecord a | Data.Map.null a = + "{}" +buildRecord a = + "{ " <> buildFieldTypes (Data.Map.toList a) <> " }" + +-- | Builder corresponding to the @FieldTypes@ parser in "Dhall.Parser" +buildFieldTypes :: Buildable a => [(Text, Expr s a)] -> Builder +buildFieldTypes [] = "" +buildFieldTypes [a] = buildFieldType a +buildFieldTypes (a:bs) = buildFieldType a <> ", " <> buildFieldTypes bs + +-- | Builder corresponding to the @FieldType@ parser in "Dhall.Parser" +buildFieldType :: Buildable a => (Text, Expr s a) -> Builder +buildFieldType (a, b) = buildLabel a <> " : " <> buildExpr0 b + +-- | Builder corresponding to the @Union@ parser in "Dhall.Parser" +buildUnion :: Buildable a => Map Text (Expr s a) -> Builder +buildUnion a | Data.Map.null a = + "<>" +buildUnion a = + "< " <> buildAlternativeTypes (Data.Map.toList a) <> " >" + +-- | Builder corresponding to the @AlternativeTypes@ parser in "Dhall.Parser" +buildAlternativeTypes :: Buildable a => [(Text, Expr s a)] -> Builder +buildAlternativeTypes [] = + "" +buildAlternativeTypes [a] = + buildAlternativeType a +buildAlternativeTypes (a:bs) = + buildAlternativeType a <> " | " <> buildAlternativeTypes bs + +-- | Builder corresponding to the @AlternativeType@ parser in "Dhall.Parser" +buildAlternativeType :: Buildable a => (Text, Expr s a) -> Builder +buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExpr0 b + +-- | Builder corresponding to the @UnionLit@ parser in "Dhall.Parser" +buildUnionLit :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder +buildUnionLit a b c + | Data.Map.null c = + "< " + <> buildLabel a + <> " = " + <> buildExpr0 b + <> " >" + | otherwise = + "< " + <> buildLabel a + <> " = " + <> buildExpr0 b + <> " | " + <> buildAlternativeTypes (Data.Map.toList c) + <> " >" + +-- | Generates a syntactically valid Dhall program +instance Buildable a => Buildable (Expr s a) + where + build = buildExpr0 + +{-| `shift` is used by both normalization and type-checking to avoid variable + capture by shifting variable indices + + For example, suppose that you were to normalize the following expression: + +> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x + + If you were to substitute @y@ with @x@ without shifting any variable + indices, then you would get the following incorrect result: + +> λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form + + In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in + order to avoid being misinterpreted as the @x@ bound by the innermost + lambda. If we perform that `shift` then we get the correct result: + +> λ(a : Type) → λ(x : a) → λ(x : a) → x@1 + + As a more worked example, suppose that you were to normalize the following + expression: + +> λ(a : Type) +> → λ(f : a → a → a) +> → λ(x : a) +> → λ(x : a) +> → (λ(x : a) → f x x@1) x@1 + + The correct normalized result would be: + +> λ(a : Type) +> → λ(f : a → a → a) +> → λ(x : a) +> → λ(x : a) +> → f x@1 x + + The above example illustrates how we need to both increase and decrease + variable indices as part of substitution: + + * We need to increase the index of the outer @x\@1@ to @x\@2@ before we + substitute it into the body of the innermost lambda expression in order + to avoid variable capture. This substitution changes the body of the + lambda expression to @(f x\@2 x\@1)@ + + * We then remove the innermost lambda and therefore decrease the indices of + both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one + less @x@ variable is now bound within that scope + + Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to + the indices of all variables named @x@ whose indices are greater than + @(n + m)@, where @m@ is the number of bound variables of the same name + within that scope + + In practice, @d@ is always @1@ or @-1@ because we either: + + * increment variables by @1@ to avoid variable capture during substitution + * decrement variables by @1@ when deleting lambdas after substitution + + @n@ starts off at @0@ when substitution begins and increments every time we + descend into a lambda or let expression that binds a variable of the same + name in order to avoid shifting the bound variables by mistake. +-} +shift :: Integer -> Var -> Expr s a -> Expr t a +shift _ _ (Const a) = Const a +shift d (V x n) (Var (V x' n')) = Var (V x' n'') + where + n'' = if x == x' && n <= n' then n' + d else n' +shift d (V x n) (Lam x' _A b) = Lam x' _A' b' + where + _A' = shift d (V x n ) _A + b' = shift d (V x n') b + where + n' = if x == x' then n + 1 else n +shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B' + where + _A' = shift d (V x n ) _A + _B' = shift d (V x n') _B + where + n' = if x == x' then n + 1 else n +shift d v (App f a) = App f' a' + where + f' = shift d v f + a' = shift d v a +shift d (V x n) (Let f mt r e) = Let f mt' r' e' + where + e' = shift d (V x n') e + where + n' = if x == f then n + 1 else n + + mt' = fmap (shift d (V x n)) mt + r' = shift d (V x n) r +shift d v (Annot a b) = Annot a' b' + where + a' = shift d v a + b' = shift d v b +shift _ _ Bool = Bool +shift _ _ (BoolLit a) = BoolLit a +shift d v (BoolAnd a b) = BoolAnd a' b' + where + a' = shift d v a + b' = shift d v b +shift d v (BoolOr a b) = BoolOr a' b' + where + a' = shift d v a + b' = shift d v b +shift d v (BoolEQ a b) = BoolEQ a' b' + where + a' = shift d v a + b' = shift d v b +shift d v (BoolNE a b) = BoolNE a' b' + where + a' = shift d v a + b' = shift d v b +shift d v (BoolIf a b c) = BoolIf a' b' c' + where + a' = shift d v a + b' = shift d v b + c' = shift d v c +shift _ _ Natural = Natural +shift _ _ (NaturalLit a) = NaturalLit a +shift _ _ NaturalFold = NaturalFold +shift _ _ NaturalBuild = NaturalBuild +shift _ _ NaturalIsZero = NaturalIsZero +shift _ _ NaturalEven = NaturalEven +shift _ _ NaturalOdd = NaturalOdd +shift d v (NaturalPlus a b) = NaturalPlus a' b' + where + a' = shift d v a + b' = shift d v b +shift d v (NaturalTimes a b) = NaturalTimes a' b' + where + a' = shift d v a + b' = shift d v b +shift _ _ Integer = Integer +shift _ _ (IntegerLit a) = IntegerLit a +shift _ _ Double = Double +shift _ _ (DoubleLit a) = DoubleLit a +shift _ _ Text = Text +shift _ _ (TextLit a) = TextLit a +shift d v (TextAppend a b) = TextAppend a' b' + where + a' = shift d v a + b' = shift d v b +shift _ _ List = List +shift d v (ListLit a b) = ListLit a' b' + where + a' = shift d v a + b' = fmap (shift d v) b +shift _ _ ListBuild = ListBuild +shift _ _ ListFold = ListFold +shift _ _ ListLength = ListLength +shift _ _ ListHead = ListHead +shift _ _ ListLast = ListLast +shift _ _ ListIndexed = ListIndexed +shift _ _ ListReverse = ListReverse +shift _ _ Optional = Optional +shift d v (OptionalLit a b) = OptionalLit a' b' + where + a' = shift d v a + b' = fmap (shift d v) b +shift _ _ OptionalFold = OptionalFold +shift d v (Record a) = Record a' + where + a' = fmap (shift d v) a +shift d v (RecordLit a) = RecordLit a' + where + a' = fmap (shift d v) a +shift d v (Union a) = Union a' + where + a' = fmap (shift d v) a +shift d v (UnionLit a b c) = UnionLit a b' c' + where + b' = shift d v b + c' = fmap (shift d v) c +shift d v (Combine a b) = Combine a' b' + where + a' = shift d v a + b' = shift d v b +shift d v (Merge a b c) = Merge a' b' c' + where + a' = shift d v a + b' = shift d v b + c' = shift d v c +shift d v (Field a b) = Field a' b + where + a' = shift d v a +shift d v (Note _ b) = b' + where + b' = shift d v b +-- The Dhall compiler enforces that all embedded values are closed expressions +-- and `shift` does nothing to a closed expression +shift _ _ (Embed p) = Embed p + +{-| Substitute all occurrences of a variable with an expression + +> subst x C B ~ B[x := C] +-} +subst :: Var -> Expr s a -> Expr t a -> Expr s a +subst _ _ (Const a) = Const a +subst (V x n) e (Lam y _A b) = Lam y _A' b' + where + _A' = subst (V x n ) e _A + b' = subst (V x n') (shift 1 (V y 0) e) b + n' = if x == y then n + 1 else n +subst (V x n) e (Pi y _A _B) = Pi y _A' _B' + where + _A' = subst (V x n ) e _A + _B' = subst (V x n') (shift 1 (V y 0) e) _B + n' = if x == y then n + 1 else n +subst v e (App f a) = App f' a' + where + f' = subst v e f + a' = subst v e a +subst v e (Var v') = if v == v' then e else Var v' +subst (V x n) e (Let f mt r b) = Let f mt' r' b' + where + b' = subst (V x n') (shift 1 (V f 0) e) b + where + n' = if x == f then n + 1 else n + + mt' = fmap (subst (V x n) e) mt + r' = subst (V x n) e r +subst x e (Annot a b) = Annot a' b' + where + a' = subst x e a + b' = subst x e b +subst _ _ Bool = Bool +subst _ _ (BoolLit a) = BoolLit a +subst x e (BoolAnd a b) = BoolAnd a' b' + where + a' = subst x e a + b' = subst x e b +subst x e (BoolOr a b) = BoolOr a' b' + where + a' = subst x e a + b' = subst x e b +subst x e (BoolEQ a b) = BoolEQ a' b' + where + a' = subst x e a + b' = subst x e b +subst x e (BoolNE a b) = BoolNE a' b' + where + a' = subst x e a + b' = subst x e b +subst x e (BoolIf a b c) = BoolIf a' b' c' + where + a' = subst x e a + b' = subst x e b + c' = subst x e c +subst _ _ Natural = Natural +subst _ _ (NaturalLit a) = NaturalLit a +subst _ _ NaturalFold = NaturalFold +subst _ _ NaturalBuild = NaturalBuild +subst _ _ NaturalIsZero = NaturalIsZero +subst _ _ NaturalEven = NaturalEven +subst _ _ NaturalOdd = NaturalOdd +subst x e (NaturalPlus a b) = NaturalPlus a' b' + where + a' = subst x e a + b' = subst x e b +subst x e (NaturalTimes a b) = NaturalTimes a' b' + where + a' = subst x e a + b' = subst x e b +subst _ _ Integer = Integer +subst _ _ (IntegerLit a) = IntegerLit a +subst _ _ Double = Double +subst _ _ (DoubleLit a) = DoubleLit a +subst _ _ Text = Text +subst _ _ (TextLit a) = TextLit a +subst x e (TextAppend a b) = TextAppend a' b' + where + a' = subst x e a + b' = subst x e b +subst _ _ List = List +subst x e (ListLit a b) = ListLit a' b' + where + a' = subst x e a + b' = fmap (subst x e) b +subst _ _ ListBuild = ListBuild +subst _ _ ListFold = ListFold +subst _ _ ListLength = ListLength +subst _ _ ListHead = ListHead +subst _ _ ListLast = ListLast +subst _ _ ListIndexed = ListIndexed +subst _ _ ListReverse = ListReverse +subst _ _ Optional = Optional +subst x e (OptionalLit a b) = OptionalLit a' b' + where + a' = subst x e a + b' = fmap (subst x e) b +subst _ _ OptionalFold = OptionalFold +subst x e (Record kts) = Record (fmap (subst x e) kts) +subst x e (RecordLit kvs) = RecordLit (fmap (subst x e) kvs) +subst x e (Union kts) = Union (fmap (subst x e) kts) +subst x e (UnionLit a b kts) = UnionLit a (subst x e b) (fmap (subst x e) kts) +subst x e (Combine a b) = Combine a' b' + where + a' = subst x e a + b' = subst x e b +subst x e (Merge a b c) = Merge a' b' c' + where + a' = subst x e a + b' = subst x e b + c' = subst x e c +subst x e (Field a b) = Field a' b + where + a' = subst x e a +subst x e (Note _ b) = b' + where + b' = subst x e b +-- The Dhall compiler enforces that all embedded values are closed expressions +-- and `subst` does nothing to a closed expression +subst _ _ (Embed p) = Embed p + +{-| Reduce an expression to its normal form, performing beta reduction + + `normalize` does not type-check the expression. You may want to type-check + expressions before normalizing them since normalization can convert an + ill-typed expression into a well-typed expression. + + However, `normalize` will not fail if the expression is ill-typed and will + leave ill-typed sub-expressions unevaluated. +-} +normalize :: Expr s a -> Expr t a +normalize e = case e of + Const k -> Const k + Var v -> Var v + Lam x _A b -> Lam x _A' b' + where + _A' = normalize _A + b' = normalize b + Pi x _A _B -> Pi x _A' _B' + where + _A' = normalize _A + _B' = normalize _B + App f a -> case normalize f of + Lam x _A b -> normalize b'' -- Beta reduce + where + a' = shift 1 (V x 0) a + b' = subst (V x 0) a' b + b'' = shift (-1) (V x 0) b' + f' -> case App f' a' of + -- fold/build fusion for `List` + App (App ListBuild _) (App (App ListFold _) e') -> normalize e' + App (App ListFold _) (App (App ListBuild _) e') -> normalize e' + + -- fold/build fusion for `Natural` + App NaturalBuild (App NaturalFold e') -> normalize e' + App NaturalFold (App NaturalBuild e') -> normalize e' + + App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero -> + normalize (go n0) + where + go !0 = zero + go !n = App succ' (go (n - 1)) + App NaturalBuild k + | check -> NaturalLit n + | otherwise -> App f' a' + where + labeled = + normalize (App (App (App k Natural) "Succ") "Zero") + + n = go 0 labeled + where + go !m (App (Var "Succ") e') = go (m + 1) e' + go !m (Var "Zero") = m + go !_ _ = internalError text + check = go labeled + where + go (App (Var "Succ") e') = go e' + go (Var "Zero") = True + go _ = False + App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0) + App NaturalEven (NaturalLit n) -> BoolLit (even n) + App NaturalOdd (NaturalLit n) -> BoolLit (odd n) + App (App ListBuild t) k + | check -> ListLit t (buildVector k') + | otherwise -> App f' a' + where + labeled = + normalize (App (App (App k (App List t)) "Cons") "Nil") + + k' cons nil = go labeled + where + go (App (App (Var "Cons") x) e') = cons x (go e') + go (Var "Nil") = nil + go _ = internalError text + check = go labeled + where + go (App (App (Var "Cons") _) e') = go e' + go (Var "Nil") = True + go _ = False + App (App (App (App (App ListFold _) (ListLit _ xs)) _) cons) nil -> + normalize (Data.Vector.foldr cons' nil xs) + where + 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) -> + normalize (OptionalLit t (Data.Vector.take 1 ys)) + App (App ListLast _) (ListLit t 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))) + where + t' = Record (Data.Map.fromList kts) + where + kts = [ ("index", Natural) + , ("value", t) + ] + adapt (n, x) = RecordLit (Data.Map.fromList kvs) + where + kvs = [ ("index", NaturalLit (fromIntegral n)) + , ("value", x) + ] + App (App ListReverse _) (ListLit t xs) -> + normalize (ListLit t (Data.Vector.reverse xs)) + App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing -> + normalize (maybe nothing just' (toMaybe xs)) + where + just' y = App just y + toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList + _ -> App f' a' + where + a' = normalize a + Let f _ r b -> normalize b'' + where + r' = shift 1 (V f 0) r + b' = subst (V f 0) r' b + b'' = shift (-1) (V f 0) b' + Annot x _ -> normalize x + Bool -> Bool + BoolLit b -> BoolLit b + BoolAnd x y -> + case x' of + BoolLit xn -> + case y' of + BoolLit yn -> BoolLit (xn && yn) + _ -> BoolAnd x' y' + _ -> BoolAnd x' y' + where + x' = normalize x + y' = normalize y + BoolOr x y -> + case x' of + BoolLit xn -> + case y' of + BoolLit yn -> BoolLit (xn || yn) + _ -> BoolOr x' y' + _ -> BoolOr x' y' + where + x' = normalize x + y' = normalize y + BoolEQ x y -> + case x' of + BoolLit xn -> + case y' of + BoolLit yn -> BoolLit (xn == yn) + _ -> BoolEQ x' y' + _ -> BoolEQ x' y' + where + x' = normalize x + y' = normalize y + BoolNE x y -> + case x' of + BoolLit xn -> + case y' of + BoolLit yn -> BoolLit (xn /= yn) + _ -> BoolNE x' y' + _ -> BoolNE x' y' + where + x' = normalize x + y' = normalize y + BoolIf b true false -> case normalize b of + BoolLit True -> true' + BoolLit False -> false' + b' -> BoolIf b' true' false' + where + true' = normalize true + false' = normalize false + Natural -> Natural + NaturalLit n -> NaturalLit n + NaturalFold -> NaturalFold + NaturalBuild -> NaturalBuild + NaturalIsZero -> NaturalIsZero + NaturalEven -> NaturalEven + NaturalOdd -> NaturalOdd + NaturalPlus x y -> + case x' of + NaturalLit xn -> + case y' of + NaturalLit yn -> NaturalLit (xn + yn) + _ -> NaturalPlus x' y' + _ -> NaturalPlus x' y' + where + x' = normalize x + y' = normalize y + NaturalTimes x y -> + case x' of + NaturalLit xn -> + case y' of + NaturalLit yn -> NaturalLit (xn * yn) + _ -> NaturalTimes x' y' + _ -> NaturalTimes x' y' + where + x' = normalize x + y' = normalize y + Integer -> Integer + IntegerLit n -> IntegerLit n + Double -> Double + DoubleLit n -> DoubleLit n + Text -> Text + TextLit t -> TextLit t + TextAppend x y -> + case x' of + TextLit xt -> + case y' of + TextLit yt -> TextLit (xt <> yt) + _ -> TextAppend x' y' + _ -> TextAppend x' y' + where + x' = normalize x + y' = normalize y + List -> List + ListLit t es -> ListLit t' es' + where + t' = normalize t + es' = fmap normalize es + ListBuild -> ListBuild + ListFold -> ListFold + ListLength -> ListLength + ListHead -> ListHead + ListLast -> ListLast + ListIndexed -> ListIndexed + ListReverse -> ListReverse + Optional -> Optional + OptionalLit t es -> OptionalLit t' es' + where + t' = normalize t + es' = fmap normalize es + OptionalFold -> OptionalFold + Record kts -> Record kts' + where + kts' = fmap normalize kts + RecordLit kvs -> RecordLit kvs' + where + kvs' = fmap normalize kvs + Union kts -> Union kts' + where + kts' = fmap normalize kts + UnionLit k v kvs -> UnionLit k v' kvs' + where + v' = normalize v + kvs' = fmap normalize kvs + Combine x y -> + case x of + RecordLit kvsX -> + case y of + RecordLit kvsY -> + RecordLit (fmap normalize (Data.Map.union kvsX kvsY)) + _ -> Combine x' y' + _ -> Combine x' y' + where + x' = normalize x + y' = normalize y + Merge x y t -> + case x' of + RecordLit kvsX -> + case y' of + UnionLit kY vY _ -> + case Data.Map.lookup kY kvsX of + Just vX -> normalize (App vX vY) + Nothing -> Merge x' y' t' + _ -> Merge x' y' t' + _ -> Merge x' y' t' + where + x' = normalize x + y' = normalize y + t' = normalize t + Field r x -> + case normalize r of + RecordLit kvs -> + case Data.Map.lookup x kvs of + Just v -> normalize v + Nothing -> Field (RecordLit (fmap normalize kvs)) x + r' -> Field r' x + Note _ e' -> normalize e' + Embed a -> Embed a + where + -- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of + -- `normalize`. In theory, this might change a failing repro case into + -- a successful one, but the risk of that is low enough to not warrant + -- the `Show` constraint. I care more about proving at the type level + -- that the @a@ and @s@ type parameters are never used + e'' = bimap (\_ -> ()) (\_ -> ()) e + + text = "normalize (" <> Data.Text.pack (show e'') <> ")" + +internalError :: Data.Text.Text -> forall b . b +internalError text = error (Data.Text.unpack [NeatInterpolation.text| +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 +then you should report the bug at: + +https://github.com/Gabriel439/Haskell-Dhall-Library/issues + +Please include the following text in your bug report: + +``` +$text +``` +|]) + +buildVector :: (forall x . (a -> x -> x) -> x -> x) -> Vector a +buildVector f = Data.Vector.reverse (Data.Vector.create (do + let cons a st = do + (len, cap, mv) <- st + if len < cap + then do + Data.Vector.Mutable.write mv len a + return (len + 1, cap, mv) + else do + let cap' = 2 * cap + mv' <- Data.Vector.Mutable.unsafeGrow mv cap' + Data.Vector.Mutable.write mv' len a + return (len + 1, cap', mv') + let nil = do + mv <- Data.Vector.Mutable.unsafeNew 1 + return (0, 1, mv) + (len, _, mv) <- f cons nil + return (Data.Vector.Mutable.slice 0 len mv) )) diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Import.hs @@ -0,0 +1,486 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# OPTIONS_GHC -Wall #-} + +{-| Dhall lets you import external expressions located either in local files or + hosted on network endpoints. + + To import a local file as an expression, just insert the path to the file, + prepending a @./@ if the path is relative to the current directory. For + example, suppose we had the following three local files: + + > -- id + > \(a : *) -> \(x : a) -> x + + > -- Bool + > forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> Bool + + > -- True + > \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True + + You could then reference them within a Dhall expression using this syntax: + + > ./id ./Bool ./True + + ... which would embed their expressions directly within the syntax tree: + + > -- ... expands out to: + > (\(a : *) -> \(x : a) -> x) + > (forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True) + > (\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True) + + ... and which normalizes to: + + > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True + + Imported expressions may contain imports of their own, too, which will + continue to be resolved. However, Dhall will prevent cyclic imports. For + example, if you had these two files: + + > -- foo + > ./bar + + > -- bar + > ./foo + + ... Dhall would throw the following exception if you tried to import @foo@: + + > dhall: + > ⤷ ./foo + > ⤷ ./bar + > Cyclic import: ./foo + + You can also import expressions hosted on network endpoints. Just use the + URL + + > http://host[:port]/path + + The compiler expects the downloaded expressions to be in the same format + as local files, specifically UTF8-encoded source code text. + + For example, if our @id@ expression were hosted at @http://example.com/id@, + then we would embed the expression within our code using: + + > http://example.com/id + + You can also reuse directory names as expressions. If you provide a path + to a local or remote directory then the compiler will look for a file named + @\@@ within that directory and use that file to represent the directory. +-} + +module Dhall.Import ( + -- * Import + load + , exprFromFile + , exprFromURL + , Cycle(..) + , ReferentiallyOpaque(..) + , Imported(..) + ) where + +import Control.Exception + (Exception, IOException, SomeException, catch, onException, throwIO) +import Control.Monad (join) +import Control.Monad.IO.Class (MonadIO(..)) +import Control.Monad.Trans.State.Strict (StateT) +import Data.ByteString.Lazy (ByteString) +import Data.Map.Strict (Map) +import Data.Monoid ((<>)) +import Data.Text.Buildable (build) +import Data.Text.Lazy (Text) +import Data.Text.Lazy.Builder (Builder) +#if MIN_VERSION_base(4,8,0) +#else +import Data.Traversable (traverse) +#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(..)) +import Network.HTTP.Client (HttpException(..), Manager) +import Prelude hiding (FilePath) +import Text.Trifecta (Result(..)) +import Text.Trifecta.Delta (Delta(..)) + +import qualified Control.Monad.Trans.State.Strict as State +import qualified Data.ByteString.Lazy +import qualified Data.Foldable as Foldable +import qualified Data.List as List +import qualified Data.Map.Strict as Map +import qualified Data.Text +import qualified Data.Text.Lazy as Text +import qualified Data.Text.Lazy.Builder as Builder +import qualified Data.Text.Lazy.Encoding +import qualified Dhall.Parser +import qualified Dhall.TypeCheck +import qualified Filesystem.Path.CurrentOS +import qualified NeatInterpolation +import qualified Network.HTTP.Client as HTTP +import qualified Network.HTTP.Client.TLS as HTTP +import qualified Filesystem.Path.CurrentOS as Filesystem +import qualified Text.Parser.Combinators +import qualified Text.Parser.Token +import qualified Text.Trifecta + +builderToString :: Builder -> String +builderToString = Text.unpack . Builder.toLazyText + +-- | An import failed because of a cycle in the import graph +newtype Cycle = Cycle + { cyclicImport :: Path -- ^ The offending cyclic import + } + deriving (Typeable) + +instance Exception Cycle + +instance Show Cycle where + show (Cycle path) = "Cyclic import: " ++ builderToString (build path) + +{-| Dhall tries to ensure that all expressions hosted on network endpoints are + weakly referentially transparent, meaning roughly that any two clients will + compile the exact same result given the same URL. + + 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 + 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 + its dependencies change. + + In general, either interpretation of referential transparency is not + enforceable in a networked context since one can easily violate referential + transparency with a custom DNS, but Dhall can still try to guard against + common unintentional violations. To do this, Dhall enforces that a + non-local import may not reference a local import. + + Local imports are defined as: + + * A file + + * A URL with a host of @localhost@ or @127.0.0.1@ + + All other imports are defined to be non-local +-} +newtype ReferentiallyOpaque = ReferentiallyOpaque + { opaqueImport :: Path -- ^ The offending opaque import + } deriving (Typeable) + +instance Exception ReferentiallyOpaque + +instance Show ReferentiallyOpaque where + show (ReferentiallyOpaque path) = + "Referentially opaque import: " ++ builderToString (build path) + +-- | Extend another exception with the current import stack +data Imported e = Imported + { importStack :: [Path] -- ^ Imports resolved so far, in reverse order + , nested :: e -- ^ The nested exception + } deriving (Typeable) + +instance Exception e => Exception (Imported e) + +instance Show e => Show (Imported e) where + show (Imported paths e) = + unlines (map (\(n, path) -> take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)) paths') + ++ "\n" + ++ show e + where + -- Canonicalize all paths + paths' = zip [0..] (drop 1 (reverse (canonicalizeAll paths))) + +newtype PrettyHttpException = PrettyHttpException HttpException + deriving (Typeable) + +instance Exception PrettyHttpException + +instance Show PrettyHttpException where + show (PrettyHttpException (FailedConnectionException2 _ _ _ _)) = + "\ESC[1;31mError\ESC[0m: Connection timed out\n" + show (PrettyHttpException e) = show e + +data Status = Status + { _stack :: [Path] + , _cache :: Map Path (Expr Src X) + , _manager :: Maybe Manager + } + +canonicalizeAll :: [Path] -> [Path] +canonicalizeAll = map canonicalize . List.tails + +stack :: Lens' Status [Path] +stack k s = fmap (\x -> s { _stack = x }) (k (_stack s)) + +cache :: Lens' Status (Map Path (Expr Src X)) +cache k s = fmap (\x -> s { _cache = x }) (k (_cache s)) + +manager :: Lens' Status (Maybe Manager) +manager k s = fmap (\x -> s { _manager = x }) (k (_manager s)) + +needManager :: StateT Status IO Manager +needManager = do + x <- zoom manager State.get + case x of + Just m -> return m + Nothing -> do + let settings = HTTP.tlsManagerSettings + { HTTP.managerResponseTimeout = Just 1000000 } -- 1 second + m <- liftIO (HTTP.newManager settings) + zoom manager (State.put (Just m)) + return m + +{-| This function computes the current path by taking the last absolute path + (either an absolute `FilePath` or `URL`) and combining it with all following + relative paths + + For example, if the file `./foo/bar` imports `./baz`, that will resolve to + `./foo/baz`. Relative imports are relative to a file's parent directory. + This also works for URLs, too. + + This code is full of all sorts of edge cases so it wouldn't surprise me at + all if you find something broken in here. Most of the ugliness is due to: + + * Handling paths ending with @/\@@ by stripping the @/\@@ suffix if and only + 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 + 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. +-} +canonicalize :: [Path] -> Path +canonicalize [] = File "." +canonicalize (File file0:paths0) = + if Filesystem.relative file0 + then go file0 paths0 + else File (clean file0) + where + go currPath [] = File (clean currPath) + go currPath (URL url0:_ ) = combine prefix suffix + where + prefix = parentURL (removeAtFromURL url0) + + suffix = clean currPath + + -- `clean` will resolve internal @.@/@..@'s in @currPath@, but we still + -- need to manually handle @.@/@..@'s at the beginning of the path + combine url path = case Filesystem.stripPrefix ".." path of + Just path' -> combine url' path' + where + url' = parentURL (removeAtFromURL url) + Nothing -> case Filesystem.stripPrefix "." path of + Just path' -> combine url path' + Nothing -> + -- This `last` is safe because the lexer constrains all + -- URLs to be non-empty. I couldn't find a simple and safe + -- equivalent in the `text` API + case Text.last url of + '/' -> URL (url <> path') + _ -> URL (url <> "/" <> path') + where + path' = Text.fromStrict (case Filesystem.toText path of + Left txt -> txt + Right txt -> txt ) + go currPath (File file:paths) = + if Filesystem.relative file + then go file' paths + else File (clean file') + where + file' = Filesystem.parent (removeAtFromFile file) currPath +canonicalize (URL path:_) = URL path + +parentURL :: Text -> Text +parentURL = Text.dropWhileEnd (/= '/') + +removeAtFromURL:: Text -> Text +removeAtFromURL url + | Text.isSuffixOf "/@" url = Text.dropEnd 2 url + | Text.isSuffixOf "/" url = Text.dropEnd 1 url + | otherwise = url + +removeAtFromFile :: FilePath -> FilePath +removeAtFromFile file = + if Filesystem.filename file == "@" + then Filesystem.parent file + else file + +-- | Remove all @.@'s and @..@'s in the path +clean :: FilePath -> FilePath +clean = strip . Filesystem.collapse + where + strip p = case Filesystem.stripPrefix "." p of + Nothing -> p + Just p' -> p' + +-- | Parse an expression from a `FilePath` containing a Dhall program +exprFromFile :: FilePath -> IO (Expr Src Path) +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` + let handler :: IOException -> IO (Result (Expr Src Path)) + handler e = do + let string' = Filesystem.Path.CurrentOS.encodeString (path "@") + + -- If the fallback fails, reuse the original exception to avoid user + -- confusion + Text.Trifecta.parseFromFileEx parser string' `onException` throwIO e + + x <- Text.Trifecta.parseFromFileEx parser string `catch` handler + case x of + Failure errInfo -> throwIO (ParseError (Text.Trifecta._errDoc errInfo)) + Success expr -> return expr + where + parser = do + Text.Parser.Token.whiteSpace + r <- unParser Dhall.Parser.exprA + Text.Parser.Combinators.eof + return r + +exprFromURL :: Manager -> Text -> IO (Expr Src Path) +exprFromURL m url = do + request <- HTTP.parseUrlThrow (Text.unpack url) + + let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString) + handler err@(HTTP.StatusCodeException _ _ _) = do + let request' = request { HTTP.path = HTTP.path request <> "/@" } + -- If the fallback fails, reuse the original exception to avoid user + -- confusion + HTTP.httpLbs request' m `onException` throwIO (PrettyHttpException err) + handler err = throwIO (PrettyHttpException err) + response <- HTTP.httpLbs request m `catch` handler + + let bytes = HTTP.responseBody response + + text <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes of + Left err -> throwIO err + Right text -> return text + + let urlBytes = Data.Text.Lazy.Encoding.encodeUtf8 url + let delta = Directed (Data.ByteString.Lazy.toStrict urlBytes) 0 0 0 0 + case Text.Trifecta.parseString parser delta (Text.unpack text) of + Failure err -> do + -- Also try the fallback in case of a parse error, since the parse + -- error might signify that this URL points to a directory list + let err' = ParseError (Text.Trifecta._errDoc err) + + request' <- HTTP.parseUrlThrow (Text.unpack url) + + let request'' = request' { HTTP.path = HTTP.path request' <> "/@" } + response' <- HTTP.httpLbs request'' m `onException` throwIO err' + + let bytes' = HTTP.responseBody response' + + text' <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes' of + Left _ -> throwIO err' + Right text' -> return text' + + case Text.Trifecta.parseString parser delta (Text.unpack text') of + Failure _ -> throwIO err' + Success expr -> return expr + Success expr -> return expr + where + parser = do + Text.Parser.Token.whiteSpace + r <- unParser Dhall.Parser.exprA + Text.Parser.Combinators.eof + return r + +{-| Load a `Path` as a \"dynamic\" expression (without resolving any imports) + + This also returns the true final path (i.e. explicit "/@" at the end for + directories) +-} +loadDynamic :: Path -> StateT Status IO (Expr Src Path) +loadDynamic p = do + paths <- zoom stack State.get + + let handler :: SomeException -> IO (Expr Src Path) + handler e = throwIO (Imported (p:paths) e) + case canonicalize (p:paths) of + File file -> do + liftIO (exprFromFile file `catch` handler) + URL url -> do + m <- needManager + liftIO (exprFromURL m url `catch` handler) + +-- | Load a `Path` as a \"static\" expression (with all imports resolved) +loadStatic :: Path -> StateT Status IO (Expr Src X) +loadStatic path = do + paths <- zoom stack State.get + + let local (URL url) = case HTTP.parseUrlThrow (Text.unpack url) of + Nothing -> False + Just request -> case HTTP.host request of + "127.0.0.1" -> True + "localhost" -> True + _ -> False + local (File _) = True + + let parent = canonicalize paths + let here = canonicalize (path:paths) + + if local here && not (local parent) + then liftIO (throwIO (Imported paths (ReferentiallyOpaque path))) + else return () + + (expr, cached) <- if here `elem` canonicalizeAll paths + then liftIO (throwIO (Imported paths (Cycle path))) + else do + m <- zoom cache State.get + case Map.lookup here m of + Just expr -> return (expr, True) + Nothing -> do + expr' <- loadDynamic path + expr'' <- case traverse (\_ -> Nothing) expr' of + -- No imports left + Just expr -> do + zoom cache (State.put $! Map.insert here expr m) + return expr + -- Some imports left, so recurse + Nothing -> do + let paths' = path:paths + zoom stack (State.put paths') + expr'' <- fmap join (traverse loadStatic expr') + zoom stack (State.put paths) + return expr'' + return (expr'', False) + + -- Type-check expressions here for two separate reasons: + -- + -- * to verify that they are closed + -- * to catch type errors as early in the import process as possible + -- + -- There is no need to check expressions that have been cached, since they + -- have already been checked + if cached + then return () + else case Dhall.TypeCheck.typeOf expr of + Left err -> liftIO (throwIO (Imported (path:paths) err)) + Right _ -> return () + + return expr + +{-| Resolve all imports within an expression + + By default the starting path is the current directory, but you can override + the starting path with a file if you read in the expression from that file +-} +load + :: Maybe Path + -- ^ Starting path + -> Expr Src Path + -- ^ Expression to resolve + -> IO (Expr Src X) +load here expr = State.evalStateT (fmap join (traverse loadStatic expr)) status + where + status = Status (Foldable.toList here) Map.empty Nothing diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Parser.hs @@ -0,0 +1,708 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Parser ( + -- * Utilities + exprFromText + + -- * Parsers + , exprA + + -- * Types + , Src(..) + , ParseError(..) + , Parser(..) + ) where + +import Control.Applicative (Alternative(..), optional) +import Control.Exception (Exception) +import Control.Monad (MonadPlus) +import Data.ByteString (ByteString) +import Data.Map (Map) +import Data.Monoid ((<>)) +import Data.Sequence (ViewL(..)) +import Data.Text.Buildable (Buildable(..)) +import Data.Text.Lazy (Text) +import Data.Typeable (Typeable) +import Data.Vector (Vector) +import Dhall.Core (Const(..), Expr(..), Path(..), Var(..)) +import Filesystem.Path (FilePath) +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) + +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 +import qualified Data.Text +import qualified Data.Text.Lazy +import qualified Data.Text.Lazy.Encoding +import qualified Data.Vector +import qualified Dhall.Core +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 + +data Src = Src Delta Delta ByteString deriving (Show) + +instance Buildable Src where + build (Src begin _ bytes) = + build text <> "\n" + <> "\n" + <> build (show (Text.PrettyPrint.ANSI.Leijen.pretty begin)) + <> "\n" + where + bytes' = Data.ByteString.Lazy.fromStrict bytes + + text = Data.Text.Lazy.strip (Data.Text.Lazy.Encoding.decodeUtf8 bytes') + +newtype Parser a = Parser { unParser :: Text.Trifecta.Parser a } + deriving + ( Functor + , Applicative + , Monad + , Alternative + , MonadPlus + , Parsing + , CharParsing + , DeltaParsing + , MarkParsing Delta + ) + +instance TokenParsing Parser where + someSpace = + Text.Parser.Token.Style.buildSomeSpaceParser + (Parser someSpace) + Text.Parser.Token.Style.haskellCommentStyle + + nesting (Parser m) = Parser (nesting m) + + semi = Parser semi + + highlight h (Parser m) = Parser (highlight h m) + + token parser = do + r <- parser + Text.Parser.Token.whiteSpace + return r + +identifierStyle :: IdentifierStyle Parser +identifierStyle = IdentifierStyle + { _styleName = "dhall" + , _styleStart = + Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ "_") + , _styleLetter = + Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ "_/") + , _styleReserved = Data.HashSet.fromList + [ "let" + , "in" + , "Type" + , "Kind" + , "forall" + , "Bool" + , "True" + , "False" + , "merge" + , "if" + , "then" + , "else" + , "Natural" + , "Natural/fold" + , "Natural/build" + , "Natural/isZero" + , "Natural/even" + , "Natural/odd" + , "Integer" + , "Double" + , "Text" + , "List" + , "List/build" + , "List/fold" + , "List/length" + , "List/head" + , "List/last" + , "List/indexed" + , "List/reverse" + , "Optional" + , "Optional/fold" + ] + , _styleHighlight = Identifier + , _styleReservedHighlight = ReservedIdentifier + } + +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) + +toMap :: [(Text, a)] -> Parser (Map Text a) +toMap kvs = do + let adapt (k, v) = (k, pure v) + let m = Data.Map.fromListWith (<|>) (fmap adapt kvs) + let action k vs = case Data.Sequence.viewl vs of + EmptyL -> empty + v :< vs' -> + if null vs' + then pure v + else + Text.Parser.Combinators.unexpected + ("duplicate field: " ++ Data.Text.Lazy.unpack k) + Data.Map.traverseWithKey action m + +reserve :: String -> Parser () +reserve string = do + _ <- Text.Parser.Token.reserve identifierStyle string + return () + +symbol :: String -> Parser () +symbol string = do + _ <- Text.Parser.Token.symbol string + return () + +lambda :: Parser () +lambda = symbol "\\" <|> symbol "λ" + +pi :: Parser () +pi = reserve "forall" <|> reserve "∀" + +arrow :: Parser () +arrow = symbol "->" <|> symbol "→" + +combine :: Parser () +combine = symbol "/\\" <|> symbol "∧" + +label :: Parser Text +label = Text.Parser.Token.ident identifierStyle "label" + +exprA :: Parser (Expr Src Path) +exprA = do + a <- exprB + + let exprA0 = do + symbol ":" + b <- exprA + return (Annot a b) + + let exprA1 = pure a + + exprA0 <|> exprA1 + +exprB :: Parser (Expr Src Path) +exprB = choice + [ noted exprB0 + , noted exprB1 + , noted exprB3 + , noted exprB5 + , noted exprB6 + , noted exprB7 + , noted (try exprB2) + , exprB8 + ] + where + exprB0 = do + lambda + symbol "(" + a <- label + symbol ":" + b <- exprA + symbol ")" + arrow + c <- exprB + return (Lam a b c) + + exprB1 = do + reserve "if" + a <- exprA + reserve "then" + b <- exprB + reserve "else" + c <- exprC + return (BoolIf a b c) + + exprB2 = do + a <- exprC + arrow + b <- exprB + return (Pi "_" a b) + + exprB3 = do + pi + symbol "(" + a <- label + symbol ":" + b <- exprA + symbol ")" + arrow + c <- exprB + return (Pi a b c) + + exprB5 = do + reserve "let" + a <- label + b <- optional (do + symbol ":" + exprA ) + symbol "=" + c <- exprA + reserve "in" + d <- exprB + return (Let a b c d) + + exprB6 = do + symbol "[" + a <- elems + symbol "]" + symbol ":" + b <- listLike + c <- exprE + return (b c (Data.Vector.fromList a)) + + exprB7 = do + reserve "merge" + a <- exprE + b <- exprE + symbol ":" + c <- exprD + return (Merge a b c) + + exprB8 = exprC + +listLike :: Parser (Expr Src Path -> Vector (Expr Src Path) -> Expr Src Path) +listLike = + ( listLike0 + <|> listLike1 + ) + where + listLike0 = do + reserve "List" + return ListLit + + listLike1 = do + reserve "Optional" + return OptionalLit + +-- TODO: Add `noted` in the right places here +exprC :: Parser (Expr Src Path) +exprC = expressionParser + where + expressionParser = Text.Parser.Expression.buildExpressionParser + [ [ operator BoolAnd (symbol "&&") + , operator NaturalTimes (symbol "*" ) + , operator Combine combine + ] + , [ operator BoolOr (symbol "||") + , operator TextAppend (symbol "++") + , operator NaturalPlus (symbol "+" ) + ] + , [ operator BoolEQ (symbol "==") + , operator BoolNE (symbol "/=") + ] + ] + exprD + + operator op parser = Infix (do parser; return op) AssocRight + +-- 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 +-- definition because left recursion greatly simplifies the use of `noted`. The +-- work-around is to parse in two phases: +-- +-- * 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 exprE) + let app nL@(Note (Src before _ bytesL) eL) nR@(Note (Src _ after bytesR) eR) = + Note (Src before after (bytesL <> bytesR)) (App nL nR) + app _ _ = Dhall.Core.internalError + ("exprD: foldl1 app (" <> Data.Text.pack (show es) <> ")") + return (Data.List.foldl1 app es) + +exprE :: Parser (Expr Src Path) +exprE = noted (do + a <- exprF + b <- many (do + symbol "." + label ) + return (Data.List.foldl Field a b) ) + +exprF :: Parser (Expr Src Path) +exprF = choice + [ noted exprF01 + , noted exprF03 + , noted exprF04 + , noted exprF05 + , noted exprF06 + , noted exprF07 + , noted exprF12 + , noted exprF13 + , noted exprF14 + , noted exprF15 + , noted exprF16 + , noted exprF17 + , noted exprF18 + , noted exprF20 + , noted exprF19 + , noted exprF21 + , noted exprF22 + , noted (try exprF25) + , noted exprF23 + , noted (try exprF26) + , noted exprF24 + , noted exprF27 + , noted (try exprF28) + , noted exprF29 + , noted (try exprF30) + , noted exprF31 + , noted exprF32 + , noted exprF02 + , noted exprF08 + , noted exprF09 + , noted exprF10 + , noted exprF11 + , noted exprF00 + , exprF33 + ] + where + exprF00 = do + a <- var + return (Var a) + + exprF01 = do + a <- const + return (Const a) + + exprF02 = do + reserve "Natural" + return Natural + + exprF03 = do + reserve "Natural/fold" + return NaturalFold + + exprF04 = do + reserve "Natural/build" + return NaturalBuild + + exprF05 = do + reserve "Natural/isZero" + return NaturalIsZero + + exprF06 = do + reserve "Natural/even" + return NaturalEven + + exprF07 = do + reserve "Natural/odd" + return NaturalOdd + + exprF08 = do + reserve "Integer" + return Integer + + exprF09 = do + reserve "Double" + return Double + + exprF10 = do + reserve "Text" + return Text + + exprF11 = do + reserve "List" + return List + + exprF12 = do + reserve "List/build" + return ListBuild + + exprF13 = do + reserve "List/fold" + return ListFold + + exprF14 = do + reserve "List/length" + return ListLength + + exprF15 = do + reserve "List/head" + return ListHead + + exprF16 = do + reserve "List/last" + return ListLast + + exprF17 = do + reserve "List/indexed" + return ListIndexed + + exprF18 = do + reserve "List/reverse" + return ListReverse + + exprF19 = do + reserve "Optional" + return Optional + + exprF20 = do + reserve "Optional/fold" + return OptionalFold + + exprF21 = do + reserve "Bool" + return Bool + + exprF22 = do + reserve "True" + return (BoolLit True) + + exprF23 = do + reserve "False" + return (BoolLit False) + + exprF24 = do + a <- Text.Parser.Token.natural + return (IntegerLit a) + + exprF25 = do + Text.Parser.Char.char '+' + a <- Text.Parser.Token.natural + return (NaturalLit (fromIntegral a)) + + exprF26 = do + a <- Text.Parser.Token.double + return (DoubleLit a) + + exprF27 = do + a <- Text.Parser.Token.stringLiteral + return (TextLit a) + + exprF28 = record + + exprF29 = recordLit + + exprF30 = union + + exprF31 = unionLit + + exprF32 = do + a <- import_ + return (Embed a) + + exprF33 = do + symbol "(" + a <- exprA + symbol ")" + return a + +const :: Parser Const +const = const0 + <|> const1 + where + const0 = do + reserve "Type" + return Type + + const1 = do + reserve "Kind" + return Kind + +var :: Parser Var +var = do + a <- label + m <- optional (do + symbol "@" + Text.Parser.Token.natural ) + let b = case m of + Just b -> b + Nothing -> 0 + return (V a b) + +elems :: Parser [Expr Src Path] +elems = Text.Parser.Combinators.sepBy exprA (symbol ",") + +recordLit :: Parser (Expr Src Path) +recordLit = + recordLit0 + <|> recordLit1 + where + recordLit0 = do + symbol "{=}" + return (RecordLit (Data.Map.fromList [])) + + recordLit1 = do + symbol "{" + a <- fieldValues + b <- toMap a + symbol "}" + return (RecordLit b) + +fieldValues :: Parser [(Text, Expr Src Path)] +fieldValues = + Text.Parser.Combinators.sepBy1 fieldValue (symbol ",") + +fieldValue :: Parser (Text, Expr Src Path) +fieldValue = do + a <- label + symbol "=" + b <- exprA + return (a, b) + +record :: Parser (Expr Src Path) +record = do + symbol "{" + a <- fieldTypes + b <- toMap a + symbol "}" + return (Record b) + +fieldTypes :: Parser [(Text, Expr Src Path)] +fieldTypes = + Text.Parser.Combinators.sepBy fieldType (symbol ",") + +fieldType :: Parser (Text, Expr Src Path) +fieldType = do + a <- label + symbol ":" + b <- exprA + return (a, b) + +union :: Parser (Expr Src Path) +union = do + symbol "<" + a <- alternativeTypes + b <- toMap a + symbol ">" + return (Union b) + +alternativeTypes :: Parser [(Text, Expr Src Path)] +alternativeTypes = + Text.Parser.Combinators.sepBy alternativeType (symbol "|") + +alternativeType :: Parser (Text, Expr Src Path) +alternativeType = do + a <- label + symbol ":" + b <- exprA + return (a, b) + +unionLit :: Parser (Expr Src Path) +unionLit = + try unionLit0 + <|> unionLit1 + where + unionLit0 = do + symbol "<" + a <- label + symbol "=" + b <- exprA + symbol ">" + return (UnionLit a b Data.Map.empty) + + unionLit1 = do + symbol "<" + a <- label + symbol "=" + b <- exprA + symbol "|" + c <- alternativeTypes + d <- toMap c + symbol ">" + return (UnionLit a b d) + +import_ :: Parser Path +import_ = do + a <- import0 <|> import1 + Text.Parser.Token.whiteSpace + return a + where + import0 = do + a <- file + return (File a) + + import1 = do + a <- url + return (URL a) + +file :: Parser FilePath +file = try (token file0) + <|> token file1 + <|> token file2 + where + file0 = do + a <- Text.Parser.Char.string "/" + b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + case b of + '\\':_ -> empty -- So that "/\" parses as the operator and not a path + _ -> return () + return (Filesystem.Path.CurrentOS.decodeString (a <> b)) + + file1 = do + a <- Text.Parser.Char.string "./" + b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + return (Filesystem.Path.CurrentOS.decodeString (a <> b)) + + file2 = do + a <- Text.Parser.Char.string "../" + b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + return (Filesystem.Path.CurrentOS.decodeString (a <> b)) + +url :: Parser Text +url = try url0 + <|> url1 + where + url0 = do + a <- Text.Parser.Char.string "https://" + b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + return (Data.Text.Lazy.pack (a <> b)) + + url1 = do + a <- Text.Parser.Char.string "http://" + b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace)) + return (Data.Text.Lazy.pack (a <> b)) + +-- | A parsing error +newtype ParseError = ParseError Doc deriving (Typeable) + +instance Show ParseError where + show (ParseError doc) = show doc + +instance Exception ParseError + +-- | Parse an expression from `Text` containing a Dhall program +exprFromText :: Delta -> Text -> Either ParseError (Expr Src Path) +exprFromText delta text = case result of + Success r -> Right r + Failure errInfo -> Left (ParseError (Text.Trifecta._errDoc errInfo)) + where + string = Data.Text.Lazy.unpack text + + parser = unParser (do + Text.Parser.Token.whiteSpace + r <- exprA + Text.Parser.Combinators.eof + return r ) + + result = Text.Trifecta.parseString parser delta string diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/TypeCheck.hs @@ -0,0 +1,2869 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wall #-} + +module Dhall.TypeCheck ( + -- * Type-checking + typeWith + , typeOf + + -- * Types + , X(..) + , TypeError(..) + , DetailedTypeError(..) + , TypeMessage(..) + ) where + +import Control.Exception (Exception) +import Data.Foldable (forM_) +import Data.Monoid ((<>)) +import Data.Set (Set) +import Data.Text.Buildable (Buildable(..)) +import Data.Text.Lazy (Text) +import Data.Text.Lazy.Builder (Builder) +import Data.Typeable (Typeable) +import Dhall.Core (Const(..), Expr(..), Var(..)) +import Dhall.Context (Context) + +import qualified Control.Monad.Trans.State.Strict as State +import qualified Data.Map +import qualified Data.Set +import qualified Data.Text +import qualified Data.Text.Lazy as Text +import qualified Data.Text.Lazy.Builder as Builder +import qualified Data.Vector +import qualified Dhall.Context +import qualified Dhall.Core +import qualified NeatInterpolation + +axiom :: Const -> Either (TypeError s) Const +axiom Type = return Kind +axiom Kind = Left (TypeError Dhall.Context.empty (Const Kind) Untyped) + +rule :: Const -> Const -> Either () Const +rule Type Kind = Left () +rule Type Type = return Type +rule Kind Kind = return Kind +rule Kind Type = return Type + +match :: Var -> Var -> [(Text, Text)] -> Bool +match (V xL nL) (V xR nR) [] = + xL == xR && nL == nR +match (V xL 0 ) (V xR 0 ) ((xL', xR'):_ ) + | xL == xL' && xR == xR' = True +match (V xL nL) (V xR nR) ((xL', xR'):xs) = + match (V xL nL') (V xR nR') xs + where + nL' = if xL == xL' then nL - 1 else nL + nR' = if xR == xR' then nR - 1 else nR + +propEqual :: Expr s X -> Expr t X -> Bool +propEqual eL0 eR0 = + State.evalState + (go (Dhall.Core.normalize eL0) (Dhall.Core.normalize eR0)) + [] + where + go (Const Type) (Const Type) = return True + go (Const Kind) (Const Kind) = return True + go (Var vL) (Var vR) = do + ctx <- State.get + return (match vL vR ctx) + go (Pi xL tL bL) (Pi xR tR bR) = do + ctx <- State.get + eq1 <- go tL tR + if eq1 + then do + State.put ((xL, xR):ctx) + eq2 <- go bL bR + State.put ctx + return eq2 + else return False + go (App fL aL) (App fR aR) = do + b1 <- go fL fR + if b1 then go aL aR else return False + go Bool Bool = return True + go Natural Natural = return True + go Integer Integer = return True + go Double Double = return True + go Text Text = return True + go List List = return True + go Optional Optional = return True + go (Record ktsL0) (Record ktsR0) = do + let loop ((kL, tL):ktsL) ((kR, tR):ktsR) + | kL == kR = do + b <- go tL tR + if b + then loop ktsL ktsR + else return False + loop [] [] = return True + loop _ _ = return False + loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0) + go (Union ktsL0) (Union ktsR0) = do + let loop ((kL, tL):ktsL) ((kR, tR):ktsR) + | kL == kR = do + b <- go tL tR + if b + then loop ktsL ktsR + else return False + loop [] [] = return True + loop _ _ = return False + loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0) + go _ _ = return False + +{-| Type-check an expression and return the expression's type if type-checking + suceeds 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. +-} +typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s) (Expr s X) +typeWith _ (Const c ) = do + fmap Const (axiom c) +typeWith ctx e@(Var (V x n) ) = do + case Dhall.Context.lookup x n ctx of + Nothing -> Left (TypeError ctx e UnboundVariable) + Just a -> return a +typeWith ctx (Lam x _A b ) = do + let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx) + _B <- typeWith ctx' b + let p = Pi x _A _B + _t <- typeWith ctx p + return p +typeWith ctx e@(Pi x _A _B ) = do + tA <- fmap Dhall.Core.normalize (typeWith ctx _A) + kA <- case tA of + Const k -> return k + _ -> Left (TypeError ctx e (InvalidInputType _A)) + + let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx) + tB <- fmap Dhall.Core.normalize (typeWith ctx' _B) + kB <- case tB of + Const k -> return k + _ -> Left (TypeError ctx' e (InvalidOutputType _B)) + + case rule kA kB of + Left () -> Left (TypeError ctx e (NoDependentTypes _A _B)) + Right k -> Right (Const k) +typeWith ctx e@(App f a ) = do + tf <- fmap Dhall.Core.normalize (typeWith ctx f) + (x, _A, _B) <- case tf of + Pi x _A _B -> return (x, _A, _B) + _ -> Left (TypeError ctx e (NotAFunction f tf)) + _A' <- typeWith ctx a + if propEqual _A _A' + then do + let a' = Dhall.Core.shift 1 (V x 0) a + let _B' = Dhall.Core.subst (V x 0) a' _B + let _B'' = Dhall.Core.shift (-1) (V x 0) _B' + return _B'' + else do + let nf_A = Dhall.Core.normalize _A + let nf_A' = Dhall.Core.normalize _A' + Left (TypeError ctx e (TypeMismatch f nf_A a nf_A')) +typeWith ctx e@(Let f mt r b ) = do + tR <- typeWith ctx r + ttR <- fmap Dhall.Core.normalize (typeWith ctx tR) + kR <- case ttR of + Const k -> return k + -- Don't bother to provide a `let`-specific version of this error + -- message because this should never happen anyway + _ -> Left (TypeError ctx e (InvalidInputType tR)) + + let ctx' = Dhall.Context.insert f tR ctx + tB <- typeWith ctx' b + ttB <- fmap Dhall.Core.normalize (typeWith ctx tB) + kB <- case ttB of + Const k -> return k + -- Don't bother to provide a `let`-specific version of this error + -- message because this should never happen anyway + _ -> Left (TypeError ctx e (InvalidOutputType tB)) + + case rule kR kB of + Left () -> Left (TypeError ctx e (NoDependentLet tR tB)) + Right _ -> return () + + case mt of + Nothing -> do + return () + Just t -> do + let nf_t = Dhall.Core.normalize t + let nf_tR = Dhall.Core.normalize tR + if propEqual nf_tR nf_t + then return () + else Left (TypeError ctx e (AnnotMismatch r nf_t nf_tR)) + + return tB +typeWith ctx e@(Annot x t ) = do + -- This is mainly just to check that `t` is not `Kind` + _ <- typeWith ctx t + + t' <- typeWith ctx x + if propEqual t t' + then do + return t + else do + let nf_t = Dhall.Core.normalize t + let nf_t' = Dhall.Core.normalize t' + Left (TypeError ctx e (AnnotMismatch x nf_t nf_t')) +typeWith _ Bool = do + return (Const Type) +typeWith _ (BoolLit _ ) = do + return Bool +typeWith ctx e@(BoolAnd l r ) = do + tl <- fmap Dhall.Core.normalize (typeWith ctx l) + case tl of + Bool -> return () + _ -> Left (TypeError ctx e (CantAnd l tl)) + + tr <- fmap Dhall.Core.normalize (typeWith ctx r) + case tr of + Bool -> return () + _ -> Left (TypeError ctx e (CantAnd r tr)) + + return Bool +typeWith ctx e@(BoolOr l r ) = do + tl <- fmap Dhall.Core.normalize (typeWith ctx l) + case tl of + Bool -> return () + _ -> Left (TypeError ctx e (CantOr l tl)) + + tr <- fmap Dhall.Core.normalize (typeWith ctx r) + case tr of + Bool -> return () + _ -> Left (TypeError ctx e (CantOr r tr)) + + return Bool +typeWith ctx e@(BoolEQ l r ) = do + tl <- fmap Dhall.Core.normalize (typeWith ctx l) + case tl of + Bool -> return () + _ -> Left (TypeError ctx e (CantEQ l tl)) + + tr <- fmap Dhall.Core.normalize (typeWith ctx r) + case tr of + Bool -> return () + _ -> Left (TypeError ctx e (CantEQ r tr)) + + return Bool +typeWith ctx e@(BoolNE l r ) = do + tl <- fmap Dhall.Core.normalize (typeWith ctx l) + case tl of + Bool -> return () + _ -> Left (TypeError ctx e (CantNE l tl)) + + tr <- fmap Dhall.Core.normalize (typeWith ctx r) + case tr of + Bool -> return () + _ -> Left (TypeError ctx e (CantNE r tr)) + + return Bool +typeWith ctx e@(BoolIf x y z ) = do + tx <- fmap Dhall.Core.normalize (typeWith ctx x) + case tx of + Bool -> return () + _ -> Left (TypeError ctx e (InvalidPredicate x tx)) + ty <- fmap Dhall.Core.normalize (typeWith ctx y ) + tty <- fmap Dhall.Core.normalize (typeWith ctx ty) + case tty of + Const Type -> return () + _ -> Left (TypeError ctx e (IfBranchMustBeTerm True y ty tty)) + + tz <- fmap Dhall.Core.normalize (typeWith ctx z) + ttz <- fmap Dhall.Core.normalize (typeWith ctx tz) + case ttz of + Const Type -> return () + _ -> Left (TypeError ctx e (IfBranchMustBeTerm False z tz ttz)) + + if propEqual ty tz + then return () + else Left (TypeError ctx e (IfBranchMismatch y z ty tz)) + return ty +typeWith _ Natural = do + return (Const Type) +typeWith _ (NaturalLit _ ) = do + return Natural +typeWith _ NaturalFold = do + return + (Pi "_" Natural + (Pi "natural" (Const Type) + (Pi "succ" (Pi "_" "natural" "natural") + (Pi "zero" "natural" "natural") ) ) ) +typeWith _ NaturalBuild = do + return + (Pi "_" + (Pi "natural" (Const Type) + (Pi "succ" (Pi "_" "natural" "natural") + (Pi "zero" "natural" "natural") ) ) + Natural ) +typeWith _ NaturalIsZero = do + return (Pi "_" Natural Bool) +typeWith _ NaturalEven = do + return (Pi "_" Natural Bool) +typeWith _ NaturalOdd = do + return (Pi "_" Natural Bool) +typeWith ctx e@(NaturalPlus l r) = do + tl <- fmap Dhall.Core.normalize (typeWith ctx l) + case tl of + Natural -> return () + _ -> Left (TypeError ctx e (CantAdd l tl)) + + tr <- fmap Dhall.Core.normalize (typeWith ctx r) + case tr of + Natural -> return () + _ -> Left (TypeError ctx e (CantAdd r tr)) + return Natural +typeWith ctx e@(NaturalTimes l r) = do + tl <- fmap Dhall.Core.normalize (typeWith ctx l) + case tl of + Natural -> return () + _ -> Left (TypeError ctx e (CantMultiply l tl)) + + tr <- fmap Dhall.Core.normalize (typeWith ctx r) + case tr of + Natural -> return () + _ -> Left (TypeError ctx e (CantMultiply r tr)) + return Natural +typeWith _ Integer = do + return (Const Type) +typeWith _ (IntegerLit _ ) = do + return Integer +typeWith _ Double = do + return (Const Type) +typeWith _ (DoubleLit _ ) = do + return Double +typeWith _ Text = do + return (Const Type) +typeWith _ (TextLit _ ) = do + return Text +typeWith ctx e@(TextAppend l r ) = do + tl <- fmap Dhall.Core.normalize (typeWith ctx l) + case tl of + Text -> return () + _ -> Left (TypeError ctx e (CantTextAppend l tl)) + + tr <- fmap Dhall.Core.normalize (typeWith ctx r) + case tr of + Text -> return () + _ -> Left (TypeError ctx e (CantTextAppend r tr)) + return Text +typeWith _ List = do + return (Pi "_" (Const Type) (Const Type)) +typeWith ctx e@(ListLit t xs ) = do + 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' + Left (TypeError ctx e (InvalidListElement i nf_t x nf_t')) ) + return (App List t) +typeWith _ ListBuild = do + return + (Pi "a" (Const Type) + (Pi "_" + (Pi "list" (Const Type) + (Pi "cons" (Pi "_" "a" (Pi "_" "list" "list")) + (Pi "nil" "list" "list") ) ) + (App List "a") ) ) +typeWith _ ListFold = do + return + (Pi "a" (Const Type) + (Pi "_" (App List "a") + (Pi "list" (Const Type) + (Pi "cons" (Pi "_" "a" (Pi "_" "list" "list")) + (Pi "nil" "list" "list")) ) ) ) +typeWith _ ListLength = do + return (Pi "a" (Const Type) (Pi "_" (App List "a") Natural)) +typeWith _ ListHead = do + return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a"))) +typeWith _ ListLast = do + return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a"))) +typeWith _ ListIndexed = do + let kts = [("index", Natural), ("value", "a")] + return + (Pi "a" (Const Type) + (Pi "_" (App List "a") + (App List (Record (Data.Map.fromList kts))) ) ) +typeWith _ ListReverse = do + return (Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a"))) +typeWith _ Optional = do + return (Pi "_" (Const Type) (Const Type)) +typeWith ctx e@(OptionalLit t xs) = do + s <- fmap Dhall.Core.normalize (typeWith ctx t) + case s of + Const Type -> return () + _ -> Left (TypeError ctx e (InvalidOptionalType t)) + let n = Data.Vector.length xs + if 2 <= n + then Left (TypeError ctx e (InvalidOptionalLiteral n)) + else return () + forM_ xs (\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' + Left (TypeError ctx e (InvalidOptionalElement nf_t x nf_t')) ) + return (App Optional t) +typeWith _ OptionalFold = do + return + (Pi "a" (Const Type) + (Pi "_" (App Optional "a") + (Pi "maybe" (Const Type) + (Pi "just" (Pi "_" "a" "maybe") + (Pi "nothing" "maybe" "maybe") ) ) ) ) +typeWith ctx e@(Record kts ) = do + let process (k, t) = do + s <- fmap Dhall.Core.normalize (typeWith ctx t) + case s of + Const Type -> return () + _ -> Left (TypeError ctx e (InvalidFieldType k t)) + mapM_ process (Data.Map.toList kts) + return (Const Type) +typeWith ctx e@(RecordLit kvs ) = do + let process (k, v) = do + t <- typeWith ctx v + s <- fmap Dhall.Core.normalize (typeWith ctx t) + case s of + Const Type -> return () + _ -> Left (TypeError ctx e (InvalidField k v)) + return (k, t) + kts <- mapM process (Data.Map.toAscList kvs) + return (Record (Data.Map.fromAscList kts)) +typeWith ctx e@(Union kts ) = do + let process (k, t) = do + s <- fmap Dhall.Core.normalize (typeWith ctx t) + case s of + Const Type -> return () + _ -> Left (TypeError ctx e (InvalidAlternativeType k t)) + mapM_ process (Data.Map.toList kts) + return (Const Type) +typeWith ctx e@(UnionLit k v kts) = do + case Data.Map.lookup k kts of + Just _ -> Left (TypeError ctx e (DuplicateAlternative k)) + Nothing -> return () + t <- typeWith ctx v + let union = Union (Data.Map.insert k t kts) + _ <- typeWith ctx union + return union +typeWith ctx e@(Combine kvsX kvsY) = do + tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) + ktsX <- case tKvsX of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX)) + let ksX = Data.Map.keysSet ktsX + + tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY) + ktsY <- case tKvsY of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY)) + let ksY = Data.Map.keysSet ktsY + + let ks = Data.Set.intersection ksX ksY + if Data.Set.null ks + then return () + else Left (TypeError ctx e (FieldCollision ks)) + return (Record (Data.Map.union ktsX ktsY)) +typeWith ctx e@(Merge kvsX kvsY t) = do + tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) + ktsX <- case tKvsX of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX)) + let ksX = Data.Map.keysSet ktsX + + tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY) + ktsY <- case tKvsY of + Union kts -> return kts + _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY)) + let ksY = Data.Map.keysSet ktsY + + let diffX = Data.Set.difference ksX ksY + let diffY = Data.Set.difference ksY ksX + + if Data.Set.null diffX + then return () + else Left (TypeError ctx e (UnusedHandler diffX)) + + let process (kY, tY) = do + case Data.Map.lookup kY ktsX of + Nothing -> Left (TypeError ctx e (MissingHandler diffY)) + Just tX -> + case tX of + Pi _ tY' t' -> do + if propEqual tY tY' + then return () + else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) + if propEqual t t' + then return () + else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t')) + _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) + mapM_ process (Data.Map.toList ktsY) + return t +typeWith ctx e@(Field r x ) = do + t <- fmap Dhall.Core.normalize (typeWith ctx r) + case t of + Record kts -> + case Data.Map.lookup x kts of + Just t' -> return t' + Nothing -> Left (TypeError ctx e (MissingField x t)) + _ -> Left (TypeError ctx e (NotARecord x r t)) +typeWith ctx (Note s e' ) = case typeWith ctx e' of + Left (TypeError ctx' (Note s' e'') m) -> Left (TypeError ctx' (Note s' e'') m) + Left (TypeError ctx' e'' m) -> Left (TypeError ctx' (Note s e'') m) + Right r -> Right r +typeWith _ (Embed p ) = do + absurd p + +{-| `typeOf` is the same as `typeWith` with an empty context, meaning that the + expression must be closed (i.e. no free variables), otherwise type-checking + will fail. +-} +typeOf :: Expr s X -> Either (TypeError s) (Expr s X) +typeOf = typeWith Dhall.Context.empty + +-- | Like `Data.Void.Void`, except with a shorter inferred type +newtype X = X { absurd :: forall a . a } + +instance Show X where + show = absurd + +instance Buildable X where + build = absurd + +-- | The specific type error +data TypeMessage s + = UnboundVariable + | InvalidInputType (Expr s X) + | InvalidOutputType (Expr s X) + | NotAFunction (Expr s X) (Expr s X) + | TypeMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X) + | AnnotMismatch (Expr s X) (Expr s X) (Expr s X) + | Untyped + | 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) + | InvalidOptionalLiteral Int + | InvalidOptionalType (Expr s X) + | InvalidPredicate (Expr s X) (Expr s X) + | IfBranchMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X) + | IfBranchMustBeTerm Bool (Expr s X) (Expr s X) (Expr s X) + | InvalidField Text (Expr s X) + | InvalidFieldType Text (Expr s X) + | InvalidAlternative Text (Expr s X) + | InvalidAlternativeType Text (Expr s X) + | DuplicateAlternative Text + | MustCombineARecord (Expr s X) (Expr s X) + | FieldCollision (Set Text) + | MustMergeARecord (Expr s X) (Expr s X) + | MustMergeUnion (Expr s X) (Expr s X) + | UnusedHandler (Set Text) + | MissingHandler (Set Text) + | HandlerInputTypeMismatch Text (Expr s X) (Expr s X) + | HandlerOutputTypeMismatch Text (Expr s X) (Expr s X) + | HandlerNotAFunction Text (Expr s X) + | NotARecord Text (Expr s X) (Expr s X) + | MissingField Text (Expr s X) + | CantAnd (Expr s X) (Expr s X) + | CantOr (Expr s X) (Expr s X) + | CantEQ (Expr s X) (Expr s X) + | CantNE (Expr s X) (Expr s X) + | CantTextAppend (Expr s X) (Expr s X) + | CantAdd (Expr s X) (Expr s X) + | CantMultiply (Expr s X) (Expr s X) + | NoDependentLet (Expr s X) (Expr s X) + | NoDependentTypes (Expr s X) (Expr s X) + deriving (Show) + +shortTypeMessage :: TypeMessage s -> Builder +shortTypeMessage msg = + "\ESC[1;31mError\ESC[0m: " <> build short <> "\n" + where + ErrorMessages {..} = prettyTypeMessage msg + +longTypeMessage :: TypeMessage s -> Builder +longTypeMessage msg = + "\ESC[1;31mError\ESC[0m: " <> build short <> "\n" + <> "\n" + <> long + where + ErrorMessages {..} = prettyTypeMessage msg + +data ErrorMessages = ErrorMessages + { short :: Builder + -- ^ Default succinct 1-line explanation of what went wrong + , long :: Builder + -- ^ Longer and more detailed explanation of the error + } + +instance Buildable ErrorMessages where + build (ErrorMessages {..}) = + "Error: " <> build short <> "\n" + <> "\n" + <> long + +_NOT :: Data.Text.Text +_NOT = "\ESC[1mnot\ESC[0m" + +prettyTypeMessage :: TypeMessage s -> ErrorMessages +prettyTypeMessage UnboundVariable = ErrorMessages {..} + where + short = "Unbound variable" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Expressions can only reference previously introduced (i.e. "bound") +variables that are still "in scope" + +For example, the following valid expressions introduce a "bound" variable named +❰x❱: + + + ┌─────────────────┐ + │ λ(x : Bool) → x │ Anonymous functions introduce "bound" variables + └─────────────────┘ + ⇧ + This is the bound variable + + + ┌─────────────────┐ + │ let x = 1 in x │ ❰let❱ expressions introduce "bound" variables + └─────────────────┘ + ⇧ + This is the bound variable + + +However, the following expressions are not valid because they all reference a +variable that has not been introduced yet (i.e. an "unbound" variable): + + + ┌─────────────────┐ + │ λ(x : Bool) → y │ The variable ❰y❱ hasn't been introduced yet + └─────────────────┘ + ⇧ + This is the unbound variable + + + ┌──────────────────────────┐ + │ (let x = True in x) && x │ ❰x❱ is undefined outside the parentheses + └──────────────────────────┘ + ⇧ + This is the unbound variable + + + ┌────────────────┐ + │ let x = x in x │ The definition for ❰x❱ cannot reference itself + └────────────────┘ + ⇧ + This is the unbound variable + + +Some common reasons why you might get this error: + +● You misspell a variable name, like this: + + + ┌────────────────────────────────────────────────────┐ + │ λ(empty : Bool) → if emty then "Empty" else "Full" │ + └────────────────────────────────────────────────────┘ + ⇧ + Typo + + +● You misspell a reserved identifier, like this: + + + ┌──────────────────────────┐ + │ foral (a : Type) → a → a │ + └──────────────────────────┘ + ⇧ + Typo + + +● You tried to define a recursive value, like this: + + + ┌─────────────────────┐ + │ let x = x + +1 in x │ + └─────────────────────┘ + ⇧ + Recursive definitions are not allowed + + +● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱ + + + Unbound variable + ⇩ + ┌─────────────────┐ + │ (x : Bool) → x │ + └─────────────────┘ + ⇧ + A ❰λ❱ here would transform this into a valid anonymous function + + + Unbound variable + ⇩ + ┌────────────────────┐ + │ (x : Bool) → Bool │ + └────────────────────┘ + ⇧ + A ❰∀❱ or ❰forall❱ here would transform this into a valid function type +|] + +prettyTypeMessage (InvalidInputType expr) = ErrorMessages {..} + where + short = "Invalid function input" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: A function can accept an input "term" that has a given "type", like +this: + + + This is the input term that the function accepts + ⇩ + ┌───────────────────────┐ + │ ∀(x : Natural) → Bool │ This is the type of a function that accepts an + └───────────────────────┘ input term named ❰x❱ that has type ❰Natural❱ + ⇧ + This is the type of the input term + + + ┌────────────────┐ + │ Bool → Integer │ This is the type of a function that accepts an anonymous + └────────────────┘ input term that has type ❰Bool❱ + ⇧ + This is the type of the input term + + +... or a function can accept an input "type" that has a given "kind", like this: + + + This is the input type that the function accepts + ⇩ + ┌────────────────────┐ + │ ∀(a : Type) → Type │ This is the type of a function that accepts an input + └────────────────────┘ type named ❰a❱ that has kind ❰Type❱ + ⇧ + This is the kind of the input type + + + ┌──────────────────────┐ + │ (Type → Type) → Type │ This is the type of a function that accepts an + └──────────────────────┘ anonymous input type that has kind ❰Type → Type❱ + ⇧ + This is the kind of the input type + + +Other function inputs are $_NOT valid, like this: + + + ┌──────────────┐ + │ ∀(x : 1) → x │ ❰1❱ is a "term" and not a "type" nor a "kind" so ❰x❱ + └──────────────┘ cannot have "type" ❰1❱ or "kind" ❰1❱ + ⇧ + This is not a type or kind + + + ┌──────────┐ + │ True → x │ ❰True❱ is a "term" and not a "type" nor a "kind" so the + └──────────┘ anonymous input cannot have "type" ❰True❱ or "kind" ❰True❱ + ⇧ + This is not a type or kind + + +You annotated a function input with the following expression: + +↳ $txt + +... which is neither a type nor a kind +|] + where + txt = Text.toStrict (Dhall.Core.pretty expr) + +prettyTypeMessage (InvalidOutputType expr) = ErrorMessages {..} + where + short = "Invalid function output" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: A function can return an output "term" that has a given "type", +like this: + + + ┌────────────────────┐ + │ ∀(x : Text) → Bool │ This is the type of a function that returns an + └────────────────────┘ output term that has type ❰Bool❱ + ⇧ + This is the type of the output term + + + ┌────────────────┐ + │ Bool → Integer │ This is the type of a function that returns an output + └────────────────┘ term that has type ❰Int❱ + ⇧ + This is the type of the output term + + +... or a function can return an output "type" that has a given "kind", like +this: + + ┌────────────────────┐ + │ ∀(a : Type) → Type │ This is the type of a function that returns an + └────────────────────┘ output type that has kind ❰Type❱ + ⇧ + This is the kind of the output type + + + ┌──────────────────────┐ + │ (Type → Type) → Type │ This is the type of a function that returns an + └──────────────────────┘ output type that has kind ❰Type❱ + ⇧ + This is the kind of the output type + + +Other outputs are $_NOT valid, like this: + + + ┌─────────────────┐ + │ ∀(x : Bool) → x │ ❰x❱ is a "term" and not a "type" nor a "kind" so the + └─────────────────┘ output cannot have "type" ❰x❱ or "kind" ❰x❱ + ⇧ + This is not a type or kind + + + ┌─────────────┐ + │ Text → True │ ❰True❱ is a "term" and not a "type" nor a "kind" so the + └─────────────┘ output cannot have "type" ❰True❱ or "kind" ❰True❱ + ⇧ + This is not a type or kind + + +You specified that your function outputs a: + +↳ $txt + +... which is neither a type nor a kind: + +Some common reasons why you might get this error: + +● You use ❰∀❱ instead of ❰λ❱ by mistake, like this: + + + ┌────────────────┐ + │ ∀(x: Bool) → x │ + └────────────────┘ + ⇧ + Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function +|] + where + txt = Text.toStrict (Dhall.Core.pretty expr) + +prettyTypeMessage (NotAFunction expr0 expr1) = ErrorMessages {..} + where + short = "Not a function" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Expressions separated by whitespace denote function application, +like this: + + + ┌─────┐ + │ f x │ This denotes the function ❰f❱ applied to an argument named ❰x❱ + └─────┘ + + +A function is a term that has type ❰a → b❱ for some ❰a❱ or ❰b❱. For example, +the following expressions are all functions because they have a function type: + + + The function's input type is ❰Bool❱ + ⇩ + ┌───────────────────────────────┐ + │ λ(x : Bool) → x : Bool → Bool │ User-defined anonymous function + └───────────────────────────────┘ + ⇧ + The function's output type is ❰Bool❱ + + + The function's input type is ❰Natural❱ + ⇩ + ┌───────────────────────────────┐ + │ Natural/even : Natural → Bool │ Built-in function + └───────────────────────────────┘ + ⇧ + The function's output type is ❰Bool❱ + + + The function's input kind is ❰Type❱ + ⇩ + ┌───────────────────────────────┐ + │ λ(a : Type) → a : Type → Type │ Type-level functions are still functions + └───────────────────────────────┘ + ⇧ + The function's output kind is ❰Type❱ + + + The function's input kind is ❰Type❱ + ⇩ + ┌────────────────────┐ + │ List : Type → Type │ Built-in type-level function + └────────────────────┘ + ⇧ + The function's output kind is ❰Type❱ + + + Function's input has kind ❰Type❱ + ⇩ + ┌─────────────────────────────────────────────────┐ + │ List/head : ∀(a : Type) → (List a → Optional a) │ A function can return + └─────────────────────────────────────────────────┘ another function + ⇧ + Function's output has type ❰List a → Optional a❱ + + + The function's input type is ❰List Text❱ + ⇩ + ┌────────────────────────────────────────────┐ + │ List/head Text : List Text → Optional Text │ A function applied to an + └────────────────────────────────────────────┘ argument can be a function + ⇧ + The function's output type is ❰Optional Text❱ + + +An expression is not a function if the expression's type is not of the form +❰a → b❱. For example, these are $_NOT functions: + + + ┌─────────────┐ + │ 1 : Integer │ ❰1❱ is not a function because ❰Integer❱ is not the type of + └─────────────┘ a function + + + ┌────────────────────────┐ + │ Natural/even +2 : Bool │ ❰Natural/even +2❱ is not a function because + └────────────────────────┘ ❰Bool❱ is not the type of a function + + + ┌──────────────────┐ + │ List Text : Type │ ❰List Text❱ is not a function because ❰Type❱ is not + └──────────────────┘ the type of a function + + +You tried to use the following expression as a function: + +↳ $txt0 + +... but this expression's type is: + +↳ $txt1 + +... which is not a function type +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..} + where + short = "Wrong function argument" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every function declares what type or kind of argument to accept + +For example: + + + ┌───────────────────────────────┐ + │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts + └───────────────────────────────┘ arguments that have type ❰Bool❱ + ⇧ + The function's input type + + + ┌───────────────────────────────┐ + │ Natural/even : Natural → Bool │ This built-in function only accepts + └───────────────────────────────┘ arguments that have type ❰Natural❱ + ⇧ + The function's input type + + + ┌───────────────────────────────┐ + │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts + └───────────────────────────────┘ arguments that have kind ❰Type❱ + ⇧ + The function's input kind + + + ┌────────────────────┐ + │ List : Type → Type │ This built-in function only accepts arguments that + └────────────────────┘ have kind ❰Type❱ + ⇧ + The function's input kind + + +For example, the following expressions are valid: + + + ┌────────────────────────┐ + │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type + └────────────────────────┘ of argument that the anonymous function accepts + + + ┌─────────────────┐ + │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of + └─────────────────┘ argument that the ❰Natural/even❱ function accepts, + + + ┌────────────────────────┐ + │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind + └────────────────────────┘ of argument that the anonymous function accepts + + + ┌───────────┐ + │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument + └───────────┘ that that the ❰List❱ function accepts + + +However, you can $_NOT apply a function to the wrong type or kind of argument + +For example, the following expressions are not valid: + + + ┌───────────────────────┐ + │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function + └───────────────────────┘ expects an argument that has type ❰Bool❱ + + + ┌──────────────────┐ + │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function + └──────────────────┘ expects an argument that has type ❰Natural❱ + + + ┌────────────────────────┐ + │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous + └────────────────────────┘ function expects an argument of kind ❰Type❱ + + + ┌────────┐ + │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an + └────────┘ argument that has kind ❰Type❱ + + +You tried to invoke the following function: + +↳ $txt0 + +... which expects an argument of type or kind: + +↳ $txt1 + +... on the following argument: + +↳ $txt2 + +... which has a different type or kind: + +↳ $txt3 + +Some common reasons why you might get this error: + +● You omit a function argument by mistake: + + + ┌────────────────────────────────────────┐ + │ List/head ([1, 2, 3] : List Integer) │ + └────────────────────────────────────────┘ + ⇧ + ❰List/head❱ is missing the first argument, + which should be: ❰Integer❱ + + +● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ + + ┌────────────────┐ + │ Natural/even 2 │ + └────────────────┘ + ⇧ + This should be ❰+2❱ +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + txt2 = Text.toStrict (Dhall.Core.pretty expr2) + txt3 = Text.toStrict (Dhall.Core.pretty expr3) + +prettyTypeMessage (AnnotMismatch expr0 expr1 expr2) = ErrorMessages {..} + where + short = "Expression doesn't match annotation" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can annotate an expression with its type or kind using the +❰:❱ symbol, like this: + + + ┌───────┐ + │ x : t │ ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱ + └───────┘ + +The type checker verifies that the expression's type or kind matches the +provided annotation + +For example, all of the following are valid annotations that the type checker +accepts: + + + ┌─────────────┐ + │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type + └─────────────┘ checker accepts the annotation + + + ┌────────────────────────┐ + │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type + └────────────────────────┘ checker accepts the annotation + + + ┌────────────────────┐ + │ List : Type → Type │ ❰List❱ is an expression that has kind ❰Type → Type❱, + └────────────────────┘ so the type checker accepts the annotation + + + ┌──────────────────┐ + │ List Text : Type │ ❰List Text❱ is an expression that has kind ❰Type❱, so + └──────────────────┘ the type checker accepts the annotation + + +However, the following annotations are $_NOT valid and the type checker will +reject them: + + + ┌──────────┐ + │ 1 : Text │ The type checker rejects this because ❰1❱ does not have type + └──────────┘ ❰Text❱ + + + ┌─────────────┐ + │ List : Type │ ❰List❱ does not have kind ❰Type❱ + └─────────────┘ + + +You or the interpreter annotated this expression: + +↳ $txt0 + +... with this type or kind: + +↳ $txt1 + +... but the inferred type or kind of the expression is actually: + +↳ $txt2 + +Some common reasons why you might get this error: + +● The Haskell Dhall interpreter implicitly inserts a top-level annotation + matching the expected type + + For example, if you run the following Haskell code: + + + ┌───────────────────────────────┐ + │ >>> input auto "1" :: IO Text │ + └───────────────────────────────┘ + + + ... then the interpreter will actually type check the following annotated + expression: + + + ┌──────────┐ + │ 1 : Text │ + └──────────┘ + + + ... and then type-checking will fail +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + txt2 = Text.toStrict (Dhall.Core.pretty expr2) + +prettyTypeMessage Untyped = ErrorMessages {..} + where + short = "❰Kind❱ has no type or kind" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: There are four levels of expressions that form a heirarchy: + +● terms +● types +● kinds +● sorts + +The following example illustrates this heirarchy: + + ┌────────────────────────────┐ + │ "ABC" : Text : Type : Kind │ + └────────────────────────────┘ + ⇧ ⇧ ⇧ ⇧ + term type kind sort + +There is nothing above ❰Kind❱ in this hierarchy, so if you try to type check any +expression containing ❰Kind❱ anywhere in the expression then type checking fails + +Some common reasons why you might get this error: + +● You supplied a kind where a type was expected + + For example, the following expression will fail to type check: + + ┌────────────────┐ + │ [] : List Type │ + └────────────────┘ + ⇧ + ❰Type❱ is a kind, not a type +|] + +prettyTypeMessage (InvalidPredicate expr0 expr1) = ErrorMessages {..} + where + short = "Invalid predicate for ❰if❱" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every ❰if❱ expression begins with a predicate which must have type +❰Bool❱ + +For example, these are valid ❰if❱ expressions: + + + ┌──────────────────────────────┐ + │ if True then "Yes" else "No" │ + └──────────────────────────────┘ + ⇧ + Predicate + + + ┌─────────────────────────────────────────┐ + │ λ(x : Bool) → if x then False else True │ + └─────────────────────────────────────────┘ + ⇧ + Predicate + + +... but these are $_NOT valid ❰if❱ expressions: + + + ┌───────────────────────────┐ + │ if 0 then "Yes" else "No" │ ❰0❱ does not have type ❰Bool❱ + └───────────────────────────┘ + + + ┌────────────────────────────┐ + │ if "" then False else True │ ❰""❱ does not have type ❰Bool❱ + └────────────────────────────┘ + + +Your ❰if❱ expression begins with the following predicate: + +↳ $txt0 + +... that has type: + +↳ $txt1 + +... but the predicate must instead have type ❰Bool❱ + +Some common reasons why you might get this error: + +● You might be used to other programming languages that accept predicates other + than ❰Bool❱ + + For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat + them as equivalent to ❰False❱. However, the Dhall language does not permit + this +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (IfBranchMustBeTerm b expr0 expr1 expr2) = + ErrorMessages {..} + where + short = "❰if❱ branch is not a term" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which +is an expression: + + + Expression for ❰then❱ branch + ⇩ + ┌────────────────────────────────┐ + │ if True then "Hello, world!" │ + │ else "Goodbye, world!" │ + └────────────────────────────────┘ + ⇧ + Expression for ❰else❱ branch + + +These expressions must be a "term", where a "term" is defined as an expression +that has a type thas has kind ❰Type❱ + +For example, the following expressions are all valid "terms": + + + ┌────────────────────┐ + │ 1 : Integer : Type │ ❰1❱ is a term with a type (❰Integer❱) of kind ❰Type❱ + └────────────────────┘ + ⇧ + term + + + ┌─────────────────────────────────────┐ + │ Natural/odd : Natural → Bool : Type │ ❰Natural/odd❱ is a term with a type + └─────────────────────────────────────┘ (❰Natural → Bool❱) of kind ❰Type❱ + ⇧ + term + + +However, the following expressions are $_NOT valid terms: + + + ┌────────────────────┐ + │ Text : Type : Kind │ ❰Text❱ has kind (❰Type❱) of sort ❰Kind❱ and is + └────────────────────┘ therefore not a term + ⇧ + type + + + ┌───────────────────────────┐ + │ List : Type → Type : Kind │ ❰List❱ has kind (❰Type → Type❱) of sort + └───────────────────────────┘ ❰Kind❱ and is therefore not a term + ⇧ + type-level function + + +This means that you cannot define an ❰if❱ expression that returns a type. For +example, the following ❰if❱ expression is $_NOT valid: + + + ┌─────────────────────────────┐ + │ if True then Text else Bool │ Invalid ❰if❱ expression + └─────────────────────────────┘ + ⇧ ⇧ + type type + + +Your ❰$txt0❱ branch of your ❰if❱ expression is: + +↳ $txt1 + +... which has kind: + +↳ $txt2 + +... of sort: + +↳ $txt3 + +... and is not a term. Therefore your ❰if❱ expression is not valid +|] + where + txt0 = if b then "then" else "else" + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + txt2 = Text.toStrict (Dhall.Core.pretty expr1) + txt3 = Text.toStrict (Dhall.Core.pretty expr2) + +prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) = + ErrorMessages {..} + where + short = "❰if❱ branches must have matching types" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which +is an expression: + + + Expression for ❰then❱ branch + ⇩ + ┌────────────────────────────────┐ + │ if True then "Hello, world!" │ + │ else "Goodbye, world!" │ + └────────────────────────────────┘ + ⇧ + Expression for ❰else❱ branch + + +These two expressions must have the same type. For example, the following ❰if❱ +expressions are all valid: + + + ┌──────────────────────────────────┐ + │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱ + └──────────────────────────────────┘ + + + ┌────────────────────────────┐ + │ λ(b : Bool) → │ + │ if b then Natural/even │ Both branches have type ❰Natural → Bool❱ + │ else Natural/odd │ + └────────────────────────────┘ + + +However, the following expression is $_NOT valid: + + + This branch has type ❰Integer❱ + ⇩ + ┌────────────────────────┐ + │ if True then 0 │ + │ else "ABC" │ + └────────────────────────┘ + ⇧ + This branch has type ❰Text❱ + + +The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is +always ❰True❱ or ❰False❱ + +Your ❰if❱ expression has the following ❰then❱ branch: + +↳ $txt0 + +... which has type: + +↳ $txt2 + +... and the following ❰else❱ branch: + +↳ $txt1 + +... which has a different type: + +↳ $txt3 + +Fix your ❰then❱ and ❰else❱ branches to have matching types +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + txt2 = Text.toStrict (Dhall.Core.pretty expr2) + txt3 = Text.toStrict (Dhall.Core.pretty expr3) + +prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..} + where + short = "Invalid type for ❰List❱ elements" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every ❰List❱ documents the type of its elements with a type +annotation, like this: + + + ┌──────────────────────────┐ + │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s + └──────────────────────────┘ + ⇧ + The type of the ❰List❱'s elements, which are ❰Integer❱s + + + ┌───────────────────┐ + │ [] : List Integer │ An empty ❰List❱ + └───────────────────┘ + ⇧ + You still specify the type even when the ❰List❱ is empty + + +The element type must be a type and not something else. For example, the +following element types are $_NOT valid: + + + ┌──────────────┐ + │ ... : List 1 │ + └──────────────┘ + ⇧ + This is an ❰Integer❱ and not a ❰Type❱ + + + ┌─────────────────┐ + │ ... : List Type │ + └─────────────────┘ + ⇧ + 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 + +... which is not a ❰Type❱ +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (InvalidListElement i expr0 expr1 expr2) = + ErrorMessages {..} + where + short = "List element has the wrong type" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every element in the list must have a type matching the type +annotation at the end of the list + +For example, this is a valid ❰List❱: + + + ┌──────────────────────────┐ + │ [1, 2, 3] : List Integer │ Every element in this ❰List❱ is an ❰Integer❱ + └──────────────────────────┘ + + +.. but this is $_NOT a valid ❰List❱: + + + ┌──────────────────────────────┐ + │ [1, "ABC", 3] : List Integer │ The second element is not an ❰Integer❱ + └──────────────────────────────┘ + + +Your ❰List❱ elements should have 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 (InvalidOptionalType expr0) = ErrorMessages {..} + where + short = "Invalid type for ❰Optional❱ element" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every optional element ends with a type annotation for the element +that might be present, like this: + + + ┌────────────────────────┐ + │ [1] : Optional Integer │ An optional element that's present + └────────────────────────┘ + ⇧ + The type of the ❰Optional❱ element, which is an ❰Integer❱ + + + ┌────────────────────────┐ + │ [] : Optional Integer │ An optional element that's absent + └────────────────────────┘ + ⇧ + You still specify the type even when the element is absent + + +The element type must be a type and not something else. For example, the +following element types are $_NOT valid: + + + ┌──────────────────┐ + │ ... : Optional 1 │ + └──────────────────┘ + ⇧ + This is an ❰Integer❱ and not a ❰Type❱ + + + ┌─────────────────────┐ + │ ... : Optional Type │ + └─────────────────────┘ + ⇧ + This is a ❰Kind❱ and not a ❰Type❱ + + +Even if the element is absent you still must specify a valid type + +You declared that the ❰Optional❱ element should have type: + +↳ $txt0 + +... which is not a ❰Type❱ + +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..} + where + short = "❰Optional❱ element has the wrong type" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: An ❰Optional❱ element must have a type matching the type annotation + +For example, this is a valid ❰Optional❱ value: + + + ┌────────────────────────┐ + │ [1] : Optional Integer │ ❰1❱ is an ❰Integer❱, which matches the type + └────────────────────────┘ + + +... but this is $_NOT a valid ❰Optional❱ value: + + + ┌────────────────────────────┐ + │ ["ABC"] : Optional Integer │ ❰"ABC"❱ is not an ❰Integer❱ + └────────────────────────────┘ + + +Your ❰Optional❱ element should have this type: + +↳ $txt0 + +... but the element you provided: + +↳ $txt1 + +... has this type instead: + +↳ $txt2 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + txt2 = Text.toStrict (Dhall.Core.pretty expr2) + +prettyTypeMessage (InvalidOptionalLiteral n) = ErrorMessages {..} + where + short = "Multiple ❰Optional❱ elements not allowed" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s: + + + ┌───────────────────────┐ + │ [] : Optional Integer │ An ❰Optional❱ value which is absent + └───────────────────────┘ + + + ┌───────────────────────┐ + │ [] : List Integer │ An empty (0-element) ❰List❱ + └───────────────────────┘ + + + ┌────────────────────────┐ + │ [1] : Optional Integer │ An ❰Optional❱ value which is present + └────────────────────────┘ + + + ┌────────────────────────┐ + │ [1] : List Integer │ A singleton (1-element) ❰List❱ + └────────────────────────┘ + + +However, an ❰Optional❱ value can $_NOT have more than one element, whereas a +❰List❱ can have multiple elements: + + + ┌───────────────────────────┐ + │ [1, 2] : Optional Integer │ Invalid: multiple elements $_NOT allowed + └───────────────────────────┘ + + + ┌───────────────────────────┐ + │ [1, 2] : List Integer │ Valid: multiple elements allowed + └───────────────────────────┘ + + +Your ❰Optional❱ value had this many elements: + +↳ $txt0 + +... when an ❰Optional❱ value can only have at most one element + +Some common reasons why you might get this error: + +● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this: + + + ┌────────────────────────────────────────────────────┐ + │ List/length Integer ([1, 2, 3] : Optional Integer) │ + └────────────────────────────────────────────────────┘ + ⇧ + This should be ❰List❱ instead +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty n) + +prettyTypeMessage (InvalidFieldType k expr0) = ErrorMessages {..} + where + short = "Invalid field type" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every record type documents the type of each field, like this: + + ┌──────────────────────────────────────────────┐ + │ { foo : Integer, bar : Integer, baz : Text } │ + └──────────────────────────────────────────────┘ + +However, fields cannot be annotated with expressions other than types + +For example, these record types are $_NOT valid: + + + ┌────────────────────────────┐ + │ { foo : Integer, bar : 1 } │ + └────────────────────────────┘ + ⇧ + ❰1❱ is an ❰Integer❱ and not a ❰Type❱ + + + ┌───────────────────────────────┐ + │ { foo : Integer, bar : Type } │ + └───────────────────────────────┘ + ⇧ + ❰Type❱ is a ❰Kind❱ and not a ❰Type❱ + + +You provided a record type with a key named: + +↳ $txt0 + +... annotated with the following expression: + +↳ $txt1 + +... which is not a type +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k ) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (InvalidField k expr0) = ErrorMessages {..} + where + short = "Invalid field" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every record literal is a set of fields assigned to values, like +this: + + ┌────────────────────────────────────────┐ + │ { foo = 100, bar = True, baz = "ABC" } │ + └────────────────────────────────────────┘ + +However, fields can only be terms and cannot be types or kinds + +For example, these record literals are $_NOT valid: + + + ┌───────────────────────────┐ + │ { foo = 100, bar = Text } │ + └───────────────────────────┘ + ⇧ + ❰Text❱ is a type and not a term + + + ┌───────────────────────────┐ + │ { foo = 100, bar = Type } │ + └───────────────────────────┘ + ⇧ + ❰Type❱ is a kind and not a term + + +You provided a record literal with a key named: + +↳ $txt0 + +... whose value is: + +↳ $txt1 + +... which is not a term +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k ) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (InvalidAlternativeType k expr0) = ErrorMessages {..} + where + short = "Invalid alternative" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every union literal begins by selecting one alternative and +specifying the value for that alternative, like this: + + + Select the ❰Left❱ alternative, whose value is ❰True❱ + ⇩ + ┌──────────────────────────────────┐ + │ < Left = True, Right : Natural > │ A union literal with two alternatives + └──────────────────────────────────┘ + + +However, this value must be a term and not a type. For example, the following +values are $_NOT valid: + + + ┌──────────────────────────────────┐ + │ < Left = Text, Right : Natural > │ Invalid union literal + └──────────────────────────────────┘ + ⇧ + This is a type and not a term + + + ┌───────────────────────────────┐ + │ < Left = Type, Right : Type > │ Invalid union type + └───────────────────────────────┘ + ⇧ + This is a kind and not a term + + +You provided a union literal with an alternative named: + +↳ $txt0 + +... whose value is: + +↳ $txt1 + +... which is not a term + +Some common reasons why you might get this error: + +● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one + alternative: + + ┌────────────────────┐ + │ < Example = Text > │ + └────────────────────┘ + ⇧ + This could be ❰:❱ instead +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k ) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (InvalidAlternative k expr0) = ErrorMessages {..} + where + short = "Invalid alternative" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Every union type specifies the type of each alternative, like this: + + + The type of the first alternative is ❰Bool❱ + ⇩ + ┌──────────────────────────────────┐ + │ < Left : Bool, Right : Natural > │ A union type with two alternatives + └──────────────────────────────────┘ + ⇧ + The type of the second alternative is ❰Natural❱ + + +However, these alternatives can only be annotated with types. For example, the +following union types are $_NOT valid: + + + ┌────────────────────────────┐ + │ < Left : Bool, Right : 1 > │ Invalid union type + └────────────────────────────┘ + ⇧ + This is a term and not a type + + + ┌───────────────────────────────┐ + │ < Left : Bool, Right : Type > │ Invalid union type + └───────────────────────────────┘ + ⇧ + This is a kind and not a type + + +You provided a union type with an alternative named: + +↳ $txt0 + +... annotated with the following expression which is not a type: + +↳ $txt1 + +Some common reasons why you might get this error: + +● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one + alternative: + + ┌─────────────────┐ + │ < Example : 1 > │ + └─────────────────┘ + ⇧ + This could be ❰=❱ instead +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k ) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (DuplicateAlternative k) = ErrorMessages {..} + where + short = "Duplicate union alternative" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: Unions may not have two alternatives that share the same name + +For example, the following expressions are $_NOT valid: + + + ┌─────────────────────────────┐ + │ < foo = True | foo : Text > │ Invalid: ❰foo❱ appears twice + └─────────────────────────────┘ + + + ┌───────────────────────────────────────┐ + │ < foo = 1 | bar : Bool | bar : Text > │ Invalid: ❰bar❱ appears twice + └───────────────────────────────────────┘ + + +You have more than one alternative named: + +↳ $txt0 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k) + +prettyTypeMessage (MustCombineARecord expr0 expr1) = ErrorMessages {..} + where + short = "You can only combine records" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can combine records using the ❰∧❱ operator, like this: + + + ┌───────────────────────────────────────────┐ + │ { foo = 1, bar = "ABC" } ∧ { baz = True } │ + └───────────────────────────────────────────┘ + + + ┌─────────────────────────────────────────────┐ + │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │ + └─────────────────────────────────────────────┘ + + +... but you cannot combine values that are not records. + +For example, the following expressions are $_NOT valid: + + + ┌──────────────────────────────┐ + │ { foo = 1, bar = "ABC" } ∧ 1 │ + └──────────────────────────────┘ + ⇧ + Invalid: Not a record + + + ┌───────────────────────────────────────────┐ + │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │ + └───────────────────────────────────────────┘ + ⇧ + Invalid: This is a record type and not a record + + + ┌───────────────────────────────────────────┐ + │ { foo = 1, bar = "ABC" } ∧ < baz = True > │ + └───────────────────────────────────────────┘ + ⇧ + Invalid: This is a union and not a record + + +You tried to combine the following value: + +↳ $txt0 + +... which is not a record, but is actually a value of type: + +↳ $txt1 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (FieldCollision ks) = ErrorMessages {..} + where + short = "Field collision" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can combine records if they don't share any fields in common, +like this: + + + ┌───────────────────────────────────────────┐ + │ { foo = 1, bar = "ABC" } ∧ { baz = True } │ + └───────────────────────────────────────────┘ + + + ┌────────────────────────────────────────┐ + │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │ + └────────────────────────────────────────┘ + + +... but you cannot merge two records that share the same field + +For example, the following expression is $_NOT valid: + + + ┌───────────────────────────────────────────┐ + │ { foo = 1, bar = "ABC" } ∧ { foo = True } │ Invalid: Colliding ❰foo❱ fields + └───────────────────────────────────────────┘ + + +You combined two records that share the following field: + +↳ $txt0 + +... which is not allowed + +Some common reasons why you might get this error: + +● You tried to use ❰∧❱ to update a field's value, like this: + + + ┌────────────────────────────────────────┐ + │ { foo = 1, bar = "ABC" } ∧ { foo = 2 } │ + └────────────────────────────────────────┘ + ⇧ + Invalid attempt to update ❰foo❱'s value to ❰2❱ + + Field updates are intentionally not allowed as the Dhall language discourages + patch-oriented programming +|] + where + txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks)) + +prettyTypeMessage (MustMergeARecord expr0 expr1) = ErrorMessages {..} + where + short = "❰merge❱ expects a record of handlers" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────────────────────────┘ + + +... but the first argument to ❰merge❱ must be a record and not some other type. + +For example, the following expression is $_NOT valid: + + + ┌─────────────────────────────────────────┐ + │ let handler = λ(x : Bool) → x │ + │ in merge handler < Foo = True > : True │ + └─────────────────────────────────────────┘ + ⇧ + Invalid: ❰handler❱ isn't a record + + +You provided the following handler: + +↳ $txt0 + +... which is not a record, but is actually a value of type: + +↳ $txt1 + +Some common reasons why you might get this error: + +● You accidentally provide an empty record type instead of an empty record when + you ❰merge❱ an empty union: + + + ┌──────────────────────────────────────────┐ + │ λ(x : <>) → λ(a : Type) → merge {} x : a │ + └──────────────────────────────────────────┘ + ⇧ + This should be ❰{=}❱ instead +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (MustMergeUnion expr0 expr1) = ErrorMessages {..} + where + short = "❰merge❱ expects a union" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────────────────────────┘ + + +... but the second argument to ❰merge❱ must be a union and not some other type. + +For example, the following expression is $_NOT valid: + + + ┌──────────────────────────────────────────┐ + │ let handlers = { Foo = λ(x : Bool) → x } │ + │ in merge handlers True : True │ + └──────────────────────────────────────────┘ + ⇧ + Invalid: ❰True❱ isn't a union + + +You tried to ❰merge❱ this expression: + +↳ $txt0 + +... which is not a union, but is actually a value of type: + +↳ $txt1 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (UnusedHandler ks) = ErrorMessages {..} + where + short = "Unused handler" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────────────────────────┘ + + +... but you must provide exactly one handler per alternative in the union. You +cannot supply extra handlers + +For example, the following expression is $_NOT valid: + + + ┌───────────────────────────────────────┐ + │ let union = < Left = +2 > │ The ❰Right❱ alternative is missing + │ in let handlers = │ + │ { Left = Natural/even │ + │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't used + │ } │ + │ in merge handlers union : Bool │ + └───────────────────────────────────────┘ + + +You provided the following handlers: + +↳ $txt0 + +... which had no matching alternatives in the union you tried to ❰merge❱ +|] + where + txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks)) + +prettyTypeMessage (MissingHandler ks) = ErrorMessages {..} + where + short = "Missing handler" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────────────────────────┘ + + +... but you must provide exactly one handler per alternative in the union. You +cannot omit any handlers + +For example, the following expression is $_NOT valid: + + + Invalid: Missing ❰Right❱ handler + ⇩ + ┌─────────────────────────────────────────────────┐ + │ let handlers = { Left = Natural/even } │ + │ in let union = < Left = +2 | Right : Bool > │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────┘ + + +Note that you need to provide handlers for other alternatives even if those +alternatives are never used + +You need to supply the following handlers: + +↳ $txt0 +|] + where + txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks)) + +prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) = + ErrorMessages {..} + where + short = "Wrong handler input type" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────────────────────────┘ + + +... as long as the input type of each handler function matches the type of the +corresponding alternative: + + + ┌───────────────────────────────────────────────────────────┐ + │ union : < Left : Natural | Right : Bool > │ + └───────────────────────────────────────────────────────────┘ + ⇧ ⇧ + These must match These must match + ⇩ ⇩ + ┌───────────────────────────────────────────────────────────┐ + │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │ + └───────────────────────────────────────────────────────────┘ + + +For example, the following expression is $_NOT valid: + + + Invalid: Doesn't match the type of the ❰Right❱ alternative + ⇩ + ┌──────────────────────────────────────────────────────────────────────┐ + │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │ + │ in let union = < Left = +2 | Right : Bool > │ + │ in merge handlers union : Bool │ + └──────────────────────────────────────────────────────────────────────┘ + + +Your handler for the following alternative: + +↳ $txt0 + +... needs to accept an input value of type: + +↳ $txt1 + +... but actually accepts an input value of a different type: + +↳ $txt2 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + txt2 = Text.toStrict (Dhall.Core.pretty expr2) + +prettyTypeMessage (HandlerOutputTypeMismatch expr0 expr1 expr2) = + ErrorMessages {..} + where + short = "Wrong handler output type" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────────────────────────┘ + + +... as long as the output type of each handler function matches the declared type +of the result: + + + ┌───────────────────────────────────────────────────────────┐ + │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │ + └───────────────────────────────────────────────────────────┘ + ⇧ ⇧ + These output types ... + + ... must match the declared type of the ❰merge❱ + ⇩ + ┌─────────────────────────────┐ + │ merge handlers union : Bool │ + └─────────────────────────────┘ + + +For example, the following expression is $_NOT valid: + + + ┌──────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Text │ + └──────────────────────────────────────────────────────────────────────┘ + ⇧ + Invalid: Doesn't match output of either handler + + +Your handler for the following alternative: + +↳ $txt0 + +... needs to return an output value of type: + +↳ $txt1 + +... but actually returns an output value of a different type: + +↳ $txt2 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + txt2 = Text.toStrict (Dhall.Core.pretty expr2) + +prettyTypeMessage (HandlerNotAFunction k expr0) = ErrorMessages {..} + where + short = "Handler is not a function" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can ❰merge❱ the alternatives of a union using a record with one +handler per alternative, like this: + + + ┌─────────────────────────────────────────────────────────────────────┐ + │ let union = < Left = +2 | Right : Bool > │ + │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ + │ in merge handlers union : Bool │ + └─────────────────────────────────────────────────────────────────────┘ + + +... as long as each handler is a function + +For example, the following expression is $_NOT valid: + + + ┌─────────────────────────────────────────┐ + │ merge { Foo = True } < Foo = 1 > : Bool │ + └─────────────────────────────────────────┘ + ⇧ + Invalid: Not a function + + +Your handler for this alternative: + +↳ $txt0 + +... has the following type: + +↳ $txt1 + +... which is not the type of a function +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..} + where + short = "Not a record" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can only access fields on records, like this: + + + ┌─────────────────────────────────┐ + │ { foo = True, bar = "ABC" }.foo │ This is valid ... + └─────────────────────────────────┘ + + + ┌───────────────────────────────────────────┐ + │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this + └───────────────────────────────────────────┘ + + +... but you cannot access fields on non-record expressions + +For example, the following expression is $_NOT valid: + + + ┌───────┐ + │ 1.foo │ + └───────┘ + ⇧ + Invalid: Not a record + + +You tried to access a field named: + +↳ $txt0 + +... on the following expression which is not a record: + +↳ $txt1 + +... but is actually an expression of type: + +↳ $txt2 + +Some common reasons why you might get this error: + +● You accidentally try to access a field of a union instead of a record, like + this: + + + ┌─────────────────┐ + │ < foo : a >.foo │ + └─────────────────┘ + ⇧ + This is a union, not a record +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k ) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + txt2 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (MissingField k expr0) = ErrorMessages {..} + where + short = "Missing record field" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: You can only access fields on records, like this: + + + ┌─────────────────────────────────┐ + │ { foo = True, bar = "ABC" }.foo │ This is valid ... + └─────────────────────────────────┘ + + + ┌───────────────────────────────────────────┐ + │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this + └───────────────────────────────────────────┘ + + +... but you can only access fields if they are present + +For example, the following expression is $_NOT valid: + + ┌─────────────────────────────────┐ + │ { foo = True, bar = "ABC" }.qux │ + └─────────────────────────────────┘ + ⇧ + Invalid: the record has no ❰qux❱ field + +You tried to access a field named: + +↳ $txt0 + +... but the field is missing because the record only defines the following fields: + +↳ $txt1 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty k ) + txt1 = Text.toStrict (Dhall.Core.pretty expr0) + +prettyTypeMessage (CantAnd expr0 expr1) = + buildBooleanOperator "&&" expr0 expr1 + +prettyTypeMessage (CantOr expr0 expr1) = + buildBooleanOperator "||" expr0 expr1 + +prettyTypeMessage (CantEQ expr0 expr1) = + buildBooleanOperator "==" expr0 expr1 + +prettyTypeMessage (CantNE expr0 expr1) = + buildBooleanOperator "/=" expr0 expr1 + +prettyTypeMessage (CantTextAppend expr0 expr1) = ErrorMessages {..} + where + short = "❰++❱ only works on ❰Text❱" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱ + +For example, this is a valid use of ❰++❱: + + + ┌────────────────┐ + │ "ABC" ++ "DEF" │ + └────────────────┘ + + +You provided this argument: + +↳ $txt0 + +... which does not have type ❰Text❱ but instead has type: + +↳ $txt1 + +Some common reasons why you might get this error: + +● You might have thought that ❰++❱ was the operator to combine two lists: + + ┌───────────────────────────────────────────────────────────┐ + │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │ Not valid + └───────────────────────────────────────────────────────────┘ + + The Dhall programming language does not provide a built-in operator for + combining two lists +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (CantAdd expr0 expr1) = + buildNaturalOperator "+" expr0 expr1 + +prettyTypeMessage (CantMultiply expr0 expr1) = + buildNaturalOperator "*" expr0 expr1 + +prettyTypeMessage (NoDependentTypes expr0 expr1) = ErrorMessages {..} + where + short = "No dependent types" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: The Dhall programming language does not allow functions from terms +to types. These function types are also known as "dependent function types" +because you have a type whose value "depends" on the value of a term. + +For example, this is $_NOT a legal function type: + + + ┌─────────────┐ + │ Bool → Type │ + └─────────────┘ + + +Similarly, this is $_NOT legal code: + + + ┌────────────────────────────────────────────────────┐ + │ λ(Vector : Natural → Type → Type) → Vector +0 Text │ + └────────────────────────────────────────────────────┘ + ⇧ + Invalid dependent type + + +Your function type is invalid because the input has type: + +↳ $txt0 + +... and the output has kind: + +↳ $txt1 + +... which makes this a forbidden dependent function type +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +prettyTypeMessage (NoDependentLet expr0 expr1) = ErrorMessages {..} + where + short = "No dependent ❰let❱" + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: The Dhall programming language does not allow ❰let❱ expressions +from terms to types. These ❰let❱ expressions are also known as "dependent ❰let❱ +expressions" because you have a type whose value depends on the value of a term. + +The Dhall language forbids these dependent ❰let❱ expressions in order to +guarantee that ❰let❱ expressions of the form: + + + ┌────────────────────┐ + │ let x : t = r in e │ + └────────────────────┘ + + +... are always equivalent to: + + + ┌──────────────────┐ + │ (λ(x : t) → e) r │ + └──────────────────┘ + + +This means that both expressions should normalize to the same result and if one +of the two fails to type check then the other should fail to type check, too. + +For this reason, the following is $_NOT legal code: + + + ┌───────────────────┐ + │ let x = 2 in Text │ + └───────────────────┘ + + +... because the above ❰let❱ expression is equivalent to: + + + ┌─────────────────────────────┐ + │ let x : Integer = 2 in Text │ + └─────────────────────────────┘ + + +... which in turn must be equivalent to: + + + ┌───────────────────────────┐ + │ (λ(x : Integer) → Text) 2 │ + └───────────────────────────┘ + + +... which in turn fails to type check because this sub-expression: + + + ┌───────────────────────┐ + │ λ(x : Integer) → Text │ + └───────────────────────┘ + + +... has type: + + + ┌───────────────────────┐ + │ ∀(x : Integer) → Text │ + └───────────────────────┘ + + +... which is a forbidden dependent function type (i.e. a function from a term to +a type). Therefore the equivalent ❰let❱ expression is also forbidden. + +Your ❰let❱ expression is invalid because the input has type: + +↳ $txt0 + +... and the output has kind: + +↳ $txt1 + +... which makes this a forbidden dependent ❰let❱ expression +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + +buildBooleanOperator :: Text -> Expr s X -> Expr s X -> ErrorMessages +buildBooleanOperator operator expr0 expr1 = ErrorMessages {..} + where + short = + Builder.fromText + (Data.Text.strip + [NeatInterpolation.text|❰$txt2❱ only works on ❰Bool❱s|] ) + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: The ❰$txt2❱ operator expects two arguments that have type ❰Bool❱ + +For example, this is a valid use of ❰$txt2❱: + + + ┌───────────────┐ + │ True $txt2 False │ + └───────────────┘ + + +You provided this argument: + +↳ $txt0 + +... which does not have type ❰Bool❱ but instead has type: + +↳ $txt1 +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + + txt2 = Text.toStrict operator + +buildNaturalOperator :: Text -> Expr s X -> Expr s X -> ErrorMessages +buildNaturalOperator operator expr0 expr1 = ErrorMessages {..} + where + short = + Builder.fromText + (Data.Text.strip + [NeatInterpolation.text|❰$txt2❱ only works on ❰Natural❱s|] ) + + long = + Builder.fromText [NeatInterpolation.text| +Explanation: The ❰$txt2❱ operator expects two arguments that have type ❰Natural❱ + +For example, this is a valid use of ❰$txt2❱: + + + ┌─────────┐ + │ +3 $txt2 +5 │ + └─────────┘ + + +You provided this argument: + +↳ $txt0 + +... which does not have type ❰Natural❱ but instead has type: + +↳ $txt1 + +Some common reasons why you might get this error: + +● You might have tried to use an ❰Integer❱, which is $_NOT allowed: + + + ┌─────────────────────────────────────────┐ + │ λ(x : Integer) → λ(y : Integer) → x $txt2 y │ Not valid + └─────────────────────────────────────────┘ + + + You can only use ❰Natural❱ numbers + + +● You might have mistakenly used an ❰Integer❱ literal, which is $_NOT allowed: + + + ┌───────┐ + │ 2 $txt2 2 │ Not valid + └───────┘ + + + You need to prefix each literal with a ❰+❱ to transform them into ❰Natural❱ + literals, like this: + + + ┌─────────┐ + │ +2 $txt2 +2 │ Valid + └─────────┘ +|] + where + txt0 = Text.toStrict (Dhall.Core.pretty expr0) + txt1 = Text.toStrict (Dhall.Core.pretty expr1) + + txt2 = Text.toStrict operator + +-- | A structured type error that includes context +data TypeError s = TypeError + { context :: Context (Expr s X) + , current :: Expr s X + , typeMessage :: TypeMessage s + } deriving (Typeable) + +instance Buildable s => Show (TypeError s) where + show = Text.unpack . Dhall.Core.pretty + +instance (Buildable s, Typeable s) => Exception (TypeError s) + +instance Buildable s => Buildable (TypeError s) where + build (TypeError ctx expr msg) + = ( if Text.null (Builder.toLazyText (buildContext ctx)) + then "" + else buildContext ctx <> "\n" + ) + <> shortTypeMessage msg <> "\n" + <> source + where + buildKV (key, val) = build key <> " : " <> build val + + buildContext = + build + . Text.unlines + . map (Builder.toLazyText . buildKV) + . reverse + . Dhall.Context.toList + + source = case expr of + Note s _ -> build s + _ -> mempty + +newtype DetailedTypeError s = DetailedTypeError (TypeError s) + deriving (Typeable) + +instance Buildable s => Show (DetailedTypeError s) where + show = Text.unpack . Dhall.Core.pretty + +instance (Buildable s, Typeable s) => Exception (DetailedTypeError s) + +instance Buildable s => Buildable (DetailedTypeError s) where + build (DetailedTypeError (TypeError ctx expr msg)) + = ( if Text.null (Builder.toLazyText (buildContext ctx)) + then "" + else buildContext ctx <> "\n" + ) + <> longTypeMessage msg <> "\n" + <> "────────────────────────────────────────────────────────────────────────────────\n" + <> "\n" + <> source + where + buildKV (key, val) = build key <> " : " <> build val + + buildContext = + build + . Text.unlines + . map (Builder.toLazyText . buildKV) + . reverse + . Dhall.Context.toList + + source = case expr of + Note s _ -> build s + _ -> mempty