Skip to content

The Joy of Concatenative Languages Part 3: Kindly Types

22
Dec
2008

In parts one and two of this series, we dipped our toes into the fascinating world that is stack-based languages.  By this point, you should be fairly familiar with how to construct simple algorithms using Cat (the language we have been working with) as well as the core terminology of the paradigm.  In fact, with just the information given so far, you could probably go on to be productive with a real-world concatenative language like Factor.  However, the interest does not just stop there…

One of the interesting challenges in programming language design is the construction of a type system.  So as to clear up any possible misconception before it arises, this is how Pierce defines such a thing:

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

For Java, which has a comparatively weak type system, this usually means preventing you from accidentally using a String as if it were an int.  In other words, Java’s type system generally proves the absence of things like NoSuchMethodError and similar.  C#, which has a slightly more-powerful type system, can also prove the absence of most NullPointerException(s) when code is written in a correct and idiomatic fashion.  Scala goes even further with pattern matching…need I go on?  The point is that type systems do different things in different languages, so the definition needs to be flexible enough to reflect that.

In this article, we’re going to look at how we can define a type system for a functional (meaning that we have quotations) concatenative language.  In a comment on the first part of this series, it was suggested that the task of typing stack-based languages is a fairly trivial one.  This is true, but only to a certain point.  As we will see, there are dragons lurking in the conceptual shadows, waiting for us to disturb their sleep.

Simple Expressions

Let’s start out with typing something simple.  Consider the following program:

 

For those of you reading the RSS, what you see between the previous paragraph and this is exactly what I intended to write: nothing at all.  In a concatenative language, the empty program is usually considered to be valid.  After all, it takes a stack as input and returns the exact same stack.  We could replicate the semantics of this program by writing “dup pop“, but why bother?

The empty program has the following type:

(->)

Or, more properly:

('A -> 'A)

To the left of the -< we have what I like to call the “input constraints”: what types must be on the stack coming into the program (or phrase).  To the right of the arrow are the “output constraints”: what types will be on the stack when we’re done.  For reasons which will become clear later on, 'A in this case represents the whole input stack (regardless of what it contains).  Since we never change anything on the stack (the program is, after all, empty), the output stack has whatever type the input stack was given.  Another way of writing this type would be as follows: 

* -> *

This literally symbolizes our intuition that the empty program has no input or output constraints.  However, this is somewhat less correct notationally since it implies that the input and output stacks are unrelated.  In fact, I would go so far as to say that this notation is wrong.  The only reason it is produced here is to serve as a memory aid.  For the remainder of the article, we will be using Cat’s notation for types.

Let’s look at something a little less trivial.  Consider the following program one word at a time:

1 2 +

Remember that an integer literal (or any literal for that matter) is just a function which pushes a specific constant onto the stack.  Let’s assign types based on what we expect the input/output constraints of these functions to be.  Note: I will be using the colon (:) notation to denote a type.  This isn’t conventional coming from C-land, but it is the gold standard of formal type theory:

1 : ('A -> 'A Int)
2 : ('A -> 'A Int)
+ : ('A Int Int -> 'A Int)

This is all very intuitive.  Integer literals work on any stack and just produce that stack with a new Int pushed onto the top.  Both 1 and 2 have the same type, which is a good sign that we’re on the right track.

The + word is a little more interesting.  Its runtime semantics are as follows: pop two integers off the stack, add them together and then push the result back on.  This word will not be able to execute without both integer values on the top of the stack.  Thus, it only makes sense that its input constraints be some stack with two values of type Int at the top.  Likewise, when we’re done, those two integers will be gone and a new Int will be pushed onto the remainder of the stack which was given to us.  Remember that 'A represents any stack, even if it is completely empty.

Coming back to our program, we can see that it is well typed by simply string together the types we have generated.  Starting from the top (using * to symbolize the empty stack):

Word Input Stack Output Stack
1 * * Int
2 * Int * Int Int
+ * Int Int * Int

Do you see how the input stack of each word matches the output stack of the previous?  In this case, this sort of one-to-one matching indicates that the program is well-typed, producing a final stack with a single Int on it.  If we actually run this program, we would see that the evaluation matches the assigned types.

First-Order Functions

This is fine for a simple addition program, but what if we throw functions into the mix?  Consider the same program we just analyzed wrapped up within a function:

define addSome {
  1 2 +
}
 
addSome

Here we define a function which has as a body the program we have already analyzed.  Down at the bottom of our new program, we actually call this function.  Here is the question: what type does the addSome word have?

To answer this question, look back at the table above and consider the Input Stack for the first word in concert with the Output Stack for the last.  Putting these two types together yields the following type for the aggregated whole:

1 2 + : ('A -> 'A Int)

These words (or “phrase”) takes any stack as input, and then through some manipulation produces a single Int on top of that stack as a result.  The stack may grow and shrink within the function, but at the end of the day, only the Int remains.  As we would expect, this matches the runtime semantics perfectly.

Given the fact that the phrase “1 2 +” has the type ('A -> 'A Int), it is reasonable to assign that same type to the function which contains it.  Thus, we can type-check the addSome program in a simple, one-row table:

Word Input Stack Output Stack
addSome * * Int

At the start of execution, the input stack to any program is *, or the empty stack.  However, this is fine with our type checker, since the program has 'A — or any stack — for its input parameters.

This is all so nice and intuitive, so let’s consider the case where we have a function which actually takes some parameters.  Specifically, let’s consider the following definition:

define addTwice {
  + +
}

At runtime, this function will take three values off the stack and then add them all together.  It is the Cat equivalent of the following in Scala:

def addTwice(a: Int, b: Int, c: Int) = a + b + c

The question is: how do we assign this (the Cat function) a type?  As we have done before, let’s look at the types of the individual words:

+ : ('A Int Int -> 'A Int)
+ : ('A Int Int -> 'A Int)

Not much help there.  Let’s try making a table:

Word Input Stack Output Stack
+ * Int Int * Int
+ * Int Int * Int

It’s tempting to look at this and just assign addTwice the type of ('A Int Int -> 'A Int).  However, this would be a mistake.  Notice the problem with our table above: the Input Stack type of the second word does not match the Output Stack of the first.  In other words, this program does not immediately type-check.

The problem is the second word is accessing more of the stack than the first.  We’re effectively “deferring” a parameter access until later in the function, rather than grabbing everything right away and threading the processing through from start to finish.  This is a perfectly reasonable pattern, but it plays havoc with our naive type system.

The solution is to merge the input constraints across both words.  The first word (+) requires two Int(s) to be on the top of the stack.  When it is done, those Int(s) are gone and a single Int has taken their place.  The second word (again +) also requires two Int(s) on the stack.  We only have one that we know of (the output Int from the first word), so we must unify the constraints and merge things back “up the chain” as it were.  In other words, our first word (+) will require not just two Int(s) on the stack but three: two for itself and one for the second word (+).  Our corrected table will look something like the following:

Word Input Stack Output Stack
+ * Int Int Int * Int Int
+ * Int Int * Int

With this new table, all of the Input and Output stacks match, which means that the type is valid and can prove runtime evaluation.  Thus, based on this whole song and dance, we can assign the following type:

addTwice : ('A Int Int Int -> 'A Int)

As expected, this function takes not two, but three Int(s) on the stack and returns the remainder of that stack with a new Int on top.

Polymorphic Words

One mildly-annoying issue that we have just skated over is the problem of polymorphism.  Consider the following two programs:

42 pop

And this…

"fourty-two" pop

The question is: what type do we assign to pop?  We can easily make the following two assertions:

42           : ('A -> 'A Int)
"fourty-two" : ('A -> 'A String)

If we attempt to use this information to type-check the first program (assuming that it is sound), we will arrive at the following type for pop:

pop : ('A Int -> 'A)

That’s intuitive, right?  All that we’re doing here is taking the first value off of the stack (an Int, in the case of the first program) and throwing it away, returning the remainder of the stack.  However, if we use this type, we will run into some serious troubles type-checking the second program:

Word Input Stack Output Stack
"fourty-two" * * String
pop * Int *

Since pop has type ('A Int -> 'A) (as we asserted above), it is inapplicable to a stack with String on top.  Note that we can’t just push these constraints “up the chain”, since it is a case of direct type mismatch, rather than a stack of insufficient depth.  In short: we’re stuck.

The only way to solve this problem is to introduce the concept of parametric types.  Literally, we need to define a type which can be instantiated against a given stack, regardless of what type happens to match the parameters in question.  Java calls this concept “generics”.  Rather than giving pop the overly-restrictive type of ('A Int -> 'A), we will instead allow the value on top of the stack to be of any type (not just Int):

pop : ('A 'a -> 'A)

Note the fact that 'A and 'a are very separate type variables in this snippet.  'A represents the “rest of the stack”, while 'a represents a specific type which just happens to be on top of the input stack.  Using this new, more flexible type, we can produce tables for both of our earlier programs:

Word Input Stack Output Stack
42 * * Int
pop * Int *

 

Word Input Stack Output Stack
"fourty-two" * * String
pop * String *

Everything matches and the world is once again very happy.  Note that we can also apply this parametric type concept to the slightly more interesting example of dup:

dup : ('A 'a -> 'A 'a 'a)

In other words, dup says that whatever type is on top of the stack when it starts, that type will be on top of the stack twice when it is finished.  Just like pop, this type can be instantiated against any stack with at least one type, regardless of whether that type is Int, String, or anything else for that matter.

Higher-Order Functions

We’ve seen how to type-check simple phrases, as well as first-order functions with deferred stack access and the occasional polymorphic word.  However, there is one particularly troublesome aspect of concatenative type systems which we have completely ignored: functions which take quotations off the stack.  In other words: what type do we assign to apply?  Consider the following function:

define trouble {
  apply
}

At runtime, trouble will pop a quotation and then evaluate it against the remainder of the stack.  Intuitively, we need to have some way of representing the type of a quotation, but that’s not even the most serious problem.  Somehow, we need to constrain the quotation to itself accept exactly the stack which remains after it is popped.  We also need to find some way of capturing its output type in order to compute the final output type of trouble.

More concretely, we can make a first attempt at assigning a type for trouble.  The underscores (_) illustrate an area where our type system is incapable of helping us:

trouble : (_ (_ -> _) -> _)

It’s very tempting to just throw an 'A in there and be done with it, but the truth is that for this type expression, there is no “unused stack”.  We don’t really know how much (or how little) of the stack will be used by the quotation; it could pop five elements, twenty or none at all.  It literally needs access to the remainder of the input stack in its entirety, otherwise the expression is useless.  Enter stack polymorphism…

Just as we needed a way to represent any single type in order to type-check pop and dup, we now need a way to represent any stack type in order to type-check apply.  Fortunately, the answer is already nestled within our pre-established notation.  Consider the type of +:

+ : ('A Int Int -> 'A Int)

We have been taking this to mean “any stack with two Int(s) on top resulting in that same stack with only one Int“.  This is true, but we’re being a little hand-wavy about the meaning of “any stack” and how it relates to 'A.  When we really get down to it, what’s happening here is 'A is being instantiated against a particular input stack, whatever that stack happens to be.  When we were type-checking + +, the first word instantiated 'A not to mean the empty stack (*), but rather a stack with at least one Int on it.  This was required to successfully type the second +.

We can very easily extend this notational convenience to represent generalized stack parameters.  Rather than being instantiated to specific types, stack parameters are instantiated to some stack in its entirety.  Just as with type parameters, wherever we see that instantiated stack parameter within a type expression, it will be replaced with whatever stack type it was assigned.  Thus, we can assign trouble the following type:

trouble : ('A ('A -> 'B) -> 'B)

In other words, trouble takes some stack A which has a quotation on top.  This quotation accepts stack A itself and returns some new stack B.  Note that we don’t really know anything about B.  It could be related to A, but it might not be.  The final result of the whole expression is this new stack B.

This concept is remarkably powerful.  With it in combination with the other types we have already examined, we can type check the entirety of Cat and be assured of the absence of type-mismatch and stack-underflow errors.  Considering the fact that Cat is almost exactly as powerful as Joy, that’s a pretty impressive feat.

From a theoretical standpoint, things get even more interesting when we consider the type of the following function:

define y {
  [dup papply] swap compose dup apply
}

This has the following type:

y : ('A ('A ('A -> 'B) -> 'B) -> 'B)

As you may have guessed by the name, this is the Y-combinator1, one of the most well-known mechanisms for producing recursion in a nameless system.  Note that this definition looks a little different from the pure-untyped lambda calculus (call-by-name semantics):

λf . (λx . f (x x)) (λx . f (x x))

What I’m trying to point out here is the fact that Cat is able to leverage its type system to assign a type to the Y-combinator.  This is something which is literally impossible in System F, a typed form of lambda-calculus.  In fact, the only way to type-check this function in a lambda-calculus-derivative system would be to add recursive types.  Cat is able to get by with a very much non-recursive type definition, something which I find fascinating in the extreme.

Update: The above paragraph is somewhat misleading.  It turns out that Cat actually does use a recursive type under the surface to derive the non-recursive type for y.  Specifically:

dup papply : ('A ('B ('B self -> 'C) -> 'C) -> 'A ('B -> 'C))

On a further theoretical note, the device in Cat’s type system which allows this power is in fact the stack type variable (e.g. 'A).  These stack types are conceptually quite similar to the type parameters we used in typing pop (e.g. 'a), but still in a very separate domain.  In fact, stack types have a different kind than regular types.  This is not to say that Cat employs higher-kinds such as Scala’s (e.g. * => *), but it does have two very different type kinds: stacks and values.

And yet, it is not kinds in and of themselves which allows for the typing of the Y-combinator.  Fω is essentially System F with higher-kinds, and yet it is still incapable of handling this tiny little expression.  Most interesting indeed…

Conclusion

As you can see, type systems and concatenative languages do fit together nicely, but it takes a lot more effort than one would initially expect.  While typing simple expressions is easy enough, the waters are muddied as soon as higher-order functions and even deferred stack access enters the mix.  This is an extremely fertile area for research, where a lot of interesting ideas are being developed.  For example, John Nowak’s 5th attempts to apply a type system to the stack-based paradigm, but in a very different way than Cat.

I hope you enjoyed this mini-series of articles on concatenative languages.  While they are a bit of a backwater in the programming language menagerie, I think that studying them can be a very instructive experience.  Furthermore, there remain some problems that are very nicely expressed in languages like Cat while being extremely unwieldy in more conventional languages like Scala.  Despite the obscurity of concatenative languages, it never hurts to have an extra language on hand, ready for those times when it really is the best tool for the job.

1 Technically, this is a little different from the Y-combinator used in conventional lambda-calculus (it executes the quotation rather than returning a fixed-point).  However, conceptually it is the same idea.

Filed in Cat | Comments (8)

The Joy of Concatenative Languages Part 2: Innately Functional

15
Dec
2008

In part one of this series, I introduced the concept of a stack-based language and in particular the syntax and rough ideas behind Cat.  However, to anyone coming into concatenative land for the first time, my examples likely seemed both odd and unconvincing.  After all, why would you ever use point-free programming when everyone else seems to be sold on the idea of name binding?  More importantly, where do these languages fit in with our established menagerie of language paradigms?

The answer to the first question really depends on the situation.  I personally think that the best motivation for concatenative languages is their syntax.  If you want to create an internal DSL, there will be no language better suited to it than one which is concatenative, Cat, Factor or otherwise.  This is because stack-oriented languages can get away with almost no syntax whatsoever.  They say that Lisp is a syntax-free language, but this holds even more strongly for languages like Cat.  Well, that and you don’t have to deal with all the parentheses…

The second question is (I think) the more interesting one: how do we classify these languages and what sort of methodologies should we apply?  At first glance, Cat (and other languages like it) seem to be quite imperative in nature.  After all, you have a single mutable stack that any function can modify.  However, if you turn your head sideways and blink twice, you begin to realize that concatenative languages are really much closer to the functional side of the oyster.

Consider the following Cat program:

define plus { + }
define minus { - }
 
7 2 3
plus minus

Trivial, but to the point.  This program first adds the numbers 2 and 3, then subtracts the result from 7.  Thus, the final result is a value of 2 on the stack.  The only twist is that we have defined functions plus and minus to do the dirty work for us.  This wasn’t strictly necessary, but I wanted to emphasize that + and - really are functions.  We could express the exact same program in Scala:

def plus(a: Int, b: Int) = a + b
def minus(a: Int, b: Int) = a - b
 
minus(7, plus(2, 3))

Do you see how the consecutive invocations of plus and minus in Cat became composed invocations in Scala?  This is where the term “concatenative language” derives from: the whole program is just a series of function compositions.  Wikipedia’s article on Cat has a very nice, mathematical description:

Two adjacent terms in Cat imply the composition of functions that generate stacks, so the Cat program f g is equivalent to the mathematical expressions and , where x is the stack input to the expression.

Strictly speaking, a concatenative language could be implemented without a stack, but such an implementation would likely be a bit harder to use than the average stack-based language.

Coming back to my original premise: concatenative languages are functional in nature.  Absolutely everything in Cat is a function.  Operators, words, even numeric literals like “3” are actually functions at the conceptual level.  Additionally, Cat, Joy and Factor all offer a mechanism for treating functions as first-class values:

2 3
[ + ]
apply

The square-bracket ([]) syntax is representative of a quotation.  Literally this mean “create a function of the enclosed words and place it as a value on the stack”.  We can pop this function off the stack and invoke it by using the apply word.  Incidentally, you may have noticed that this syntax is remarkably close to that which is used in if conditionals:

5 0 <
[ "strange math" ]
[ "all is well" ]
if

This syntax works because if isn’t conceptually a language primitive: it’s just another function which happens to take a boolean and two quotations off the stack.  For the sake of efficiency, Cat does indeed implement if as a primitive, but this was a deliberate optimization rather than an implementation forced by the language design.  Untyped Cat (see Part 3) is equivalent in power to the pure-untyped lambda calculus, and as our friend Alonzo Church showed us, if-style conditionals are easily accomplished:

TRUE = λa . λb . a
FALSE = λa . λb . b

IF = λp . λt . λe . p t e

Yeah, maybe we’re drifting a bit off-point here…

Higher-Order Programming

So if Cat is just another functional programming language, then we should be able to implement all of those higher-order design patterns that we’ve come to know and love in languages like Scala and ML.  To see how, let’s look at implementing some simple list manipulation functions in Cat.  The easiest would be to start with append, which pops two lists off of the stack and pushes a new list which is the end-to-end concatenation of the two originals:

define append {
  empty
  [ pop ]
  [
    uncons
    [append] dip
    cons
  ]
  if
}

This function first starts by checking to see if the top list is empty.  If so, then just pop it off the stack and leave the other right where it is.  Appending an empty list should always yield the original list.  However, if the head list is not empty, then we need to work a bit.  First, we decompose it into its tail and head, which are pushed onto the stack in order by the uncons function.  Next, we need to recursively append the tail with our second list on the stack.  However, the head of the list from uncons is in the way on top of the stack.  We could use stack manipulation to move things around and get our lists up to the head of the stack, but dip provides us with a handy, higher-order shortcut.  We temporarily remove the top of the stack, invoke the quotation “[append]” against the remainder and then push the old top back on top of the result.

The dip operation is surprisingly powerful, making it possible to completely live without either variables or multiple stacks.  Any non-trivial Cat program will need to make use of this handy function at some level.

Once we have the old head and the new appended-list on the stack, all we need to do is put them back together using cons.  This function leaves a new list on the stack in place of the old list and head element.  This Cat program is almost precisely analogous to the following ML:

fun append ls nil = ls
  | append ls (hd :: tail) = hd :: (append ls tail)

Personally, I find the ML a lot easier to read, but that’s just me.  Obviously it’s a lot shorter, but as it turns out, our Cat implementation, while intuitive, was sub-optimal.  Cat already implements append in the guise of the cat function, and it is far more concise than what I showed:

define cat {
  swap [cons] rfold
}

It’s almost frightening how short this is: only three words.  It’s not as if rfold is doing anything mysterious either; it’s just a simple right-fold function that takes a list, an initial value and a quotation, producing a result by traversing the entire list.  We can use something similar back in ML-land, achieving an implementation which is arguably equivalent in subjective elegance:

val append = foldr (op::)

Moving on, we can also implement a length function in Cat, this time using fold to tighten things up:

define length {
  0 [ pop 1 + ] fold
}

You’ll notice that we have to mess around a bit in the quotation in order to avoid the first “parameter”, the current element of the list (which we do not need).  Expressing this in ML yields a very similar degree of cruft:

val length = foldl (fn (n, _) => n + 1) 0

Conclusion

The important take-away from this tangled morass of an article is the fact that Cat is a highly functional language, capable of easily keeping up with some of the stalwart champions of the paradigm.  More significantly, this is a trait which is shared by all concatenative languages.  Rather than throwing away all of the old wisdom learned in language design, stack-based languages build on it by providing an alternative view into the world of functions.

In the next (and final) article of the series, we will take a brief look at the challenges of applying a type system to a concatenative language and the fascinating techniques used by Cat to achieve just that.

Filed in Cat | Comments (14)

The Joy of Concatenative Languages Part 1

8
Dec
2008

Concatenative languages like Forth have been around for a long time.  Hewlett-Packard famously employed a stack-based language called “RPL” on their HP-28 and HP-48 calculators, bringing the concept of Reverse Polish Notation to the mainstream…or as close to the mainstream as a really geeky toy can get.  Surprisingly though, these languages have not seen serious adoption beyond the experimental and embedded device realms.  And by “adoption”, I mean real programmers writing real code, not this whole interpreted bytecode nonsense.

This is a shame, because stack-based languages have a remarkable number of things to teach us.  Their superficial distinction from conventional programming languages very quickly gives way to a deep connection, particularly with functional languages.  However, if we dig even deeper, we find that this similarity has its limits.  There are some truly profound nuggets of truth waiting to be uncovered within these murky depths.  Shall we?

Trivial aside: I’m going to use the terms “concatenative” and “stack-based” interchangeably through the article.  While these are most definitely related concepts, they are not exactly synonyms.  Bear that in mind if you read anything more in-depth on the subject.

The Basics

Before we look at some of those “deeper truths of which I speak, it might be helpful to at least understand the fundamentals of stack-based programming.  From Wikipedia:

The concatenative or stack-based programming languages are ones in which the concatenation of two pieces of code expresses the composition of the functions they express. These languages use a stack to store the arguments and return values of operations.

Er, right.  I didn’t find that very helpful either.  Let’s try again…

Stack-based programming languages all share a common element: an operand stack.  Consider the following program:

2

Yes, this is a real program.  You can copy this code and run/compile it unmodified using most stack-based languages.  However, for reasons which will become clear later in this series, I will be using Cat for most of my examples.  Joy and Factor would both work well for the first two parts, but for part three we’re going to need some rather unique features.

Returning to our example: all this will do is take the numeric value of 2 and push it onto the operand stack.  Since there are no further words, the program will exit.  If we want, we can try something a little more interesting:

2 3 +

This program first pushes 2 onto the stack, then 3, and finally it pops the top two values off of the stack, adds them together and pushes the result.  Thus, when this program exits, the stack will only contain 5.

We can mix and match these operations until we’re blue in the face, but it’s still not a terribly interesting language.  What we really need is some sort of flow control.  To do that, we need to understand quotations.  Consider the following Scala program:

val plus = { (x: Int, y: Int) => x + y }
plus(2, 3)

Notice how rather than directly adding 2 and 3, we first create a closure/lambda which encapsulates the operation.  We then invoke this closure, passing 2 and 3 as arguments.  We can emulate these exact semantics in Cat:

2 3
[ + ]
apply

The first line pushes 2 and 3 onto the stack.  The second line uses square brackets to define a quotation, which is Cat’s version of a lambda.  Note that it isn’t really a closure since there are no variables to enclose.  Joy and Factor also share this construct.  Within the quotation we have a single word: +.  The important thing is the quotation itself is what is put on the stack; the + word is not immediately executed.  This is exactly how we declared plus in Scala.

The final line invokes the apply word.  When this executes, it pops one value off the stack (which must be a quotation).  It then executes this quotation, giving it access to the current stack.  Since the quotation on the head of the stack consists of a single word, +, executing it will result in the next two elements being popped off (2 and 3) and the result (5) being pushed on.  Exactly the same result as the earlier example and the exact same semantics as the Scala example, but a lot more concise.

Cat also provides a number of primitive operations which perform their dirty work directly on the stack.  These operations are what make it possible to reasonably perform tasks without variables.  The most important operations are as follows:

  • swap — exchanges the top two elements on the stack.  Thus, 2 3 swap results in a stack of “3 2” in that order.
  • pop — drops the first element of the stack.
  • dup — duplicates the first element and pushes the result onto the stack.  Thus, 2 dup results in a stack of “2 2“.
  • dip — pops a quotation off the stack, temporarily removes the next item, executes the quotation against the remaining stack and then pushes the old head back on.  Thus, 2 3 1 [ + ] dip results in a stack of “5 1“.

There are other primitives, but these are the big four.  It is possible to emulate any control structure (such as if/then) just using the language shown so far.  However, to do so would be pretty ugly and not very useful.  Cat does provide some other operations to make life a little more interesting.  Most significantly: functions and conditionals.  A function is defined in the following way:

define plus { + }

Those coming from a programming background involving variables (that would be just about all of us) would probably look at this function and feel as if something is missing.  The odd part of this is there is no need to declare parameters, all operands are on the stack anyway, so there’s no need to pass anything around explicitly.  This is part of why concatenative languages are so extraordinarily concise.

Conditionals also look quite weird at first glance, but under the surface they are profoundly elegant:

2 3 plus    // invoke the `plus` function
10 <
[ 0 ]
[ 42 ]
if

Naturally enough, this code pushes 0 onto the stack.  The conditional for an if is just a boolean value pushed onto the stack.  On top of that value, if will expect to find two quotations, one for the “then” branch and the other for the “else” branch.  Since 5 is less than 10, the boolean value will be True.  The if function (and it could just as easily be a function) pops the quotations off of the stack as well as the boolean.  Since the value is True, it discards the second quotation and executes the first, producing 0 on the stack.

I’ll leave you with the more complicated example of the factorial function:

define fac {
  dup 0 eq
  [ pop 1 ]
  [ dup 1 - fac * ]
  if
}

Note that this isn’t even the most concise way of writing this, but it does the job.  To see how, let’s look at how this will execute word-by-word (assuming an input of 4):

Stack Word
4

dup
4 4

0
4 4 0

eq
4 False

[ pop 1 ]
4 False [pop 1]

[ dup 1 - fac * ]
4 False [pop 1] [dup 1 - fac *]

if
4

dup
4 4

1
4 4 1

-
4 3

fac (assume magic recursion)
4 6

*

The final result is 24, a value which is left on the stack.  Pretty nifty, eh?

Conclusion

You’ll notice this is a shorter post than I usually spew forth (no pun intended…this time).  The reason being that I want this to be fairly easy to digest.  Concatenative languages (and Cat in particular) are not all that difficult to digest.  They are a slightly different way of thinking about programming, but as we will see in the next part, not so different as it would seem.

Note: Cat is written in C# and is available under the MIT License.  Don’t fear the CLR though, Cat runs just fine under Mono.  If you really want to experiment with no risk to yourself, a Javascript interpreter is available.

Filed in Cat | Comments (13)

Introduction to Automated Proof Verification with SASyLF

1
Dec
2008

Doesn’t that title just get the blood pumping?  Proof verification has a reputation for being an inordinately academic subject.  In fact, even within scholarly (otherwise known as “unrealistically intelligent“) circles, the automated verification of proofs is known mainly as a complex, ugly and difficult task often not worth the effort.  This is a shame really, because rigorous proofs are at the very core of both mathematics and computer science.  We are nothing without logic (paraphrased contrapositive from Descartes).  Believe it or not, understanding basic proof techniques will be of tremendous aid to your cognitive process, even when working on slightly less ethereal problems such as how to get the freakin’ login page to work properly.

Well, if you made it all the way to the second paragraph, then you either believe me when I say that this is legitimately useful (and cool!) stuff, or you’re just plain bored.  Either way, read on as we commence our exciting journey into the land of rigorous proofs!

SASyLF Crash Course

If you’re at all familiar with the somewhat-specialized field of proof verification, you probably know that SASyLF (pronounced “sassy elf”) is not the most widely used tool for the job.  In fact, it may very well be the least well-known.  More commonly, proofs that require automatic verification are written in Twelf or Coq.  Both of these are fine tools and capable of a lot more than SASyLF, but they can also be extremely difficult to use.  One of the primary motivations behind SASyLF was to produce a tool which was easier to learn, had a higher level syntax (easier to read) and which gave more helpful error messages than Twelf.  The main idea behind these convolutions was to produce a tool which was more suitable for use in the classroom.

The main design decision which sets SASyLF apart from Twelf is the way in which proofs are expressed.  As I understand it, Twelf exploits Curry-Howard correspondence to represent proofs implicitly in the types of a functional program (update: this is incorrect; see below).  While this can be very powerful, it’s not the most intuitive way to think about a proof.  Eschewing this approach, SASyLF expresses proofs using unification (very similar to Prolog) and defines inference rules explicitly in a natural-language style.

There are three main components to a SASyLF proof:

  • Syntax
  • Judgments
  • Theorems/Lemmas

Intuitively enough, the syntax section is where we express the grammar for the language used throughout our proof.  This grammar is expressed very naturally using BNF, just as if we were defining the language mathematically for a hand-written proof.  Left-recursion is allowed, as is right-recursion, arbitrary symbols, ambiguity and so on.  SASyLF’s parser is mind bogglingly powerful, capable of chewing threw just about any syntax you throw at it.  The main restriction is that you cannot use parentheses, square brackets ([]), pipes (|) or periods (.) in your syntax.  The pure-untyped lambda calculus defined in SASyLF would look something like this:

t ::= fn x => t[x]
    | t t
    | x

I said we couldn’t use brackets, but that’s only because SASyLF assigns some special magic to these operators.  In a nutshell, they allow the above definition of lambda calculus to ignore all of the issues associated with variable name freshness and context.  For simplicity’s sake, that’s about as far as I’m going to go into these mysterious little thingies.

The judgments section is where we define our inference rules.  Just as if we were defining these rules by hand, the syntax has the conditionals above a line of hyphens with the conclusion below.  The label for the rule goes to the right of the “line”.  What could be more natural?

judgment eval: t -> t

t1 -> t1'
--------------- E-Beta1
t1 t2 -> t1' t2

The judgment syntax is what defines the syntax for the -> “operator”.  Once SASyLF sees this, it knows that we may define rules of the form t -> t, where t is defined by the syntax section.  Further on down, SASyLF sees our E-Beta1 rule.  Each of the tokens within this rule (aside from ->) begins with “t“.  From this, SASyLF is able to infer that we mean “a term as defined previously”.  Thus, this rule is syntactically valid according to our evaluation judgment and the syntax given above.

Of course, theorems are where you will find the real meat of any proof (I’m using the word “proof” very loosely to mean the collection of proven theorems and lemmas which indicates some fact(s) about a language).  SASyLF wouldn’t be a very complete proof verification system without support for some form of proving.  Once again, the syntax is extremely natural language, almost to the point of being overly-verbose.  A simple theorem given the rules above plus a little would be to show that values cannot evaluate:

theorem eval-value-implies-contradiction:
    forall e: t -> t'
    forall v: t value
    exists contradiction .

    _: contradiction by unproved
end theorem

Note that contradiction is not more SASyLF magic.  We can actually define what it means to have a contradiction by adding the following lines to our judgment section:

judgment absurd: contradiction

In other words, we can have a contradiction, but there are no rules which allow us to get it.  In fact, the only way to have a contradiction is to somehow get SASyLF to the point where it sees that there are no cases which satisfy some set of proven facts (given the forall assumptions).  If SASyLF cannot find any cases to satisfy some rules, it allows us to derive anything at all, including judgments which have no corresponding rules.

Readers who have yet to fall asleep will notice that I cleverly elided a portion of the “theorem” code snippet.  That’s because there wasn’t really a way to prove that contradiction given the drastically abbreviated rules given in earlier samples.  Instead of proving anything, I used a special SASyLF justification, unproved, which allows the derivation of any fact given no input (very useful for testing incomplete proofs).  Lambda calculus isn’t much more complicated than what I showed, but it does require more than just an application context rule in its evaluation semantics.  In order to get a taste for SASyLF’s proof syntax, we’re going to need to look at a much simpler language.

Case Study: Integer Comparison

For this case study, we’re going to be working with simple counting numbers which start with 0 and then proceed upwards, each value expressed as the successor of its previous value.  Thus, the logical number 3 would be s s s 0.  Not a very useful language in the real world, but much easier to deal with in the field of proof verification.  The syntax for our natural numbers looks like this:

n ::= 0
    | s n

With this humble definition for n, we can go on to define the mathematical greater-than comparison using two rules under a single judgment:

judgment gt: n > n

------- gt-one
s n > n

n1 > n2
--------- gt-more
s n1 > n2

Believe it or not, this is all we need to do in terms of definition.  The first rule says that the successor of any number is greater than that same number (3 > 2).  The second rule states that if we already have two numbers, one greater than the other (12 > 4), then the successor of the greater number will still be greater than the lesser (13 > 4).  All very intuitive, but the real question is whether or not we can prove anything with these definitions.

An Easy Lemma

For openers, we can try something reasonably simple: prove that all non-zero numbers are greater than zero.  This is such a simple proof that we won’t even bother calling it a theorem, we will give it the lesser rank of “lemma”:

lemma all-gt-zero:
    forall n
    exists s n > 0 .

    _: s n > 0 by induction on n:
        case 0 is
            _: s 0 > 0 by rule gt-one
        end case

        case s n1 is
            g: s n1 > 0 by induction hypothesis on n1
            _: s s n1 > 0 by rule gt-more on g
        end case
    end induction
end lemma

In order to prove anything about n, we first need to “pull it apart” and find out what it’s made of.  To do that, we’re going to use induction.  We could also use case analysis, but that would only work if our proof didn’t require “recursion” (we’ll get to this in a minute).  There are two cases as given by the syntax for n: when n is “0“, and when n is “s n1“, where n1 is some other number.  We must prove that s n > 0 for both of these cases individually, otherwise our proof is not valid.

The first case is easy.  When n is 0, the proof is trivial using the rule gt-one.  Notice that within this case we are no longer proving s n > 0, but rather s 0 > 0.  This is the huge win brought by SASyLF’s unification: n is “0” within this case.  Anything we already know about n, we also know about 0.  When we apply the rule gt-one, SASyLF sees that we are attempting to prove s n > n where n is “0“.  This is valid by the rule, so the verification passes.

The second case is where things get interesting.  We have that n is actually s n1, but that doesn’t really get us too much closer to proving s s n1 > 0 (remember, unification).  Fortunately, we can prove that s n1 > 0 because we’re writing a lemma at this very moment which prove that.  This is like writing a function to sum all the values in a list: when the list is empty, the result is trivial; but when the list has contents, we must take the head and then add it to the sum of the tail as computed by…ourself.  Induction is literally just recursion in logic.  Interestingly enough, SASyLF is smart enough to look at all of the inductive cases in your proof and verify that they are valid.  This is sort-of the equivalent of a compiler looking at your code and telling you whether or not it will lead to an infinite loop.

To get that s n1 > 0, we use the induction hypothesis, passing n1 as the “parameter”.  However, we’re not quite done yet.  We need to prove that s s n1 > 0 in order to unify with our original target (s n > 0).  Fortunately, we already have a rule that allows us to prove the successor of a number retains its greater-than status: gt-more.

However, gt-more has a condition in our definition.  It requires that we already have some fact n1 > n2 in order to obtain s n1 > n2.  In our case, we already have this fact (s n1 > 0), but we need to “pass” it to the rule.  SASyLF allows us to do this by giving our facts labels.  In this case, we have labeled the s n1 > 0 fact as “g“.  We take this fact, pack it up and send it to gt-more and it gives us back our final goal.

A Slightly Harder Theorem

A slightly more difficult task would be to prove that the successors of two numbers preserves their greater-than relationship.  Thus, if we know that 4 > 3, we can prove that 5 > 4.  More formally:

theorem gt-implies-gt-succ:
    forall g: n1 > n2
    exists s n1 > s n2 .

    _: s n1 > s n2 by unproved
end theorem

At first glance, this looks impossible since we don’t really have a rule dealing with s n on the right-hand side of the >-sign.  We can try to prove this one step at a time to see whether or not this intuition is correct.

Almost any lemma of interest is going to require induction, so immediately we jump to inducting on the only fact we have available: g.  Note that this is different from what we had in the earlier example.  Instead of getting the different syntactic cases, we’re looking at the the rules which would have allowed the input to be constructed.  After all, whoever “called” our theorem will have needed to somehow prove that n1 > n2, it would be helpful to know what facts they used to do that.  SASyLF allows this using the case rule syntax.  We start with the easy base case:

_: s n1 > s n2 by induction on g:
    case rule
        ------------ gt-one
        _: s n2 > n2
    is
        _: s s n2 > s n2 by rule gt-one
    end case
end induction

In this case, the term _: s n2 > n2 is unified with n1 > n2.  Thus, n1 is actually “s n2“.  This means that by unification, we are actually trying to prove s s n2 > s n2.  Fortunately, we have a rule for that.  If we let “n” be “s n2“, we can easily apply the rule gt-one to produce the desired result.

The second case is a bit trickier.  We start out by defining the case rule according to the inference rules given in the judgment section.  The only case left is gt-more, so we mindlessly copy/paste and correct the variables to suit our needs:

case rule
    g1: n11 > n2
    ------------- gt-more
    _: s n11 > n2
is
    _: s s n11 > s n2 by unproved
end case

In this case, n1 actually unifies with “s n11“.  This is probably the most annoying aspect of SASyLF: all of the syntax is determined by token prefix, so every number has to start with n, occasionally making proofs a little difficult to follow.

At this point, we need to derive s s n11 > s n2.  Since the left and right side of the > “operator” do not share a common sub-term, the only rule which could possibly help us is gt-more.  In order to apply this rule, we will somehow need to derive s n11 > s n2 (remember, gt-more takes a known greater-than relationship and then tells us something about how the left-successor relates to the right).  We can reflect this “bottom-up” step towards a proof in the following way:

case rule
    g1: n11 > n2
    ------------- gt-more
    _: s n11 > n2
is
    g: s n11 > s n2 by unproved
    _: s s n11 > s n2 by rule gt-more on g
end case

At this point, SASyLF will warn us about the unproved, but it will happily pass the rest of our theorem.  This technique for proof development is extremely handy in more complicated theorems.  The ability to find out whether or not your logic is sound even before it is complete can be very reassuring (in this way you can avoid chasing entirely down the wrong logical path).

In order to make this whole thing work, we need to somehow prove s n11 > s n2.  Fortunately, we just so happen to be working on a theorem which could prove this if we could supply n11 > n2.  This fact is conveniently available with the label of “g1“.  We feed this into the induction hypothesis to achieve our goal.  The final theorem looks like this:

theorem gt-implies-gt-succ:
    forall g: n1 > n2
    exists s n1 > s n2 .

    _: s n1 > s n2 by induction on g:
        case rule
            ------------ gt-one
            _: s n2 > n2
        is
            _: s s n2 > s n2 by rule gt-one
        end case

        case rule
            g1: n11 > n2
            ------------- gt-more
            _: s n11 > n2
        is
            g2: s n11 > s n2 by induction hypothesis on g1
            _: s s n11 > s n2 by rule gt-more on g2
        end case
    end induction
end theorem

Conclusion

I realize this was a bit of a deviation from my normal semi-practical posts, but I think it was still a journey well worth taking.  If you’re working as a serious developer in this industry, I strongly suggest that you find yourself a good formal language and/or type theory textbook (might I recommend?) and follow it through the best that you can.  The understanding of how languages are formally constructed and the mental circuits to create those proofs yourself will have a surprisingly powerful impact on your day-to-day programming.  Knowing how the properties of a language are proven provides tremendous illumination into why that language is the way it is and somtimes how it can be made better.

Credit: Examples in this post drawn rather unimaginatively from Dr. John Boyland’s excellent course in type theory.

Filed in Scala | Comments (10)

Infinite Lists for the Finitely Patient

17
Nov
2008

Functional programming has a lot of weird and abstract concepts.  Monads of course are the poster child for all that is strange and confusing in functional languages, but there are other examples.  At first glance, it seems that the concept of an infinite list would be just as bizarre and incomprehensible as anything else in the paradigm, but really things aren’t as bad as all that.  In fact, even the die-hard imperative programmer can likely benefit from the patterns and techniques enabled by this obtuse construct.

For the first part of the article, I’m going to use a lot of examples involving numbers.  This is just because I’m lazy and only want to introduce one concept at a time.  Everyone understands the idea that there are an infinite amount of integers starting from 0 and counting upward.  Please bear with me all the way to the end, I promise I will give some more convincing motivation for infinite lists along the way.

If you’re already familiar with the semantics of infinite lists, feel free to skip to the section answering that all-important question: Why Do We Care?

Syntax

Before we dive into the topic of infinite lists and how they are practically applicable, it’s important to understand the underlying mechanics and (critically) how the API works in practice.  I’ll be using Scala to illustrate.  Any language which supports lambdas would actually suffice, but Scala’s unique blend of the functional and the object-oriented can be very useful in illustrating infinite lists in an imperative context.  Also, for the duration of the article, I will be making use of the following implicit conversion:

class RichStream[A](str: =>Stream[A]) {
  def ::(hd: A) = Stream.cons(hd, str)
}
 
implicit def streamToRichStream[A](str: =>Stream[A]) = new RichStream(str)

The only thing you need to know about the above is that it dramatically simplifies the syntax required when working with infinite lists in Scala.  Since the focus of this article is infinite lists and not implicit conversions, we will just take the above as magic incantations and leave it at that.

The primary medium for working with infinite lists in Scala is the scala.Stream class.  This class is not magic, you could write it yourself in plain-old-Scala without too much trouble.  Stream inherits from the all-encompassing scala.Iterable trait, meaning that familiar methods like map, foldLeft and foreach are all available for use with an infinite list as well as a finite one.

In terms of mechanics, infinite lists are very similar to finite ones: composed of a head—which is some data of type A—and a tail—which is another Stream[A].  The critical distinction which allows infinite lists to be infinite is the fact that this tail is lazily evaluated.  That means that the tail as a value is not available until you ask for it.  This is a profound idea with far reaching consequences, particularly in languages which take it to its greatest extreme (Haskell).

Just like with a normal, finite List, we build instances of Stream using a cons cell.  This is basically the in-code representation of head/tail concept.  Normally, this “cons for Streams” is handled by the singleton method Stream.cons (the equivalent of Clojure’s lazy-cons).  However, thanks to our magic implicit conversion noted above, we can make use of the same right-associative :: operator that we use with regular every-day finite Lists.  For example, we can easy create an infinite list of the natural numbers (from 0 to ∞):

def from(n: Int): Stream[Int] = n :: from(n + 1)
 
val nats = from(0)

In this example, from is what is known as a generator function.  That is to say, it takes an input and transforms it directly into some output structure.  Well, actually that’s only part of the definition, but the rest of it gets a little weird…

One very important property of from which should immediately jump out at you is the fact that it is infinitely recursive.  It takes a number, invokes this mysterious :: operator on that value and then recursively calls back to itself.  There is no conditional guard, no base case, just an endless series of calls.  Intuitively, this should lead to non-termination at runtime…except that it doesn’t.  Remember what I said about the lazily-evaluated tail?  This is where that idea really begins to take effect.  The from function is not infinitely recursive; at least, not right away.

Because the tail of a Stream is lazy, there is no need to actually invoke from(n + 1) until that particular element of the list (or one which comes after it) is required.  To prove this intuition, we can add a side-effect to the from function so that we can trace the execution:

def from(n: Int): Stream[Int] = {
  println("Requesting n = " + n)
  n :: from(n + 1)
}
 
val nats = from(0)

This code will print exactly (and only) the following:

  Requesting n = 0

The invocation from(1) is never processed because it does not need to be.  We can force further evaluation of the list by requesting a later element:

nats(4)      // get the fifth natural number (4)

This will print the following:

  Requesting n = 1
  Requesting n = 2
  Requesting n = 3
  Requesting n = 4

Notice that we don’t evaluate for n = 0 a second time.  Infinite lists are lazy, but not inefficient.  Each element is evaluated exactly once, and only as necessary.  You can exploit this property to do some really amazing things (such as the most concise Fibonacci sequence you will ever see).

As mentioned previously, all of the standard utility methods available on collections are also usable with infinite lists.  For example, it might be moderately interesting to get a list of all multiples of 5.  We could create a new generator function (e.g. fromBy5) which only returned multiples of five, but there is a much easier technique we could apply.  We already have a list of all natural numbers, why not make use of that?  If we multiplied every natural number by 5, the result would be identical to the infinite list of the multiples of 5.  If you haven’t taken calculus, this statement probably sounds a little weird.  After all, wouldn’t the list of all natural numbers multiplied by 5 be bigger than just the list of the multiples of five?

Actually, the answer to this question is “no”, and we could prove that mathematically if it weren’t entirely besides the point.  The really interesting thing to focus on is the technique suggested: take the infinite list of natural numbers (which we already have) and multiply each element by 5, resulting in another infinite list.  If you’re at all familiar with the higher-order processing of finite collections, you should be thinking map:

val fives = nats map { _ * 5 }

For those of you not “in the know”, the ever-cryptic { _ * 5 } syntax actually means the following: { x => x * 5 }.  The advantage of the former over the latter is merely brevity.

The definition of the map method goes something like this:

For every element within the target collection, apply the specified function value and store the result in the corresponding location of a new collection.

“For every element…”  That phrase should be raising huge red flags.  It implies that map is trying to iterate over the entire nats collection—a collection of infinite size.  Once again, we seem to have created a non-terminating expression.

Fortunately, the laziness of infinite lists comes to our rescue.  Just like :: doesn’t evaluate the tail until it is absolutely required to do so, map doesn’t actually invoke the function it is passed until an element is retrieved from the mapped list.  Once again making use of our println-enabled from method, we can test when the elements are being retrieved:

val nats = from(0)
val fives = nats map { _ * 5 }
 
println("Querying list...")
fives(4)                      // get the fifth multiple of five (20)

When this code executes, it will print the following:

  Requesting n = 0
  Querying list...
  Requesting n = 1
  Requesting n = 2
  Requesting n = 3
  Requesting n = 4

Surprised?  It helps to remember this simple fact: everything about an infinite list is lazy.  Nothing is evaluated until it absolutely must.

So, that means we can do something like the following, right?

for (n <- fives) {
  println(n)
}

If we were to execute this snippet, the result would be as follows:

  Requesting n = 0
  0
  Requesting n = 1
  5
  Requesting n = 2
  10
  Requesting n = 3
  15
  Requesting n = 4
  20
  Requesting n = 5
  25
  Requesting n = 6
  30
  .
  .
  .

In other words, this evaluation really is non-terminating.  This is because there is no way for the laziness of the list to help us.  We’re trying to iterate over every element in the list, retrieving that element for evaluation right away.  In this sort of situation, evaluation cannot be deferred, and thus the program will never end.

As it turns out, there are a number of operations on infinite lists which cannot be done lazily.  The foreach method is one of these, as are foldLeft, foldRight, reduce(Left and Right), length, etc.  As a general rule of thumb, virtually any operation on an infinite list which produces another infinite list can be performed lazily.  Otherwise, if a result is of an immediate type (such as Int or even Array), the evaluation absolutely must be performed at that exact point in the code.  More formally: any operation on an infinite list which is catamorphic (meaning that it takes the whole collection and reduces it to a single value) will force the evaluation of the collection in its entirety.

So if it’s impossible to iterate, fold or get the length of an infinite list, of what use could they possibly be?  It is true that infinite lists in and of themselves would be too “high-minded” for any practical application, but that’s what the take method is designed to fix.  The Stream#take(Int) method is a way of imposing a narrow window on an infinite list.  Rather than looking at every single natural number from 0 to infinity, we just look at the numbers from 0 to 9.  Put into code:

val nats = from(0)
val digits = nats.take(10)
 
for (d <- digits) {
  println(d)
}

This will print (exactly):

  0
  1
  2
  3
  4
  5
  6
  7
  8
  9

The beauty of this is that we have created an infinite list, taken exactly what we needed and ignored the rest.  Most of the time, this is how you will use the streams which you create.  Note that the take method still does not force evaluation of the list.  If we go back to our fancy printlnified version of from, we can see that evaluation is still being performed lazily, just limited to an upper bound of 9 (because we took the first 10 elements, starting from 0):

  Requesting n = 0
  0
  Requesting n = 1
  1
  Requesting n = 2
  2
  Requesting n = 3
  3
  Requesting n = 4
  4
  Requesting n = 5
  5
  Requesting n = 6
  6
  Requesting n = 7
  7
  Requesting n = 8
  8
  Requesting n = 9
  9

Why Do We Care?

Thus far, we have looked at a few examples of infinite lists, all of them having to do with numbers.  This list is surprisingly useful (as we will see in a moment), but it is far from the only infinite list we can create.  This section will explore some slightly more down-to-earth applications for infinite lists, including use-cases which everyone (even the dirty-scumbag imperative lovers) can relate to.  :-)

Conceptually, infinite lists are a way of flattening recursion and packaging it up in a form which can be manipulated in a less clumsy fashion.  Got that?  Good.  Now, read it again.

Let’s consider the simple (and extremely common) case in C/C++ where we must iterate over all of the elements of an array.  I’m using C++ here because Java has the enhanced for-loop which completely blows my example out of the proverbial water:

char *names[6] = { "Daniel", "Chris", "Joseph", "Renee", "Bethany", "Grace" };
int len = 6;
 
for (int i = 0; i < len; ++i)
{
    cout << names[i] << endl;
}

We’ve all written code like this.  In fact, most of us have probably written it so often that the prefix “for (int i = 0; ” has become part of our permanent muscle memory.  However, look at what we have done here.  Strictly speaking, we’re not looping over the the array of names at all.  We are actually looping over every successive integer between 0 and 6.

Replicating these semantics in a functional programming language is actually a bit tricky (assuming that we rule out higher-order solutions like foreach).  Ignoring for the moment the issues associated with side-effects and I/O, we have a somewhat more serious issue to worry about: functional languages don’t have any loops.  Of course, Scala does (while and do/while), but for the sake of argument we will ignore this fact.

The idiom for “looping” in functional languages is to use recursion.  Instead of maintaining a mutable counter (i) which changes value at each iteration, we will define a loop method which takes a parameter i, processes the ithe element of an array and then recursively calls itself, passing i + 1.  In code, this looks like the following:

val names = Array("Daniel", "Chris", "Joseph", "Renee", "Bethany", "Grace")
 
def loop(i: Int) {
  if (i < names.length) {
    println(names(i))
    loop(i + 1)
  }
}
loop(0)

Just in case you were confused as to why some people dislike functional languages, the above is “it”.  Scala will compile the above into a form which is actually just as efficient as the earlier C++ example, but that’s not really the point.  The problem is that this code is horribly ugly.  The underlying meaning (looping over the array) is completely obscured behind a fog of syntax and method dispatch.  You can easily imagine how a more complex looping example (particularly with nested loops) might get unmaintainably messy.

This is where infinite lists swoop in and save the day.  Remember when I said that infinite lists serve to bottle up recursion in a form that we can swallow?  (if you don’t remember, scroll back up and read it again)  We can make use of the fact that we have already defined an infinite list of all integers starting at 0.  All we have to do is just take exactly the number we need (names.length) and then use a for-comprehension to iterate over the result:

for (i <- nats.take(names.length)) {
  println(names(i))
}

If you actually unroll the evaluation semantics of the above, you will find that we’re still using recursion, it’s just being handled behind the scenes in the from method.  This is what I meant when I said that infinite lists “flatten recursion”.

Note that the above idiom is so common-place that Scala actually defines a specialization of infinite lists just to represent ranges of integers.  Oddly enough, this class is called “Range“.  We can create a range by using the until method on a starting integer, passing it an end-point:

for (i <- 0 until names.length) {
  println(names(i))
}

This way, we don’t have to define a new infinite list of nats every time we need to iterate over a range of numbers.

Of course, iteration over an integer range is a fairly trite example.  Everyone reading this article should know that there are better ways of accomplishing what we just did.  For example, the higher-order method foreach is capable of printing the names array in a far more concise fashion:

names foreach println

Let’s try something a little more complex.  Imagine that we have to loop through 10 random integers between -100 and 100.  Just to make this really fun, let’s say that we have to perform this as an inner and an outer loop, printing out all combinations of the same 10 random numbers.

If it weren’t for the restriction that the 10 random numbers need be the same between both loops, an imperative programmer might just do something like the following:

int a = 0;
for (int i1 = 0; i1 < 10; i1++) {
    a = // generate random number
 
    int b = 0;
    for (int i2 = 0; i2 < 10; i2++) {
        b = // generate random number
        System.out.println("(" + a + ", " + b + ")");
    }
}

This code is really nasty.  Not only that, but it doesn’t do what we want since the random numbers generated for the inner loop will be different from the ones generated for the outer.  We could technically fiddle with shared seeds and the like, but even that isn’t a really elegant solution.

Using infinite lists, the solution is surprisingly simple.  All we need to do is define an infinite list of random numbers between -100 and 100, then take the first 10 values from this list and perform standard nested iteration using a for-comprehension.  It’s much easier to write in Scala than it is to say:

def randomGen: Stream[Int] = (Math.random * 200).toInt - 100 :: randomGen
val random = randomGen
 
for (a <- random.take(10); b <- random.take(10)) {
  println("(" + a + ", " + b + ")")
}

When this executes, it will print the following sequence:

  (68, 68)
  (68, -83)
  (68, -79)
  (68, -78)
  (68, -18)
  (68, -80)
  (68, 29)
  (68, 10)
  (68, -63)
  (68, 3)
  (-83, 68)
  (-83, -83)
  (-83, -79)
  (-83, -78)
  .
  .
  .

Pretty nifty, eh?  You’ll notice that this time our generator function didn’t need to take a parameter.  This dramatically simplified the syntax involved in generating the infinite list.  However, despite the fact that we no longer require a parameter for our generator, we still need to assign the list to a value.  Consider these two (incorrect!) definitions for random:

def random: Stream[Int] = (Math.random * 200).toInt - 100 :: random
// or even...
val random: Stream[Int] = (Math.random * 200).toInt - 100 :: random

The first definition for random (as a function) will indeed work, producing an infinite list of random numbers.  However, that list will not be repeatable.  In other words, consecutive invocations of random (such as in our nested loop example) will produce different lists.  Swinging to the other end of the scale, the value definition for random will actually produce an infinite list of exactly the same number (e.g. 42, 42, 42, 42, 42, 42, ...).  The reason for this is left as an exercise for the reader.

Let’s consider one last example.  This time, we’ll look at something a little less “functional” in nature.  Imagine that you have defined a database schema which looks like the following:


people
id INTEGER
firstName VARCHAR
lastName VARCHAR
parentID INTEGER

This is a fairly simple parent/child schema with each row having a reference to its parent.  It’s not difficult to imagine a scenario where one might want to traverse the “ancestry” of a row in the table, perhaps looking for some specific criterion or just for enumerative purposes.  This could be done in Java (and other languages) by maintaining a mutable “person” variable containing the current row in the database.  This variable could be modified iteratively based on successive queries determining its corresponding parentID.  However, as you can imagine, the code would be messy and prone to subtle errors.

The better approach in this situation is actually to make use of an infinite list.  While it is true that the list could not possibly be infinite given a finite database, the concept of a lazily-constructed collection can still simplify the issue.  We would construct the list using the following generator method:

def ancestors(id: Int) = {
  val conn: Connection = ...
 
  try {
    val res = conn.executeQuery("SELECT parentID FROM people WHERE id = ?")
 
    if (res.next()) {
      val parentID = res.getInt(1)
      parentID :: ancestors(parentID)
    } else Stream.empty
  } finally {
    conn.close()
  }
}

One item of note regarding this function is the use of the Stream.empty constant.  This is precisely analogous to the Nil object used in constructing conventional lists: it simply marks the end of the linked list.  Because every person will have a finite ancestry, we aren’t actually exploiting the infinite potential (no pun intended) of streams.  In fact, we are only using the data structure as a tool to facilitate lazy evaluation.

The nice thing about representing the database traversal in the given fashion is the ability to treat the results as a fully-realized collection even before the queries have actually been run.  For example, we can generate a list of all people in the parentage of person 42, and then restrict this list to only people with an odd id.  I have no idea why this would be useful, but here it is:

val parents = ancestors(42)
val fewerParents = parents filter { _ % 2 == 1 }
 
for (id <- fewerParents) {
  println(nameForPerson(id))       // get a person's name and print
}

All of the logic associated with traversing the database tree is nicely tucked away within the ancestors function.  This separation of logic allows for much cleaner code at times, hence reducing the potential for silly mistakes.

Conclusion

Infinite lists can be a surprisingly powerful tool, even in the arsenal of someone who is still devoted to the Dark Side of imperative programming.  Our last example looked at a scenario where an infinite list could be useful, despite the obviously side-effecting nature of the problem.  Similarly, the example of a list of random numbers shows how infinite lists can even be used to solve problems which are extremely difficult to solve using classical, imperative techniques.

To summarize: infinite lists are not just a beautiful mathematical formalism stemming from the forbidding forests of Haskell, they can also be a useful device when approaching down-to-earth problems like complex iteration.  The next time you find yourself writing unpleasant code to loop over complex data sets, stop and consider whether or not a stream might be a better solution.

Filed in Scala | Comments (14)