diff options
author | Nadrieril | 2019-03-01 17:28:19 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-01 17:28:19 +0100 |
commit | e5d9aee00b0c775df1d8e2d8819aeb80dffa73c2 (patch) | |
tree | e763a24a0d635048232e72e167ca37eafec69369 /src/errors/NoDependentLet.txt | |
parent | 8a2b7536902831079eddd7b00291b718f5dd7186 (diff) |
Split abnf_to_pest and dhall into their own crates
Diffstat (limited to 'src/errors/NoDependentLet.txt')
-rw-r--r-- | src/errors/NoDependentLet.txt | 76 |
1 files changed, 0 insertions, 76 deletions
diff --git a/src/errors/NoDependentLet.txt b/src/errors/NoDependentLet.txt deleted file mode 100644 index fdc65b4..0000000 --- a/src/errors/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 |