blob: bd7d483b18d7fed414aeda5005a160799e28165a (
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
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
|
