-
Notifications
You must be signed in to change notification settings - Fork 36
/
Copy pathextra.lhs
203 lines (154 loc) · 7.27 KB
/
extra.lhs
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
## Evaluating First-Class Functions by Substitution
[This section might be useful if I decide to cover the
normal implementation of lambda-calculus using beta reduction]
Now its time for write a semantics for a language with
first-class functions. Since we have seen that booleans,
integers and other data types can be represented by functions,
there is no reason to include them in the language. What
remains are just variables, functions (lambda expressions),
and function application.
> data Exp'9 = Variable'9 String -- variables
> | Function'9 String Exp'9 -- function creation
> | Call'9 Exp'9 Exp'9 -- function call
This is exactly the abstract syntax of
the *lambda calculus*, as defined by Church in the 1930s.
As we will see in (TODO: reference Church Encodings), we don't need to
define a type of *values* because we are going to use
lambda expressions as the values.
Church defined the semantics of lambda calculus using
substitution.
We introduced substitution for arithmetic
expressions in [Chapter 1](#BasicSubst) so that you would familiar with
the concept by the time we got here.
Substitution for
lambda expressions is a little more complex, however.
In the previous approach we substituted variables for
values in expressions, but now we will substitute variables
for expressions in expressions.
> substitute'9 :: String -> Exp'9 -> Exp'9 -> Exp'9
> substitute'9 var exp target = subst target
> where
> -- uses subst function defined in the next few paragraphs
Since expressions can
contain variables, we will have to be more careful.
The first case, for substitution into a variable
expression, is the same as previous cases:
> subst (Variable'9 name) =
> if var == name then exp else Variable'9 name
The second case is substitution into a function call. It just
substitutes into the function and the argument:
> subst (Call'9 fun arg) =
> Call'9 (subst fun) (subst arg)
The last case is substitution *into* a lambda expression.
This case is similar to the case of substitution into
a |let| expression (TODO: reference chapter), because
both a |let| and a lambda introduce a new variable name.
Here is a first attempt at substituting *into* a lambda
expression.
````
-- first version is not quite correct
subst (Function'9 name body) =
if var == name
then Function'9 name body
else Function'9 name (subst body)
````
This version properly handles *shadowing* of the outer
|var| by the |name| bound in the lambda: if the names are
the same, then substitution does not occur in the body.
Consider some cases that this handles correctly:
* Substitute $x \mapsto 5$ in $\lambda f.f(x)$ \ \ \ $\Rightarrow$ \ \ \ $\lambda f.f(5)$
* Substitute $x \mapsto 5$ in $\lambda x.f(x)$ \ \ \ $\Rightarrow$ \ \ \ $\lambda x.f(x)$
* Substitute $x \mapsto y$ in $\lambda f.f(x)$ \ \ \ $\Rightarrow$ \ \ \ $\lambda f.f(y)$
* Substitute $f \mapsto \lambda z.z+3$ in $\lambda x.f(x)$ \ \ \ $\Rightarrow$ \ \ \ $\lambda x.(\lambda z.z+3)(x)$
* Substitute $f \mapsto \lambda z.z+3$ in $\lambda z.f(z)$ \ \ \ $\Rightarrow$ \ \ \ $\lambda z.(\lambda z.z+3)(z)$
However, this version does *not* properly handle the case
where the |exp| being substituted has free variables!
Here is a case that does not work correctly:
* Substitute $y \mapsto x*2$ in $\lambda x.y+x$ \ \ \ $\Rightarrow$ \ \ \ $\lambda x.(x*2)+x$
The problem here is that the $x+1$ in the expression being substituted
is a free variable, but it becomes bound in the result because it is
substituted into the body of a lambda that uses the same variable name.
They aren't really the same variable, even though they have the same name!
One way to see that they are not the same variable is to rename
the bound occurrence of $x$ to be some other variable name, $m$.
* Substitute $y \mapsto x*2$ in $\lambda m.y+m$ \ \ \ $\Rightarrow$ \ \ \ $\lambda m.(x*2)+m$
In this case the substitution is correct.
When a variable that was free ends up becoming bound, it is called *variable capture*.
*variable capture* has never been a problem in any previous versions of
substitution that we have discussed, because all previous
cases of substitution have involved substitution of a
variable for a *value*, and values do not have variables in them.
The definition of substitution is it must replace all
*free* occurrences of a variable with a new value, and that
all variables that are *free* in either the target or expression
being substituted must remain free. In other words, substitution must
avoid variable capture.
The solution to variable capture identified above was to rename
the bound variable if variable capture is about to happen.
> subst (Function'9 name body) =
> if var == name
> then Function'9 name body
> else Function'9 name' (subst body')
> where Function'9 name' body' = avoid_capture var exp (Function'9 name body)
> avoid_capture var exp (Function'9 name body) =
> if elem name (free_vars exp)
> then let name' = new_variable (Call'9 exp body) in
> Function'9 name' (substitute'9 name (Variable'9 name') body)
> else Function'9 name body
TODO: need to define these property!
> new_variable exp = "foo"
> free_vars exp = []
### Other Junk
Here is a typical example of a program that uses mutable state,
written in JavaScript:
````Java
var count = 0;
function makeVar() {
count = count + 1;
return "v" + count;
}
````
It declares a global variable named |count| with inital value |0| and defines a
funtion |makeVar| that returns a new variable name each time
it is called. The function |count| works by incrementing the
|count| and then returning a string formed by concatenating the
letter |"v"| with the string representation of |count|. Running
|makeVar| is easy, as it produces a new variable name each time it is
executed:
```Java
print( makeVar() ); // print "v1"
print( makeVar() ); // print "v3"
print( makeVar() ); // print "v4"
```
The use of global variables is poor programming style.
A fix for this problem appears later, in section on Objects (TODO:REF).
Mutable state is not possible in pure functional
languages, including Haskell, because there is no way to modify a
data structure or variable value after is has been constructed
or bound. But it is possible to compute a new data struture
that is based on an existing one. This is the notion of
*functional update* or *functional change*: a function can
act as a transformation of a value into a new value.
This idea can be used to implement a pure functional version of
|makeVar|. The pure functional version of |makeVar| will
take *as an input* the current value of the counter, and it
will produce as outputs the new variable name *and* the
updated counter.
> makeVar count =
> let count' = count + 1 in
> ("v" ++ show count', count')
The |count| variable is now an explicit input and output of the
function, rather than a global variable. The fact that the
counter is now explicit is evident in the type of |makeVar|:
> makeVar :: Int -> (String, Int)
Calling the pure version of |makeVar| is not so easy, because it
requires and extra input and produces an extra output:
> main'99 = do
> let c0 = 0
> let (var1, c1) = makeVar c0
> print var1
> let (var2, c2) = makeVar c1
> print var2
> let (var3, c3) = makeVar c1
> print var3
To simulate the behavior of |makeVar|, for example,