blob: fdc65b45876f90c07a16eef14898d5ba083e75cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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
|
