diff options
Diffstat (limited to 'dhall')
34 files changed, 0 insertions, 1765 deletions
diff --git a/dhall/src/error/text/AnnotMismatch.txt b/dhall/src/error/text/AnnotMismatch.txt deleted file mode 100644 index 4904bf8..0000000 --- a/dhall/src/error/text/AnnotMismatch.txt +++ /dev/null @@ -1,117 +0,0 @@ -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❱ diff --git a/dhall/src/error/text/CantTextAppend.txt b/dhall/src/error/text/CantTextAppend.txt deleted file mode 100644 index 26b9ceb..0000000 --- a/dhall/src/error/text/CantTextAppend.txt +++ /dev/null @@ -1,28 +0,0 @@ -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 diff --git a/dhall/src/error/text/DuplicateAlternative.txt b/dhall/src/error/text/DuplicateAlternative.txt deleted file mode 100644 index 077f8aa..0000000 --- a/dhall/src/error/text/DuplicateAlternative.txt +++ /dev/null @@ -1,18 +0,0 @@ -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 diff --git a/dhall/src/error/text/FieldCollision.txt b/dhall/src/error/text/FieldCollision.txt deleted file mode 100644 index 2b2d260..0000000 --- a/dhall/src/error/text/FieldCollision.txt +++ /dev/null @@ -1,43 +0,0 @@ -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 diff --git a/dhall/src/error/text/HandlerInputTypeMismatch.txt b/dhall/src/error/text/HandlerInputTypeMismatch.txt deleted file mode 100644 index 7d3525b..0000000 --- a/dhall/src/error/text/HandlerInputTypeMismatch.txt +++ /dev/null @@ -1,49 +0,0 @@ -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 diff --git a/dhall/src/error/text/HandlerNotAFunction.txt b/dhall/src/error/text/HandlerNotAFunction.txt deleted file mode 100644 index ff87443..0000000 --- a/dhall/src/error/text/HandlerNotAFunction.txt +++ /dev/null @@ -1,32 +0,0 @@ -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 diff --git a/dhall/src/error/text/HandlerOutputTypeMismatch.txt b/dhall/src/error/text/HandlerOutputTypeMismatch.txt deleted file mode 100644 index f359459..0000000 --- a/dhall/src/error/text/HandlerOutputTypeMismatch.txt +++ /dev/null @@ -1,51 +0,0 @@ -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 diff --git a/dhall/src/error/text/IfBranchMismatch.txt b/dhall/src/error/text/IfBranchMismatch.txt deleted file mode 100644 index a95b130..0000000 --- a/dhall/src/error/text/IfBranchMismatch.txt +++ /dev/null @@ -1,63 +0,0 @@ -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 diff --git a/dhall/src/error/text/IfBranchMustBeTerm.txt b/dhall/src/error/text/IfBranchMustBeTerm.txt deleted file mode 100644 index 4c15881..0000000 --- a/dhall/src/error/text/IfBranchMustBeTerm.txt +++ /dev/null @@ -1,51 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidAlterantive.txt b/dhall/src/error/text/InvalidAlterantive.txt deleted file mode 100644 index 391fc3a..0000000 --- a/dhall/src/error/text/InvalidAlterantive.txt +++ /dev/null @@ -1,48 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidAlterantiveType.txt b/dhall/src/error/text/InvalidAlterantiveType.txt deleted file mode 100644 index f5dadef..0000000 --- a/dhall/src/error/text/InvalidAlterantiveType.txt +++ /dev/null @@ -1,49 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidField.txt b/dhall/src/error/text/InvalidField.txt deleted file mode 100644 index bfbf106..0000000 --- a/dhall/src/error/text/InvalidField.txt +++ /dev/null @@ -1,35 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidFieldType.txt b/dhall/src/error/text/InvalidFieldType.txt deleted file mode 100644 index 4f76a64..0000000 --- a/dhall/src/error/text/InvalidFieldType.txt +++ /dev/null @@ -1,34 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidInputType.txt b/dhall/src/error/text/InvalidInputType.txt deleted file mode 100644 index eabafa4..0000000 --- a/dhall/src/error/text/InvalidInputType.txt +++ /dev/null @@ -1,61 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidListElement.txt b/dhall/src/error/text/InvalidListElement.txt deleted file mode 100644 index 59db7b7..0000000 --- a/dhall/src/error/text/InvalidListElement.txt +++ /dev/null @@ -1,30 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidListType.txt b/dhall/src/error/text/InvalidListType.txt deleted file mode 100644 index 676647e..0000000 --- a/dhall/src/error/text/InvalidListType.txt +++ /dev/null @@ -1,43 +0,0 @@ -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❱ diff --git a/dhall/src/error/text/InvalidOptionType.txt b/dhall/src/error/text/InvalidOptionType.txt deleted file mode 100644 index 3bc81de..0000000 --- a/dhall/src/error/text/InvalidOptionType.txt +++ /dev/null @@ -1,44 +0,0 @@ -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❱ - diff --git a/dhall/src/error/text/InvalidOptionalElement.txt b/dhall/src/error/text/InvalidOptionalElement.txt deleted file mode 100644 index 0254220..0000000 --- a/dhall/src/error/text/InvalidOptionalElement.txt +++ /dev/null @@ -1,29 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidOptionalLiteral.txt b/dhall/src/error/text/InvalidOptionalLiteral.txt deleted file mode 100644 index 41c0fdc..0000000 --- a/dhall/src/error/text/InvalidOptionalLiteral.txt +++ /dev/null @@ -1,53 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidOutputType.txt b/dhall/src/error/text/InvalidOutputType.txt deleted file mode 100644 index dd2695d..0000000 --- a/dhall/src/error/text/InvalidOutputType.txt +++ /dev/null @@ -1,68 +0,0 @@ -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 diff --git a/dhall/src/error/text/InvalidPredicate.txt b/dhall/src/error/text/InvalidPredicate.txt deleted file mode 100644 index 4c15881..0000000 --- a/dhall/src/error/text/InvalidPredicate.txt +++ /dev/null @@ -1,51 +0,0 @@ -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 diff --git a/dhall/src/error/text/MissingField.txt b/dhall/src/error/text/MissingField.txt deleted file mode 100644 index de14a33..0000000 --- a/dhall/src/error/text/MissingField.txt +++ /dev/null @@ -1,30 +0,0 @@ -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 diff --git a/dhall/src/error/text/MissingHandler.txt b/dhall/src/error/text/MissingHandler.txt deleted file mode 100644 index 433445e..0000000 --- a/dhall/src/error/text/MissingHandler.txt +++ /dev/null @@ -1,32 +0,0 @@ -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 diff --git a/dhall/src/error/text/MustCombineARecord.txt b/dhall/src/error/text/MustCombineARecord.txt deleted file mode 100644 index 141b969..0000000 --- a/dhall/src/error/text/MustCombineARecord.txt +++ /dev/null @@ -1,46 +0,0 @@ -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: - -↳ $txt1 diff --git a/dhall/src/error/text/MustMergeARecord.txt b/dhall/src/error/text/MustMergeARecord.txt deleted file mode 100644 index 79094bd..0000000 --- a/dhall/src/error/text/MustMergeARecord.txt +++ /dev/null @@ -1,43 +0,0 @@ -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 diff --git a/dhall/src/error/text/MustMergeUnion.txt b/dhall/src/error/text/MustMergeUnion.txt deleted file mode 100644 index 68df70c..0000000 --- a/dhall/src/error/text/MustMergeUnion.txt +++ /dev/null @@ -1,31 +0,0 @@ -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 diff --git a/dhall/src/error/text/NoDependentLet.txt b/dhall/src/error/text/NoDependentLet.txt deleted file mode 100644 index fdc65b4..0000000 --- a/dhall/src/error/text/NoDependentLet.txt +++ /dev/null @@ -1,76 +0,0 @@ -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 diff --git a/dhall/src/error/text/NoDependentTypes.txt b/dhall/src/error/text/NoDependentTypes.txt deleted file mode 100644 index 435bdcb..0000000 --- a/dhall/src/error/text/NoDependentTypes.txt +++ /dev/null @@ -1,31 +0,0 @@ -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 diff --git a/dhall/src/error/text/NotAFunction.txt b/dhall/src/error/text/NotAFunction.txt deleted file mode 100644 index dd2695d..0000000 --- a/dhall/src/error/text/NotAFunction.txt +++ /dev/null @@ -1,68 +0,0 @@ -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 diff --git a/dhall/src/error/text/NotARecord.txt b/dhall/src/error/text/NotARecord.txt deleted file mode 100644 index e0eebc8..0000000 --- a/dhall/src/error/text/NotARecord.txt +++ /dev/null @@ -1,48 +0,0 @@ -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 diff --git a/dhall/src/error/text/TypeMismatch.txt b/dhall/src/error/text/TypeMismatch.txt deleted file mode 100644 index 4904bf8..0000000 --- a/dhall/src/error/text/TypeMismatch.txt +++ /dev/null @@ -1,117 +0,0 @@ -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❱ diff --git a/dhall/src/error/text/UnboundVariable.txt b/dhall/src/error/text/UnboundVariable.txt deleted file mode 100644 index bd7d483..0000000 --- a/dhall/src/error/text/UnboundVariable.txt +++ /dev/null @@ -1,97 +0,0 @@ -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 diff --git a/dhall/src/error/text/Untyped.txt b/dhall/src/error/text/Untyped.txt deleted file mode 100644 index 4904bf8..0000000 --- a/dhall/src/error/text/Untyped.txt +++ /dev/null @@ -1,117 +0,0 @@ -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❱ diff --git a/dhall/src/error/text/UnusedHandler.txt b/dhall/src/error/text/UnusedHandler.txt deleted file mode 100644 index 2e46a12..0000000 --- a/dhall/src/error/text/UnusedHandler.txt +++ /dev/null @@ -1,32 +0,0 @@ -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❱ |