Higher-order functions --- those that take functions as arguments or return functions as results --- are powerful tools for building programs. An interesting application of higher-order functions is to implement infinite sequences of values as (total) functions from the natural numbers (non-negative integers) to the type of values of the sequence. We will develop a small package of operations for creating and manipulating sequences, all of which are higher-order functions since they take sequences (functions!) as arguments and/or return them as results. A natural way to define many sequences is by recursion, or self-reference. Since sequences are functions, we may use recursive function definitions to define such sequences. Alternatively, we may think of such a sequence as arising from a "loopback" or "feedback" construct. We will explore both approaches.
Sequences may be used to simulate digital circuits by thinking of a "wire" as a sequence of bits developing over time. The ith value of the sequence corresponds to the signal on the wire at time i. For simplicity we will assume a perfect waveform: the signal is always either high or low (or is undefined); we will not attempt to model electronic effects such as attenuation or noise. Combinational logic elements (such as and gates or inverters) are operations on wires: they take in one or more wires as input and yield one or more wires as results. Digital logic elements (such as flip-flops) are obtained from combinational logic elements by feedback, or recursion --- a flip-flop is a recursively-defined wire!
Let us begin by developing a sequence package. Here is a suitable signature defining the type of sequences:
signature SEQUENCE = sig
type 'a seq = int -> 'a
val constantly : 'a -> 'a seq (* constant sequence *)
val alternately : 'a * 'a -> 'a seq (* alternating values *)
val insert : 'a * 'a seq -> 'a seq (* insert an element at the front *)
val map : ('a -> 'b) -> 'a seq -> 'b seq
val zip : 'a seq * 'b seq -> ('a * 'b) seq
val unzip : ('a * 'b) seq -> 'a seq * 'b seq
val merge : ('a * 'a) seq -> 'a seq (* fair merge *)
val stretch : int -> 'a seq -> 'a seq
val shrink : int -> 'a seq -> 'a seq
val take : int -> 'a seq -> 'a list
val drop : int -> 'a seq -> 'a seq
val shift : 'a seq -> 'a seq
val loopback : ('a seq -> 'a seq) -> 'a seq
end
Observe that we expose the representation of sequences as functions. This is done
to simplify the definition of recursive sequences as recursive functions.
Alternatively we could have hidden the representation type, at the expense of making it a
bit more awkward to define recursive sequences. In the absence of this exposure of
representation, recursive sequences may only be built using the loopback
operation which constructs a recursive sequence by "looping back" the output of
a sequence transformer to its input. Most of the other operations of the signature
are adaptations of familiar operations on lists. Two exceptions to this rule are the
functions stretch
and shrink
that dilate and contract the
sequence by a given time parameter --- if a sequence is expanded by k, its value
at i is the value of the original sequence at i/k, and dually for
shrinking.
Here's an implementation of sequences as functions.
structure Sequence :> SEQUENCE = struct
type 'a seq = int -> 'a
fun constantly c n = c
fun alternately (c,d) n = if n mod 2 = 0 then c else d
fun insert (x, s) 0 = x
| insert (x, s) n = s (n-1)
fun map f s = f o s
fun zip (s1, s2) n = (s1 n, s2 n)
fun unzip (s : ('a * 'b) seq) = (map #1 s, map #2 s)
fun merge (s1, s2) n =
(if n mod 2 = 0 then s1 else s2) (n div 2)
fun stretch k s n = s (n div k)
fun shrink k s n = s (n * k)
fun drop k s n = s (n+k)
fun shift s = drop 1 s
fun take 0 _ = nil
| take n s = s 0 :: take (n-1) (shift s)
fun loopback loop n = loop (loopback loop) n
end
Most of this implementation is entirely straightforward, given the ease with which we
may manipulate higher-order functions in ML. The only tricky function is loopback
,
which must arrange that the output of the function loop
is "looped
back" to its input. This is achieved by a simple recursive definition of a
sequence whose value at n is the value at n of the sequence resulting
from applying the loop to this very sequence.
The sensibility of this definition of loopback
relies on two separate
ideas. First, notice that we may not simplify the definition of loopback
as follows:
fun loopback loop = loop (loopback loop) (* bad definition *)
The reason is that any application of loopback
will immediately loop
forever! In contrast, the original definition is arranged so that application of loopback
immediately returns a function. This may be made more apparent by writing it in the
following form, which is entirely equivalent to the definition given above:
fun loopback loop = fn n => loop (loopback loop) n
This format makes it clear that loopback immediately returns a function when applied to a loop functional.
Second, for an application of loopback
to a loop to make sense, it must be
the case that the loop returns a sequence without "touching" the argument
sequence (i.e., without applying the argument to a natural number).
Otherwise accessing the sequence resulting from an application of loopback would
immediately loop forever. Some examples will help to illustrate the point.
First, let's build a few sequences without using the loopback
function,
just to get familiar with using sequences:
val evens : int seq = fn n => 2*n
val odds : int seq = fn n => 2*n+1
val nats : int seq = merge (evens, odds)
fun fibs n =
(insert (1, insert (1, map (op +) (zip (drop 1 fibs, fibs)))))(n)
We may "inspect" the sequence using take
and drop
,
as follows:
take 10 nats (* [0,1,2,3,4,5,6,7,8,9] *)
take 5 (drop 5 nats) (* [5,6,7,8,9] *)
take 5 fibs (* [1,1,2,3,5] *)
Now let's consider an alternative definition of fibs
that uses the
loopback operation:
fun fibs_loop s = insert (1, insert (1, map (op +) (zip (drop 1 s, s))))
val fibs = loopback fibs_loop;
The definition of fibs_loop
is exactly like the original definition of fibs
,
except that the reference to fibs
itself is replaced by a reference to the
argument s
. Notice that the application of fibs_loop
to an
argument s
does not inspect the argument s
!
One way to understand loopback is that it solves a system of equations for an unknown sequence. In the case of the second definition of fibs, we are solving the following system of equations for f:
f 0 = 1
f 1 = 1
f (n+2) = f (n+1) + f (n)
These equations are derived by inspecting the definitions of insert
, map
,
zip
, and drop
given earlier. It is obvious that the
solution is the Fibonacci sequence; this is precisely the sequence obtained by applying loopback
to fibs_loop
.
Here's an example of a loop that, when looped back, yields an undefined sequence --- any attempt to access it results in an infinite loop:
fun bad_loop s n = s n + 1
val bad = loopback bad_loop
val _ = bad 0 (* infinite loop! *)
In this example we are, in effect, trying to solve the equation s n = s n + 1 for s, which has no solution (except the totally undefined sequence). The problem is that the "next" element of the output is defined in terms of the next element itself, rather than in terms of "previous" elements. Consequently, no solution exists.
With these ideas in mind, we may apply the sequence package to build an implementation of digital circuits. Let's start with wires, which are represented as sequences of levels:
datatype level = High | Low | Undef
type wire = level seq
type pair = (level * level) seq
val Zero : wire = constantly Low
val One : wire = constantly High
(* clock pulse with given duration of each pulse *)
fun clock (freq:int):wire = stretch freq (alternately (Low, High))
We include the "undefined" level to account for propagation delays and settling times in circuit elements.
Combinational logic elements (gates) may be defined as follows. We introduce an explicit unit time propagation delay for each gate --- the output is undefined initially, and is then determined as a function of its inputs. As we build up layers of circuit elements, it takes longer and longer (proportional to the length of the longest path through the circuit) for the output to settle, exactly as in "real life".
infixr **;
fun (f ** g) (x, y) = (f x, g y) (* apply two functions in parallel *)
fun logical_and (Low, _) = Low (* hardware logical and *)
| logical_and (_, Low) = Low
| logical_and (High, High) = High
| logical_and _ = Undef
fun logical_not Undef = Undef
| logical_not High = Low
| logical_not Low = High
fun logical_nop l = l
val logical_nor =
logical_and o (logical_not ** logical_and) (* a nor b = not a and not b *)
type unary_gate = wire -> wire
type binary_gate = pair -> wire
fun gate f w 0 = Undef (* logic gate with unit propagation delay *)
| gate f w i = f (w (i-1))
val delay : unary_gate = gate logical_nop (* unit delay *)
val inverter : unary_gate = gate logical_not
val nor_gate : binary_gate = gate logical_nor
It is a good exercise to build a one-bit adder out of these elements, then to string them together to form an n-bit ripple-carry adder. Be sure to present the inputs to the adder with sufficient pulse widths to ensure that the circuit has time to settle!
Combining these basic logic elements with recursive definitions allows us to define
digital logic elements such as the RS flip-flop. The propagation delay inherent in
our definition of a gate is fundamental to ensuring that the behavior of the flip-flop is
well-defined! This is consistent with "real life" --- flip-flop's depend
on the existence of a hardware propagation delay for their proper functioning. Note
also that presentation of "illegal" inputs (such as setting both the R and the S
leads high results in metastable behavior of the flip-flop, here as in real life
Finally, observe that the flip-flop exhibits a momentary "glitch" in its output
before settling, exactly as in the hardware case. (All of these behaviors may be
observed by using take
and drop
to inspect the values on the
circuit.)
fun RS_ff (S : wire, R : wire) =
let
fun X n = nor_gate (zip (S, Y))(n)
and Y n = nor_gate (zip (X, R))(n)
in
Y
end
(* generate a pulse of b's n wide, following by w *)
fun pulse b 0 w i = w i
| pulse b n w 0 = b
| pulse b n w i = pulse b (n-1) w (i-1)
val S = pulse Low 2 (pulse High 2 Zero);
val R = pulse Low 6 (pulse High 2 Zero);
val Q = RS_ff (S, R);
val _ = take 20 Q;
val X = RS_ff (S, S); (* unstable! *)
val _ = take 20 X;
It is a good exercise to derive a system of equations governing the RS flip-flop from the definition we've given here, using the implementation of the sequence operations given above. Observe that the delays arising from the combinational logic elements ensure that a solution exists by ensuring that the "next" element of the output refers only the "previous" elements, and not the "current" element.
Finally, we consider a variant implementation of an RS flip-flop using the loopback operation:
fun loopback2 (f : wire * wire -> wire * wire) =
unzip (loopback (zip o f o unzip))
fun RS_ff' (S : wire, R : wire) =
let
fun RS_loop (X, Y) =
(nor_gate (zip (S, Y)), nor_gate (zip (X, R)))
in
loopback2 RS_loop
end
Here we must define a "binary loopback" function to implement the flip-flop.
This is achieved by reducing binary loopback to unary loopback by composing with zip
and unzip
.