diff options
author | Nadrieril | 2019-05-07 18:12:04 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-07 18:12:04 +0200 |
commit | 3da450aa3fae23214aa982643b9bc4dd0ea4eaa6 (patch) | |
tree | 02e00cd008d2e7dc899b9211379596fe792f41c8 /dhall/src/error/text/NoDependentLet.txt | |
parent | d8a3e831fb67f86269c4baa99f9f0798a73a7247 (diff) | |
parent | 14dfeb8e7d2aa87a361a711a485243449426b144 (diff) |
Merge branch 'reorganize'
Diffstat (limited to 'dhall/src/error/text/NoDependentLet.txt')
-rw-r--r-- | dhall/src/error/text/NoDependentLet.txt | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/dhall/src/error/text/NoDependentLet.txt b/dhall/src/error/text/NoDependentLet.txt new file mode 100644 index 0000000..fdc65b4 --- /dev/null +++ b/dhall/src/error/text/NoDependentLet.txt @@ -0,0 +1,76 @@ +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 |