Implement typing and familiar data structures in λ calculus.
All we have is functions and names, but no restrictions on
operations between them: e.g.
iszero true ==>
λ n (n select-first) true ==>
true select-first ==
λ first. λ second. first select-first ==>
λ second. select-first ==
λ second. λ first. λ second. first}
a function of 3 args that returns 2nd... but it seems
pretty meaning- and useless.
Bad old days: Machine code and BCPL. Need types for familiar reasons. Ultimately, get Java that is very rule-bound about types.
Typed objects have a type and a value.
Construct them, extract value or type, test the type, and handle type errors.
One idea: use integers to represent types and to use numerical comparison for type-checking.
λ calculus implementation: pair functions (of course):
Typed objects represented as type-value pairs.
def make-obj type value = λ s. (s type value)
def type obj = obj select-first
def value obj = obj select-second
Define (dynamically) typed objs, ops, in terms of untyped:
Start with untyped operations, which is what we have (and like machine code), but only use typed ops on typed args to avoid overriding checks. Use UPPER CASE LETTERS for typed constructs, lower for untyped.
Type errors can be represented by integers, say:
def error-type = zero
def MAKE-ERROR = make-obj error-type
which expands as
make-obj error-type ==
λ type. λ value. λ s. (s type value )
error-type =>
λ value. λ s. (s error-type value).
Then can define ERROR, iserror, etc..
Go on to implement and check for type errors, and how to implement typed booleans, conditionals, numbers and arithmetic, and characters. Static and dynamic type-checking.
Booleans, types
def bool-type = one
def MAKE-BOOL = make-obj bool-type ==
λ value. λ s. (s bool-type value)
def TRUE = MAKE-BOOL true ==
λ s. (s bool-type true)
def FALSE = MAKE-BOOL false ==
λ s. (s bool-type false)
def isbool = istype bool-type ==
λ obj. (equal(type obj) bool-type)...
Boolean Function Example
def NOT X =
if isbool X
then MAKE-BOOL (not(value X))
else BOOL-ERROR
Normal approach: with MAKE-NUMB, error object, isnumb, etc. then:
def SUCC N =
if isnumb N
then MAKE-NUMB(succ(value N))
else NUMB-ERROR
Numbers...
def 1 = SUCC 0
def 2 = SUCC 1
...
So 1 expands to an isnumb test
(7 or so lines to derive true) and a MAKE-NUMB,
which takes 8 lines to turn into
λ s. (s numb-type one).
Allow Infix: add rewrite rules like
< exp1 > AND < exp2 > == AND < exp1 > < exp2 >,
similarly for OR, +, -, *, /. No precedence or associativity.
Type structures: Lists of definitions: e.g. Booleans are
defined as lists of definitions, and Boolean
functions are too:
NOT TRUE = FALSE
NOT FALSE = TRUE
But to implement the definition we use conditionals:
def NOT X =
IF X
THEN FALSE
ELSE TRUE
Henceforth, we can define Boolean functions by using TRUE and FALSE
in place of X
with this sort of notation:
def NOT TRUE = FALSE
or NOT FALSE = TRUE
...another e.g.
def IMPLIES TRUE Y = Y
or IMPLIES FALSE Y = TRUE
When a fn with multi-case def. applied to arg, the arg is matched against the structured bound variable (or constant or constructor sequences) to see which case applies: use the bound variables from that case. Structure Matching!.
In our functional notation, we have to use conditional expressions explicitly to determine
the structure and figure out the case, then use explicit selection of
substructures from structured arguments.
Recall that PROLOG does structure-matching directly (through
unification), and
uses structured arguments like
FOO([X | L], [H | T]).
We'll extend our emerging λ-calculus-based
language to include structure matching (purely through syntactic
sugaring).
We've seen the syntax for cases (our e.g.: Booleans) --
IF-THEN-ELSE, def or.
With numbers, we allow zero and bound variables qualified by nested
SUCCs in place of b.v.s: e.g. sum of first X ints:
SUM 0 = 0
SUM (SUCC X) = (SUCC X) + SUM(X)
Which we had to write
rec SUM X =
IF ISZERO X
THEN 0
ELSE X + (SUM(PRED(X))
We can now write
rec SUM 0 = 0
or SUM (SUCC X) = (SUCC X) + SUM(X)
...similarly
rec POWER X 0 = 1
or POWER X (SUCC Y) = X*(POWER X Y)
The list data structure holds a variable length sequence of values. We can develop list constructors and accessors using pair functions (AGAIN!!).
Obviously, the pair represents the HEAD and TAIL (CAR, CDR) of the list. It is fairly straightforward to introduce simpler list notation and produce needed list utilities, including list comparison, indexed access (a,k.a arrays), and mapping functions (like mapcar in Scheme or LISP.) Strings can be represented as lists of characters, and we can even work out numeric string to number conversion.
def CONS H T ==
if islist T
then MAKE-LIST λ s . (s H T)
else LIST-ERROR
...and our fave
rec APPEND L1 L2 =
IF (ISNIL L1)
THEN L2
ELSE CONS (HEAD L1) (APPEND (TAIL L1) L2)
A new Prolog-like notation for lists is easy to define:
:: for CONS, [ ] to delimit lists,
NIL == [], etc.
Flatten [[1,2],3] goes to [1,2,3]. Empty list is flat, if head is not
a list join it to flattened tail, else append flattened head to
flattened tail.
rec FLAT [] = []
or FLAT(H::T) =
IF NOT (ISLIST H)
THEN H::(FLAT T)
ELSE APPEND (FLAT H) (FLAT T)
Note, in LISP, no case definitions OR structure matching: explicit list selection is necessary.
Generally, objects are defined by a constant base cases and structured recursion cases, so their definitions have base cases with constants for matching constant arguments, and recursion cases with structured bound variables for matching structured arguments (above, [] and [H::T]).
Use lists for ``structs'' (as in Prolog, Scheme, LISP...). Need accessors and updaters.
Generalize structure matching by using selector functions and allowing arbitrary bound variable lists that include explicit or implicit empty lists.
Important operations (e.g. sorting, searching) inefficient with lists: introduce trees.
We won't do any details here: they are quite straightforward and methodical and the result is we can implement all our CSC172 algorithms on linked lists and trees.
EXAMPLE:
E.g. of generalized structure matching and
a new list notation: Here's
three-field record for stock control:
< < item-name > , < stock-level >,
< reorder-level > >
Define selector functions:
def ITEM [I,S,R] = I
def STOCK [I,S,R] = S
def REORDER [I,S,R] = R
The bound variable list is a list, i.e. ends with NIL, so
[I,S,R] == I::S::R::NIL.
This matches the argument and we get assignment of I
as item-name function, etc.
Bound variable [I,S,R]::T matches a list with T
matching the TAIL of the list (Prolog-like).
A function to find all items whose level is
below the reorder level recursively builds and returns
a list of such records.
rec REORD [] 0
or REORD ([I,S,R]:T) =
IF LESS S R
THEN [I,S,R]::(REORD T)
ELSE REORD T
DESIRE: notation for local variables, which are of course name-value associations for use within an expression.
HOW? What do you think?
HINT: There's only two things it can be: abstraction or application.
Consider:
λ < name >. < body > < argument >
Requires replacement of all free occurrences of
< name >
in < body > with < argument > before evaluating
< body >.
Just what we want from a local variable, no? We use
let < name > = < argument > in < body >
to express the "local variable" semantics of this application
(variable binding).
P.S. We've seen Scheme uses exactly this implementation for let!
May see this in readings. Haskell Curry noticed you can implement a nest of single-argument function calls with one multi-argument function call and vice-versa.
E.g.
Converting
curried function
to uncurried
function and back is easy. The curried one is the nested one with single
arguments.
Thus by using the currying function we can now write
def SUM-SQ1 [X,Y] = (X*X) + (Y*Y)
(We've come a long way!
looks like a
(weakly) typed programming
language, (but we know it's all just functions!)
Recall: def curry f x y = f [x,y]
Now if: def curry-SUM-SQ = curry SUM-SQ1
RHS expands to
λ f. λ x. λ y. (f [x,y]) SUM-SQ1 =>
λ x. λ y. (SUM-SQ1 [x,y])
so
def curry-SUM-SQ x y = SUM-SQ1 [x,y]
thus the nested, curried form is the same as the argument-list form.
Likewise
def uncurry g [a,b] = g a b
works in reverse.
Common in λ calculus since we've used it from the start! Generally, idea is to create a new function from a multi-argument function by supplying some of its arguments.
Happens automagically with nested single-argument functions.
Lots of ILs don't allow
functions as objects: can't get new functions by
partial application: instead, obvious ploy:
New fn calls old one with parameters frozen in:
function add-1 (x)
return add(1,x);
we have now developed a rather high-level, weakly-typed functional language that actually begins to look like, say, Scheme.
Recall we can always get back to pure λ calculus by simple, unambiguous substitution rules.
The appearance of a big ontology of functions, values, structures... but they're really all pure λ functions interpreted in different ways. All these things are ``really'' the same and therefore we can't type-check them -- so we can't for instance constrain selector and constructor functions for data structures to have appropriate arguments.
Our weak type-checking will detect some clashes when functions are evaluated, but in principle we can still apply anything to anything else, which definitely will produce a fine λ expression --- but it may not have any plausible interpretation.
(< name > < argument >) ==
( < function > < argument >)
We'll soon have names for functions like identity and concepts like true two,...
For your sanity and success remember NEVER to expand a name until it is the function you want to apply, as above!
This saves you from useless and dangerous copying of complex substructure that is best notated by its simple name.
E.g.
(self-apply ((apply identity) apply)) ==
(λs. (s s) ((apply identity) apply))
Not
(self-apply ((apply identity) apply)) ==
(self-apply ((λ func. λ arg. (func arg)
identity) apply)
BUT...! With applicative order, we'll have the luxury of
evaluating arguments before functions. Then it's a judgement call,
but often useful to do that. Here, clearly, (with -> as a new
notation
for applicative order reduction):
(self-apply ((apply identity) apply)) ->
(self-apply apply)