diff options
| -rw-r--r-- | examples/gfcc/complin.tex | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/examples/gfcc/complin.tex b/examples/gfcc/complin.tex index 324c97e11..accad0bda 100644 --- a/examples/gfcc/complin.tex +++ b/examples/gfcc/complin.tex @@ -304,6 +304,17 @@ Here is an example of a piece of code and its abstract syntax. The details of expression and type syntax will be explained in the next section. +Our binding syntax is more liberal than C's in two ways. +First, +lambda calculus permits overshadowing previous bindings +by new ones, e.g. to write \verb6\x -> (\x -> f x)6. +The corresponding overshadowing of declarations is not +legal in C, within one and the same block. +Secondly, we allow declarations anywhere in a block, +not just in the beginning. +The second deviation would be easy to mend, whereas +the first one is inherent to the method of \HOAS. + \subsection{Types and expressions} |