The Fix Is Infix

There's nothing like implementing something from scratch to make you appreciate it. In this case, I've been working on a toy logic programming language, ostensibly to investigate opportunities for parallelism in the implementation, but I haven't actually gotten around to the parallelism part—both because the talk I was supposed to give on the topic has been postponed, and because I've gotten distracted by the sheer fun of logic programming itself.

Until I started this project, I never gave much thought to the syntax of Prolog. The format of a Prolog predicate looks very much like an expression in many programming languages, that is, it looks either like a constant identifier, as in this simple rule:

    toast_is_delicious.

or like a C-style function, with a function name followed by parenthesized arguments, as in:

    grandmother(A,B) :- grandparent(A,B), female(A).

which is a rule consisting of three predicates: the head of the rule is grandmother(A,B), and the body of the rule consists of the conjunction of the two predicates grandparent(A,B) and female(A). (You can read the rule as “A is a grandmother of B if A is a grandparent of B and A is female”.)

One common problem with the C-style function syntax is that it is not always obvious which parameter is which. In the case of a two-argument predicate named with a noun, like grandmother above, the usual understanding is that the first argument will be the grandmother, and the second the grandchild; that is, the pattern:

    noun(arg1,arg2)

is to be read:

    arg1 is the noun of arg2.

Here it helps that there is a pretty obvious English translation of the Prolog predicate, and the order in which arg1 and arg2 appear in that translation is the same as in the Prolog. (You could also read the predicate as “arg1 is arg2's noun”, but that doesn't affect the order in which the arguments appear.)

However, not all relationships we want to talk about are as simple as the grandmother-grandchild relationship. Consider:

    gives(A,B,C).

Does this mean that A gives B C, or A gives B to C? In the former case, B is the recipient; in the latter, the gift. English is not helpful as a guide here, because both sentences are idiomatic English. And in general, the more arguments a predicate has, the more ways there will be translate it into natural language.

Of course, the problem of which argument is which is not limited to Prolog; most of us with some programming experience will have had to look up the parameter order to at least some of the functions we've used in other programming languages. Static typing can help with this problem, but only if different parameters have incompatible types.

Anyway, I started out basing my toy language on the Logic Programming section of Abelson and Sussman's venerable Structure and Interpretation of Computer Programs. Because SICP uses Scheme, its logic programming clauses look like Lisp rather than C:

    (rule (toast-is-delicious))
    
    (rule (grandmother ?a ?b)
          (and (grandparent ?a ?b)
               (female ?a)))

Traditional Prolog makes a distinction between predicates and lists, where lists are a built-in data structure; in the syntax, lists are surrounded by square brackets instead of parentheses. Unlike Prolog, the SICP formulation of logic programming does not make a distinction between predicates and lists; the same unification algorithm works for both. The result is a language that feels altogether freer; for example, you can create a database like:

    (rule (alice chases rabbits))
    (rule (alice has a restaurant where you can get anything you want))
    (rule (alice sends a message to bob encrypted with bobs public key))

and ask all about Alice with the query:

    (alice . ?what)

In my own toy language, I adopt a SICP-like conflation of predicates and lists. Also, I add a parser that accepts a slightly more traditional Prolog-like syntax that omits the outer parentheses on each predicate. So you might say:

    grandmother A B: grandparent A B, female A.

But why on earth would you put it that way? If you have any familiarity with English, doesn't that strike you as awfully stilted? How about:

    A is grandmother of B: A is grandparent of B, A is female.

Granted, this is still not natural language, but for me, at least, it's easier to read. And you no longer have to say this:

    gives A B C.

because you can say this:

    A gives B to C.

English, like many other languages, uses words in infix position to describe relationships between other words in a sentence; and in a context where you can arrange words in a way that exploits that natural ordering, you might as well do so.

Writing database rules in such a free, naturalistic style is not without peril. Natural languages are full of words that can be used in different ways. You might not expect a query like:

    X flies like|Y.

(where the vertical bar is the infix cons operator) to yield both:

    X = time
    Y = (an arrow)

and:

    X = fruit
    Y = (a banana)

(although then again, you might). So although at first the syntax I've presented here may make it look as if you can say anything you want, if you actually try it out, you'll realize that you have to adopt conventions as rigorous (and perhaps almost as unnatural) as in any ordinary Prolog program.

Does the sort of free-form infix notation I've presented here have any value in other sorts of programming languages than logic programming languages? One big sticking point I can see is that most programming languages offer no typographic distinction between constant and variable names—so would make a sound be a command to trigger your computer speakers, or to ensure the soundness of some assertion bound to the variable a? Although some programming languages do use sigils to distinguish different sorts of identifiers, the whole idea of nonconstant variables borders on oxymoronic in modern functional programming languages (Scala's use of an uppercase/lowercase in pattern matching notwithstanding). In a unification-based language like Prolog, however, the constant/variable distinction is not just natural, but essential. So I suspect there's nothing here that transfers easily to other contexts.

If you think the syntax I've presented is either too far from real logic programming or some sort of advance in the state of the art, I should point out that there's a perfectly straightforward transformation to genuine, unadulterated Prolog. For example, you can turn:

    (H|_) contains H.
    (_|T) contains X: T contains X.

into:

    cons(cons(H,_),cons(contains,cons(H,nil))).
    cons(cons(_,T),cons(contains,cons(X,nil))) :-
      cons(T,cons(contains,cons(X,nil))).

But are you sure you want to?

Five for '15

2014 was a pretty good year for me in terms of learning new things. My meetup group held a bunch of meetings at which we explored type-theoretic topics and worked our way through some computer-assisted theorem proving.

But next week is another year, and I'm trying to figure out what I should be trying to figure out next. I've come up with five things I'd like to learn about in 2015:

1. How concurrent can logic programming get, and what techniques are used to parallelize operations in a language like Prolog? This is a separate question from how to create Prolog predicates that perform conventional sorts of thread management operations, which is mostly what you find if you search for “concurrent Prolog”. It's also separate from the question of how concurrent logic programming should get—the consensus seems to be that Japan's fifth generation computer project yielded the answer “not very” (people found it hard to write programs in a way that took full advantage of concurrent logical operations). But I'm still curious to figure out just how you'd adapt a logic programming implementation (like the one described in Structure and Interpretation of Computer Programs) if you pretended that you could run arbitrarily many processes at once with no communication costs between them.

2. On a related note, how might you compile a dependently typed programming language to Prolog? There seems to be a straightforward translation of dependent algebraic data types to Prolog clauses, but I haven't sat down to figure out how you'd integrate that with an interpreter for the dependently typed lambda calculus. As a subquestion, is it possible to generate the Prolog such that it does not use any sequential operations like cuts, so as to take advantage of my infinitely parallel Prolog implementation from the previous question?

3. What type systems have been developed for process calculi? Are any as expressive as the dependently typed lambda calculus? What sort of mathematics do such type systems lead to? (These are some topics we may explore in the meetup group this year.)

   I realize that a fair amount has been written on this topic; I just haven't read it yet. But straight off, it seems as if a type system for something like the pi calculus couldn't look much like one for the lambda calculus. A function type in the lambda calculus assumes that control returns to the caller of the function; the function type describes the relationship between the inputs and outputs to the function. In the pi calculus, control could go off in any (or no) direction—the closest analog to a function type would be a channel type that describes what types of values get sent to the channels that are inputs to the channel in question (I think). This sounds a lot wilder than the tidy walled garden of the lambda calculus.

4. Is there an elegant way to create a sort of dependently typed Lisp? By which I don't mean that I just want more parentheses so that I can stuff complex type declarations into them—I'm not that fond of traditional Lisp syntax, and I'm even a fan of infix operators. What I'm looking for is a way to create a language with a sophisticated type system (like the dependently typed lambda calculus) that is homoiconic—that is, not only is there is a straightforward correspondence between a source program and the resulting syntax tree, but syntax trees themselves are easy to understand and manipulate (at least that's what I mean by “homoiconic”; there seems to be plenty of controversy out there about how the term should be understood). More specifically, I'd like a language where equivalents of the standard Lisp operations quote and eval are easy to define and use.

5. Looking in a slightly different direction, how can one develop neural networks that implement functions of arbitrary (dependent) type? I've read a little about how recurrent neural networks can handle variable-sized data as input to an artificial neural network, but how does that work for output?

If 2014 for me was the Year of the Lambda Calculus, it looks as if 2015 will be the Year of the Pi Calculus, given how frequently I've mentioned concurrency above.

I hesitate to formulate my interest in these topics as any sort of New Year's resolution, because we all know what happens to New Year's resolutions. But I have agreed to give a short presentation on opportunities for concurrency in Prolog implementations on the 4th of January. I've found that promising a talk on a topic one knows nothing about is an excellent motivator for learning about said topic.

Poker with Tarot Cards

So recently I was learning to play Poker along with an inquisitive 10-year-old named Eli, and the question came up: how would you play Poker with Tarot cards?

(The comedian Steven Wright is known for saying, “Last night I stayed up late playing Poker with Tarot cards. I got a full house and four people died.”—but in fact, the Tarot deck has been used for playing games since it appeared in Europe in the 15th century, presumably with few fatalities. According to the Wikipedia article on Tarot cards, the earliest record we have for the practice we now consider the primary purpose of the Tarot—telling fortunes, where each card has a particular significance—dates from the 18th century. So if historical precedence is any guarantee, you are most likely not courting spiritual disaster by sneaking in a few hands of Tarot Klondike.)

Of course, making the rules is always more fun than playing by the rules, so I'm hardly the first person to suggest alternate ways of playing Poker. Variations include:

• Play with multiple 52-card decks;
• Scored hands of 6 cards instead of 5 (in this case, using 2 standard decks);
• Use of a fifth 13-card suit, with an additional scored hand, namely a “super” (one of each of the 5 suits);
• And of course, playing Poker with Tarot cards—dividing the trumps into 3 new suits, or with a modified Tarot deck that extends the 4 minor suits to have 22 cards, like the trumps.

The knobs that can be twiddled in designing a new Poker variant (ignoring the betting, which is a whole nother can of worms) include:

• The deck:
  • The number of suits
  • The number of ranks
  • Whether all suits have the same ranks (is the deck a rectangular grid?)
• The number of cards that count as a hand (could be more or less than the usual 5)
• The types of card combinations that are scored:
  • Straights (card ranks are sequential)
  • Flushes (all cards are of the same suit)
  • n of a kind (that is, groups of n cards of the same rank)
  • Or something else, like the super mentioned above. You could also eliminate or modify one of the standard combinations—maybe flushes don't count for anything, or you allow a “small straight” (all but one of the cards' ranks are sequential)

Let the twiddling begin!

The deck of interest here is the 78-card Tarot deck of 5 suits, where the trumps have 22 cards and the other suits (the standard 4 from the 52-card deck) 14 cards each. The trumps are numbered 0 through 21; the other suits 1 through 10 and then Jack, Knight, Queen, King (or Valet, Cavalier, Dame, Roi in the French Tarot deck I have).

A 5-card hand seems a bit small for a deck that is half again as large as the standard one, so I'd prefer 6. Eli agrees, which settles it.

How to score the hands is a bit of a puzzle. What is a straight? Do we just do a sequential mapping of the trump ranks to the ranks in other suits, and decree that a Jack is an 11, a Knight a 12, a Queen a 13, and a King a 14? Somehow that doesn't seem very satisfactory. I gnawed on this problem for a while and finally decided that straights are based on the nominal ranks of the cards, and the permissible straights are defined by how those ranks are ordered in each suit. That is, the ranks in a straight must be a subsequence of either:

    0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 0

or:

    1 2 3 4 5 6 7 8 9 10 J N Q K 1

(where the lowest card in each suit may also be the highest, for purposes of a straight, as is conventional).

For example, a 6-card straight 3-4-5-6-7-8 may consist of a mix of trump and nontrump suits, but a straight that begins with 8-9-10 must continue with either the 11-12-13 of trumps or the J-N-Q of some other suit(s), so as to preserve a sequence of ranks that actually appears in some suit.

Increasing the number of suits means that flushes become rarer, and increasing the number of cards in the hand means that straights become rarer. These both seem like aesthetic flaws, but I've decided to allow small straights (that is, sequences of 5 cards within a 6-card hand; big straights of 6 cards are also allowed), while ignoring the flush problem (you still need all 6 cards to be of the same suit for a flush. Mixing small straights and small flushes just makes the names of the hands too long).

Here's the ranking of hands (with frequency), based on the above choices:

	big straight flush	0.000023%
	small straight flush	0.000235%
	5 of a kind	0.000284%
	4 of a kind + pair	0.002403%
	3 of a kind + 3 of a kind	0.002412%
	flush	0.033468%
	big straight	0.049992%
	4 of a kind	0.052961%
	pair + pair + pair	0.097513%
	small straight pair	0.106750%
	3 of a kind + pair	0.353574%
	small straight	0.504444%
	3 of a kind	2.466884%
	pair + pair	6.093654%
	pair	40.184611%
	high card	50.050791%

A “small straight flush” consists of 6 cards of the same suit, but only 5 of them are in sequence. A “small straight pair” has 5 cards in sequence, and the rank of one member of the sequence is repeated in the sixth card (as in 4-5-6-7-8-5).

If the whole big straight/small straight thing gives you the willies, an alternative ranking that uses only 6-card straights is:

	straight flush	0.000023%
	5 of a kind	0.000284%
	4 of a kind + pair	0.002403%
	3 of a kind + 3 of a kind	0.002412%
	flush	0.033703%
	straight	0.049992%
	4 of a kind	0.052961%
	pair + pair + pair	0.097513%
	3 of a kind + pair	0.353574%
	3 of a kind	2.466884%
	pair + pair	6.093654%
	pair	40.291361%
	high card	50.555235%

And in case anyone is curious what happens in a standard 52-card deck with 5-card hands where you allow small (4-card) straights, the rankings are:

	big straight flush	0.001539%
	small straight flush	0.012159%
	4 of a kind	0.024010%
	3 of a kind + pair	0.144058%
	flush	0.184381%
	big straight	0.392465%
	small straight pair	0.650106%
	3 of a kind	2.112845%
	small straight	3.100471%
	pair + pair	4.753902%
	pair	41.606797%
	high card	47.017268%

For reference, the standard scoring in the standard deck is:

	straight flush	0.001539%
	4 of a kind	0.024010%
	3 of a kind + pair (full house)	0.144058%
	flush	0.196540%
	straight	0.392465%
	3 of a kind	2.112845%
	pair + pair	4.753902%
	pair	42.256903%
	high card	50.117739%

If you're interested only in standard scoring of 5-card hands in alternate decks, Travis Hydzik has a calculator that quickly figures out hand values for any deck with at least 4 suits and at least 5 ranks, where every suit has the same ranks. If you play with this tool a little bit, you'll see that 13 ranks is something of a sweet spot for decks with a moderate number of suits (between 5 and 9)—with fewer ranks, pairs become even more common than hands with nothing in particular (that is, hands ordered by high card), which strikes me as perverse.

So, I've answered the Tarot Poker question to my own satisfaction. If you want to play Poker with Tarot cards and make different rules, by all means go ahead. Discovering the analogies that work for you between the standard deck and a different deck is more than half the fun.

I thought I would be done by now, but I'm not. Traipsing around the Web in search of alternate card decks led me to something wonderful that you can actually buy: a Fanucci deck. If you are sufficiently Old School, you might recognize this as belonging to the Zork subgame Double Fanucci. What's wonderful about the Fanucci deck? Well, it's got 15 suits named Books, Bugs, Ears, Faces, Fromps, Hives, Inkblots, Lamps, Mazes, Plungers, Rain, Scythes, Time, Tops, and Zurfs—11 cards each, numbered 0 through 9, then ∞—along with 9 unranked trumps called Beauty, Death, Granola, Grue, Jester, Light, Lobster, Snail, and Time (that's right, there's a Time trump that is not part of the Time suit).

Thank you, Internet!

If you don't immediately want to play with something like that, then I just don't know what's wrong with you. Unfortunately, this is just a blog, so I can't actually play a game with the Fanucci cards with you here, but I can tell you what happens when you try to apply the standard Poker scoring rules to the Fanucci deck (5-card hands—I'm treating only the cards ranked 0 through 9 as able to participate in straights; the trumps have no numeric rank and so cannot participate in straights or n of a kind):

	straight flush	0.000007%
	flush	0.000555%
	5 of a kind	0.002634%
	4 of a kind	0.190342%
	straight	0.363255%
	3 of a kind + pair	0.418992%
	3 of a kind	4.593350%
	pair + pair	6.961714%
	high card	41.277900%
	pair	46.191251%

Hmm, high card is more common than a pair. A bit disappointing, but not unexpected, given how many more suits there are than ranks.

One way to try to fix Fanucci Poker is by not letting pairs count for anything, which gets you:

	straight flush	0.000007%
	flush	0.000555%
	5 of a kind	0.002634%
	4 of a kind	0.190342%
	straight	0.363255%
	3 of a kind	5.012342%
	high card	94.430865%

but this means that 94% of hands are scored by high card, which is way off the 50% for standard Poker. That can't be right.

More in the spirit of things is probably to reverse the role of ranks and suits: ranks count only when all 5 of your cards are the same (a flush-like 5 of a kind), whereas any 2 or more of the same suit count (an n-of-a-kind-like flush). So, for example, a straight 3-flush is a straight where 3 of the cards have the same suit:

	straight 5-flush	0.000007%
	straight 4-flush	0.000502%
	5-flush	0.000555%
	straight 3-flush + 2-flush	0.001005%
	5 of a kind	0.002634%
	straight 3-flush	0.013059%
	straight 2-flush + 2-flush	0.019589%
	4-flush	0.065484%
	straight 2-flush	0.156714%
	3-flush + 2-flush	0.163567%
	straight	0.172385%
	3-flush	2.518297%
	2-flush + 2-flush	4.194274%
	2-flush	39.967163%
	high card	52.724764%

This treatment makes 53% of hands scored by high card, which is satisfyingly close to conventional.

I've calculated the odds above with the help of a Scala program I wrote. Because I didn't trust myself to do the combinatorial math for quirky decks where the suits don't all have the same length, the program actually enumerates all possible hands (ignoring order) and checks each of them—this takes many hours on my laptop for 6-card Tarot hands or 5-card Fanucci hands. You're welcome to try the program out for yourself, but if you want to play 7-card Fanucci, you might want to take a different approach.

Anyway, I hope all this encourages you to get some unfamiliar cards and try something new. All decks on hand!

Code Dependent More

The more I learn about the dependently typed lambda calculus, the cooler it seems. You can use it to describe refinement types (aka subset types), which are about as expressive as a type system can get; you can prove theorems (see chapter 8 of the Idris tutorial); you can even, if the Homotopy Type Theory people have their way, use it to build an entirely new foundation for mathematics.

However, I think dependent types need a bit of a marketing makeover. They have a reputation for being abstruse, to say the least. I mean, have you even read the dependent types chapters in Benjamin Pierce's Types and Programming Languages, long the bible of the aspiring type theorist? No, of course you haven't, because those chapters weren't written (although dependent types do merit a whole section in Chapter 30). The dependently typed calculus is apparently so arcane that even the place you go to find out everything about types won't say much about them.

(Not that Pierce is in any way a slacker; his more recent Software Foundations is all about the use of dependent types in the automated proof assistant Coq.)

Although following all the mathematics to which dependent types lead takes a good deal of sophistication (a lot more than I've got), and the implementation choices facing a programming language designer who wants to use dependent types are considerable (let's sweep those under a Very Large Rug), a description of what the dependently typed lambda calculus is is not particularly difficult to grasp for anyone who has used a statically typed programming language.

But then, of course, there's the word “dependent”, which pop psychology has not endowed with the most favorable of connotations. (I'd rather be addicted to coding than addicted to codeine, but still.) Surely more programmers would satisfy their curiosity about more expressive type systems if the dependently typed lambda calculus were just called something else (and while we're at it, preferably something shorter).

So What Is It?

If you haven't seen the dependently typed lambda calculus before, then you might want to start at the beginning, with the untyped lambda calculus (which, if you've used any kind of conventional programming language, you already sort of know, even if you don't know you know it). In the concise notation favored by programming language geeks, the grammar for the untyped calculus looks like:

	e  :=		v		a variable
			λv.e		a function with parameter v and body e
			e1 e2		the function e1 applied to the argument e2
			built-in value		whatever you want: true, 42, etc.

This may look too succinct to make anything out of, but it just means that the untyped lambda calculus is a language that contains variables, functions, function calls, and built-in values. Actually, you can leave out the built-in values (I put them in blue so you can distinguish the pricey add-ons from the base model)—you'll still have a Turing-complete language—but the built-in values (along with parentheses, which you can use to group things) make it feel more like a Lisp dialect, maybe one where curried functions are the norm.

If you're a fan of static types you'd probably prefer a variant of the lambda calculus that has those, and the simplest way to do that is named (surprise!) the simply typed lambda calculus. It has a more complicated grammar than the untyped calculus, because it divides expressions into two categories: terms, which evaluate to a value at runtime, and for which I'll use the letter e; and types, which constrain terms in the usual statically typed way, and which get the letter t:

	e  :=		v		a variable
			λv: t.e		a function with parameter v of type t and body e
			e1 e2		the function e1 applied to the argument e2
			built-in value		whatever you want: true, 42, etc.
	t  :=		t1 → t2		a function type, where t1 is the input type and t2 is the output
			built-in type		whatever you want: Bool, Int, etc.

You'll notice (because it's bright red) that I added a type annotation (: t) as the only change to the term syntax from the untyped lambda calculus. Types can be either function types or built-in types.

This isn't a very sophisticated type system, and you'd hate trying to write any real code in it. Without more add-ons, we can't get correct types out of it for things like product types (think tuples) or sum types (disjoint unions).

Historically, and in most textbooks, the simply typed lambda calculus is augmented with a bunch of special-purpose gadgetry (like those missing product and sum types), and then followed by several progressively more powerful type systems, like the parametric polymorphism that is at the core of languages like Haskell and Scala.

Boooooring!

Instead, let's just skip to the good bits. The dependently typed lambda calculus is not only more powerful than everything we're skipping over; it's also got a shorter grammar:

	e  :=		v		a variable
			λv: e1.e2		a function with parameter v of type e1 and body e2
			e1 e2		the function e1 applied to the argument e2
			e1 → e2		a nondependent function type, where e1 is the input type and e2 is the output
			(v: e1) → e2		a dependent function type, where v, the input, has type e1, and e2 is the output type (which can mention v)
			*		the type of types
			built-in values and types		whatever you want: true, 42, Bool, Int, etc.

But whoa, what happened to the types? Unlike the simply typed calculus, there's no t in this grammar! Well, the big thing about the dependently typed lambda calculus (aside from the dependent function types) is that types are themselves values (the OO folks would say they are reified), and type expressions may involve arbitrary computation. In short, types are just terms!

Everyone's Favorite Example

So what can you actually do with the dependently typed lambda calculus? Well, the traditional (practically mandatory) example is one of a list (let's follow convention and call it a Vec) that has its length encoded in its type.

(This is not really the most exciting thing you can do with dependent types. It's actually possible to encode natural numbers in the type system of Scala or Haskell, so you can already implement Vec in either of those languages. But the two languages' type systems are oriented towards doing typical type-level stuff, so numbers-as-types are pretty awkward—it turns out that regular numbers are still the most convenient way of representing numbers.)

You can specify the type of Vec in the dependently typed lambda calculus as:

    Vec: * → Nat → *

where Nat is the type of natural numbers. That is, a Vec is parameterized by the type of its elements (remember that * is the type of types) and the number of its elements—Vec is actually a function that, given those arguments, returns a type.

The constructor for the empty Vec, Nil, has type:

    Nil: (A: *) → Vec A 0

That is, given a type A, Nil gives you back a Vec of that type with zero elements. You'll remember that we said Vec itself is a function that takes two arguments and returns a type—so the type of Nil is indeed a type, even though it looks like a (plain old, value-level) function call. (If this is the first time you're seeing this, I hope that's as much of a rush for you as it was for me.)

It's clearly not fair for me to leave with you with just Vecs of zero elements, so here's the type of Cons, which constructs a nonempty Vec:

    Cons: (A: *) → (n: Nat) → A → (Vec A n) → (Vec A (n + 1))

That is, you feed Cons the element type A and the size n of the old list you are prepending to, along with an A and the old list, and you get back a new list with size n + 1.

Back to the Whinging

All this technical exposition is fine (although I've left out a whole lot of stuff, like how you actually execute programs written in these calculi), but I really came here to complain, not to explain.

When talking about the polysyllabically-named dependently typed lambda calculus, I have to keep using the terms “depedent function type” and “nondependent function type” (hardly anyone says “independent”), which further pushes up the syllable count. By the time I name what I'm talking about, I've forgotten what I was going to say.

I like to think of nondependent function types (say, A → B) as cake types, because the arrow (like frosting) separates two layers (A and B) with distinct, relatively homogeneous structure, like cake layers. By extension, dependent function types (say, (x: A → b x)) are pie types: the variable x gets mixed from the left side of the arrow into the right, making the whole type chunky with xs, kind of like the bits of apple in an apple pie. So how about calling the whole calculus the pie calculus?

(Now, it may have occurred to you that you don't really need to have two different function types. Wouldn't a cake type be a degenerate version of a pie type, one that didn't happen to mention its variable on the right side of the arrow? Well, yes, you're right—the cake is a lie, albeit a little white lie. But the upshot is that the pie calculus is even simpler than I've made it out to be, because you can drop the production for the cake type from the grammar.)

As it happens, there are a couple of alternate notations for dependent function types. Instead of:

    (x: A) → B

you can say:

    ∀x: A. B

or:

    Πx: A. B

Hey, that last convention makes it look as if the pie calculus is actually the Π calculus! But no, that would make life too easy. It turns out that the pi calculus is already something else, namely a formalism for describing concurrent computations. It's related to the lambda calculus, so no end of confusion would ensue if you tried to hijack the name.

So I guess I'll have to keep calling my favorite calculus by its mind-numbingly long name. Life is unfair, etc., etc.

And So Can You!

You can mitigate some of life's unfairness by mastering the dependently typed lambda calculus yourself. Check out Coq (the aforementioned Coq-based Software Foundations is probably the easiest way to get into dependent types), or Idris, or Agda, or even F* (or, for a quite different take on what it means to implement the calculus, Sage), and start amazing your friends with your new superpowers!

A Completely Objective Observation

When you talk to Scala programmers and use the word “object”, they hear “composable parameterized namespace that is a first-class value”.

When use the word “object” in front of Haskell programmers, they hear “Voldemort”.

Backward Is Forward

The ML section of Dan Grossman's Coursera course is now behind us, and Racket is coming up fast. But I'm still musing about ML and syntax.

One thing Professor Grossman mentioned in passing was the |> operator, which he says is predefined in F# and can easily be defined in ML as:

fun x |> f = f x

That is, it reverses the order of function application: the argument comes first, then the function. This lets you write what feel like Unix-style pipelines:

strs |> (filter (length _ < 3)) |> (map toUpper)

This seems somehow easier to read than:

map toUpper (filter (length _ < 3) strs)

But why is it easier to read? I suppose it's because deep in our hearts we think of functions as little machines, and we like the picture of feeding an input to the first machine, which then feeds its output to the next machine, and so on in a little assembly line.

One reason why object-oriented programming Refuses to Die, even after repeated declarations of Total Victory by the Functional Programming Army, may be that it naturally chains operations in this backwards order. Compare:

strs |> (filter (length _ < 3)) |> (map toUpper)

with:

strs.filter(_.length < 3).map(_.toUpper)

There is, of course, more going on in the OO version than a reordering of the functional version; the objects in question are actually dispatching the methods after the periods. But visually, the OO version doesn't do much more than substitute . for |>, and it retains the readability advantages over the forwards-facing FP version (assuming you agree that using |> does, indeed, enhance readability).

If you read my previous post on concise syntax, you might not have cared for the fact that I wrote a pattern-matching expression as:

(pat1, expr1 | pat2, expr2 | ... | patn, expr2) foo

that is, putting the value to match at the end. But with the pipeline operator, you can say:

foo |> (pat1, expr1 | pat2, expr2 | ... | patn, expr2)

which looks a lot more traditional (maybe only if your traditions are of very recent origin).

But all this brings up the question: Why does function application normally put the function first, anyway? Why isn't the default the other way around?

Aha, you say, Forth! Or at least something like it; Arcane Sentiment has an amusing post speculating on how languages might have evolved in postfix world. And also one on the pipeline operator itself.

Here I have to insert a confession: I sometimes have difficulty keeping track of the ordering in the usual function composition operator. I like to read f ∘ g as “f after g” instead of the officially sanctioned “f composed with g”, because putting the f before the g somehow suggests that the f happens first.

Forth, of course, lays out the functions in the order they are applied. g f means f ∘ g. In fact, rather than thinking of a program in such a language as being a series of operations on a stack, you can think of it as a composition of functions—curiously, it comes out looking just the same.

You might think that all the backwards-facing languages are untyped or dynamically typed, but if you just imagine looking at all your forwards-facing statically typed code in the mirror, you realize that that doesn't have to be the case (backwards everything parse just). And so you might be interested in Jon Purdy's statically typed concatenative language Kitten, something like the love child of Forth and Haskell. He explains how the type-checking works in this post.

In Forth (or Kitten), the function application operator is still just whitespace, as in ML or Haskell. I wonder, would either language let you define a <| that applies a function in the usual order? I don't recall enough Forth, or understand enough Kitten, to be sure.

And where does infix fit into all this? If forwards (or "head-on-the-left") languages can accommodate infix operators, surely the stack-based head-on-the-right ones can too. You can also imagine a language where the forwards and backwards function application operators are equally concise (<| and |>? \ and /? ◁ and ▷?), where you'd have no inherent direction at all, tossed around at the whim of whatever operator you've landed on most recently. Perhaps it would be fun to execute programs in such a language twice, once from each end, swapping the precedences of the forwards and backwards operators.

For all that forwards and backwards function application seem both to be useful (perhaps even equally so), I've never seen anyone suggest that function definition should, in general, be reversible—that is, that you should be able to declare your parameter after the function body:

x + y <= y fn <= x fn

At first glance, this appears to be a case of That's Just Wrong. But it looks a lot more reasonable if you include the bindings for the parameters immediately afterwards, as in a Haskell-style where clause:

x + y
where x = 1
      y = 2

And maybe there's an argument somewhere for reading a backwards definition as:

x + y forSome y forSome x

but, if so, I'm not going to be the one to make it.

The Language Is Dead. Long Live the Language!

All Souls Day is almost upon us, so it seems a fine time to be contemplating everything that has died, and everything that will.

I attended a meetup a couple of months ago billed, in part, as a discussion of the future of Scala. As you might imagine, that's a sufficiently broad topic to be hijacked in interesting ways. But one of the questions that surprised me by its frequency was: does Scala have a future?

Having spent a number of years working on a language whose niche was far smaller than Scala's, I'm accustomed to thinking of Scala as having an enormous community and being extremely well-established. It doesn't seem very likely that it could all just go away, at least not on short notice.

But I've been around long enough to recognize that everything does, without exception, ultimately go away. Scala will too. But Scala's demise probably won't come about because Martin Odersky and everyone he's inspired to work on the language will just decide to leave the world of software and take a vow of silence in a monastery somewhere.

The most likely scenario for the End of Scala is not that it instantly disappears (wouldn't all the code written in it keep running?), and we all have to start over at the beginning using the original version of Fortran from 1957. Instead, I'd expect that Scala's ideas get incorporated into something that the Scala community likes even better—a prospect that is not particularly grim, and maybe even thrilling.

Given that Scala has been less resistant to change than some languages, the Next Big Thing after Scala might just be a newer version of Scala. Then again, it might not. But those of us who, through Scala, have acquired a much richer vision of what programming is all about will never regret having learned it.

A Brief Ceremony

Warning: This post makes use of unconventional notation. If you believe that the One True Meaning of the ASCII characters was revealed for all time to Saints Kernighan and Ritchie, or if you are otherwise firmly attached to the syntax of a particular programming language, read at risk of disgust and disgruntlement.

As I mentioned previously, I've been learning Standard ML as part of Dan Grossman's Coursera course. As usual when one starts to pick up a new language, ML seems remarkably clean and simple—and, as usual, I'm not sure whether that's because it is all that clean and simple, or whether I'm just learning the easy parts first, because that's generally where you start.

The parts of ML we've covered so far in class are focused on the functional basics: declaring a function, invoking a function, passing a function to another function—in short, the lambda calculus. And contemplating the lambda calculus in its many guises is always as pleasurable as watching fluffy clouds drift by in the summer sky.

But one thing that strikes me about ML is that its take on these basics is a bit verbose compared with other languages I've seen. For example:

(* ML *)
let val a = b
    val c = d
in  e
end

seems a lot wordier than Scala's:

// Scala
val a = b
val c = d
e

as well as requiring deeper indentation. And fn to introduce an anonymous function has a lot more visual weight than Haskell's simple backslash.

So all this got me to wondering: just how terse a notation can I come up with for declaring and applying functions? ML and Haskell already use whitespace as the application operator—and that's zero characters if you're not counting whitespace, so I can't imagine how you'd do better.

How about function declaration? All the languages I've ever encountered have distinct syntax for declaring a named function and binding an anonymous function to a name. For example, in Scala you have:

def foo (a: Int, b: Int) = bar

versus:

val foo = (a: Int, b: Int) => bar

and similarly in ML (currying rather than tupling, to keep up with the fashionable):

fun foo a b = bar

versus:

val foo = fn a => fn b => bar

Is there a way to make an analog to the val versions above so simple that the def/fun forms are unnecessary? If so, binding an identifier needs to be pretty concise. The best way I can think of to approach this is to think of the binding operator as an infix operator, as in a = b, with no introductory let or val. However, the equals sign usually has a pretty important role to play in comparisons, and I'd rather not overload it. Ideal would be ≡, which is Unicode character hex 2261 (“identical to”), but the gods of ASCII did not see fit to endow us with that character, and for regrettably many tools, venturing outside of 7-bit territory is still a leap into the mojibake abyss. So I've provisionally settled on:

a ~ b

which defines the identifier a to have the value of the expression b in whatever follows, up to the next scope-closing delimiter.

The next step in overthrowing the tyranny of the fun keyword is an infix lambda operator (about which the author of the Arcane Sentiment blog has done some philosophizing). Although most of the languages I know require some sort of introductory prefix when declaring an anonymous function, in Scala you can get away with:

a => b

provided that the type inference winds are blowing your way.

However, a two-character infix lambda looks pretty hefty to me, particularly if you're going to chain it in a curried function declaration like:

a => b => c => d

On the same basis, I reject /\ (even though it looks like a capital lambda). In fact, even single-character choices with a vague A-frame resemblance to the letter lambda seem to clamor for too much attention when you lay them out:

a \ b \ c \ d    -- does this look like quoted spaces to you?
a / b / c / d    -- would you do this to your division operator?
a % b % c % d    -- a lambda with a bug squashed on it?

What I'm really looking for is something as lightweight as the series comma used when declaring C-style tupled parameters. And then it occurred to me—the comma itself is up for grabs, as in:

a, b, c, d

So now we can turn something like:

val foo = fn a => fn b => bar

into:

foo ~ a, b, bar

There remains one more thicket of verbosity to hack through before we can pose beneath the Mission Accomplished banner, and that is pattern matching. Pattern matching is a sign of civilization as surely as the motorcar and the wireless, and I'd hate to try to present any examples longer than half a line without it. Pattern matching syntax is one of ML's less attractive features, as it requires not one but two keywords to get going:

case foo of
    pat1 => expr1
  | pat2 => expr2
    ...
  | patn => exprn

Scala sort of starts out improving on that by having an infix match keyword:

foo match {
  case pat1 => expr1
  case pat2 => expr2
  ...
  case patn => exprn
}

but then you've got the curly braces and the repeated case keyword, and it all goes to hell.

One way to approach the patterns you're matching is to treat each as a function parameter (oh, didn't I mention that all function parameters are patterns? No, because you already knew that). So given a value to match and a sequence of functions, the pattern matcher's task is to find the first function in the sequence that would be legal to call with the given value as an argument. Indeed, you might say that your sequence of functions is itself a function, and the value to match is its argument, and that's precisely how we'll do it:

f ~ f1 | f2 | ... | fn

is the function that first tries to call f1, then if that doesn't work, f2, and so on up to fn. So we've reduced the above Scala and ML examples to:

(pat1, expr1 | pat2, expr2 | ... | patn, expr2) foo

Now we're just about far enough along to fold something leftwards like:

foldl ~ f, z, ([L], z | a :: as, foldl f (f z a) as)

except that the L in [L] needs some excusing. ASCII just doesn't have enough matching delimiters. At a minimum, you'll want convenient groupers for lists and tuples. And if you start doing anything useful, you'll quickly want shorthand for sets and maps as well. Parentheses and curly braces are off limits, because I'm giving them their usual Scala meaning (mutatis mutandis), and less than and greater than are comparison operators (this isn't XML). That leaves an awful lot of work for the square brackets, so I'm letting the first token after the [ disambiguate, as in:

[T "This" "is" "a" "tuple"]
[L a list]
[S 1 2 3 1]                           -- a set of *three* elements
[M key1 -> value1 key2 -> value2]     -- and a map

As you can see, within square brackets, whitespace is treated as an item separator rather than function application (infix operators are still recognized). You can always parenthesize to call your favorite function:

[T (cos x + sin y) (sin x + cos y)]

And if you're really insecure about having lost your tupling comma, you can use double comma as an infix operator to make a synonym for the above like:

(cos x + sin y),,(sin x + cos y)

One last thought before putting this post to bed. It would be a wonderful universe if we could dispense entirely with a built-in if then else in favor of pattern matching, but even:

(true, expr1 | false, expr2) cond

is awfully talky (not to mention backwards), and I don't see how to trim it down without betraying my logic. So, infixally once more:

cond ? expr1 ! expr2

where exclamation mark takes over for C's colon. The colon is reserved for specifying types, about which, mercifully, I have given no thought whatsoever.

Classes (Not the OO Kind)

Labor Day is well behind us, but it's not too late to go back to school. The proliferation of free online classes means that if you have the time and the curiosity, there's no reason to be ignorant about anything anymore.

The first massive online open courses (MOOCs) I signed up for were Peter Norvig and Sebastian Thrun's AI course and Andrew Ng's machine learning class, offered by Stanford in the fall of 2011. I joined because I'd heard about them on a news story on NPR. NPR was reporting that signups were exceeding all expectations, into the tens of thousands of students (the AI course ultimately had about 160,000). I figured that this was an experiment unlikely to be repeated and I'd better make sure I took advantage of it. Both courses were a lot of fun, and I found myself more motivated to learn and complete the course than if I'd just read books on those topics.

I've taken several more courses since then, both from Coursera and from Udacity, the two companies created after the successes of the Stanford courses in the fall of 2011 (Professor Ng cofounded Coursera, and and Professor Thrun Udacity). None of the classes has been graded quite as rigorously as a typical university undergraduate course, mainly because the constraints of automatic grading (required for classes with thousands of students) mean that a lot of test questions are multiple-choice. That said, the MOOCs have still been a very satisfying experience—I've learned plenty and, I think, retained as much as in a typical in-person class.

Right now I'm taking four Coursera courses: Tim Roughgarden's Algorithms Part 2 (I somehow managed to graduate without taking an algorithms class, but it's never too late); Martin Odersky's Functional Programming in Scala (so far a bit elementary, but everyone I've talked with who uses Scala seems to think it's worthwhile); Michael Geneserth's General Game Playing (I've always wondered how that works); and Dan Grossman's Programming Languages (an excuse to learn ML, Racket, and Ruby, none of which I know).

I still don't understand how so many MOOCs are being offered at absolutely no cost, and maybe it's a business model that won't last. Get 'em while they're hot! (I'm not sure what the Coursera signup deadlines are like, but the General Game Playing and Programming Languages classes have just begun, if you want to join me.)

And finally, if there's something you want to study for which no one has set up a MOOC, the modern world offers you another study alternative besides curling up in a corner with a book. I mentioned previously that the Scala Study Meetup Group is working its way through a textbook; the Bay Area Categories and Types group has been doing the same with Benjamin Pierce's Basic Category Theory for Computer Scientists (I still can't claim to understand much of category theory despite attending the meetups faithfully, but it's a start).

So if there's something you want to learn, don't sit around bemoaning your ignorance. Join a class or start a meetup group, have some fun, and find out just how much more there is to be ignorant about.

Stateless Monad

I read some time ago about the Haskell State monad. I thought, Cool! A fully general way to manage states! Lots of things have states, and they need a lot of managing! But then when I actually found the specification, I couldn't make head or tails of it. I kept scratching my head and squinting at it, and I still couldn't see where in the State monad is the state kept? All I could see was some mechanism for deriving a new state from an old one.

Now, as part of the Scala Study Group meetup in San Francisco, I'm working my way through the early access edition of Paul Chiusano and Rúnar Bjarnason's Functional Programming in Scala. Chapter 6 introduces the State monad (without ever using the word “monad”), and now that I'm working in a more familiar programming language I can finally see that, like so many other things in this confusing world, the State monad is misnamed. An instance of it is not a state; it is a transition rule between states.

Why can't people just say what they mean in the first place? If I ever write my own State monad, it's going to be called Transition.

Heartlessly Endorsed

I suppose there must be a special hell for people who don't take their LinkedIn accounts seriously, and if so I'm headed there full steam. Still, you can imagine my horror when I noticed in the latest missive from LinkedIn (just as I was going to delete it) that several of my acquaintances have endorsed me for my XML skills.

I deplore XML. There are certainly times when you want a human-readable and -editable data format that's not tied to any particular programming language or application, but something like JSON is a lot more succinct. And I've seen plenty of occasions where people used XML for small amounts of information that was tied to a particular programming language or application, where a short piece of program code or a simple text file would have been a lighterweight choice. And though I've been forced to use XML on occasion, I've done my best to block the experience from my mind.

So what's the protocol for unwanted LinkedIn endorsements? Will my contacts be livid if I reject the endorsement? If I accept, does it go on my Permanent Record? And if so, will prospective employers refuse to consider me for any job except shoveling out the XML stables?

Sugar-Free Loops

Sugar-free loops: not a breakfast cereal.

I've recently been playing with a minimalist language that eschews pretty much all syntactic sugar. It has no classes (or typeclasses), no mutable state, no jumps or labels, no modules or packages. It has no libraries—and if it did, they'd be useless, because it has no identifiers with which to name the contents of the libraries.

The language is basically the lambda calculus, plus built-in integers, a few integer functions, and a conditional If. Variables are represented as zero-based De Bruijn indices, using the notation V(i) for the variable in the ith enclosing scope. V is actually a special case of the Var operator, whose argument can be an arbitrary expression rather than just an integer constant—useful if you want to invent arrays.

Calling this thing a “language” is probably an abuse of the term; it's just a data structure with an interpreter.

Although I wouldn't want to program such a thing on a regular basis, I did want to be able to process sequences of varying lengths with it. Given the pure functional nature of the language, this requires recursion. And given the lack of identifiers, the language doesn't do the recursion for me; I need to use an explicit fixpoint combinator. The call-by-value Y combinator in this language looks like:

  fix =
    Lam(
      Lam(V(1)(Lam(V(1)(V(1))(V(0)))))(
        Lam(V(1)(Lam(V(1)(V(1))(V(0)))))))

So I know I'll apply this to my looping function, but what does the looping function look like? Well, you can generally view a loop that computes a value as a fold. But unlike folds in high-level languages, there aren't have any prepackaged sequence operations to use in the fold, so I have to take those operations as parameters. Specifically, my fold (as passed to the Y comnbinator to create a usable recursive fold) will look like:

  λf.λmore?.λhead.λtail.λstep.λaccum.λnext.
    if not more? next then
      accum
    else
      f more? head tail step (step accum (head next)) (tail next)

where more? applied to a sequence tells whether there are any more elements (the sequence is not empty), head provides the current element of the sequence and tail the rest, step performs one step of the fold operation, accum is the value accumulated by the fold, and next is the sequence from which to get the next element. Stripped of sugar, this becomes:

  unfixedFold =
    Lam(                              // f (fold itself): V(6)
      Lam(                            // more: V(5)
        Lam(                          // head: V(4)
          Lam(                        // tail: V(3)
            Lam(                      // step: V(2)
              Lam(                    // accum: V(1)
                Lam(                  // next: V(0)
                  If(
                    Not(V(5)(V(0))),  // not more?
                    V(1),             // no more, return accum
                    V(6)(             // else apply f to
                      V(5))(V(4))(V(3))(V(2))(
                                      // same more?, head, tail, step,
                      V(2)(V(1))(V(4)(V(0))))(
                                      // step(accum,head(next)),
                      V(3)(V(0)))))))))))
                                      // and tail(next)

The only form of input in this language is to bind the input to variables, as if the program were called from within a series of nested functions applied to the inputs. A program to iterate through such inputs and compute the maximum value looks like:

  fix(unfixedFold)(
    Lam(Lt(V(0),Minus(Depth,I(1)))))(   // more?: variable index less
                                        // than lexical depth
    Lam(Var(Plus(V(0),I(1)))))(         // head: index into inputs (add
                                        // 1 to index to account for
                                        // head function itself)
    Lam(Plus(V(0),I(1))))(              // tail: increment index
    Lam(If(Gt(V(0),V(1)),V(0),V(1))))(  // step: max of arguments
    V(0))(                              // accum starts as zeroth input
    I(1))                               // index after zeroth input

Four out of five dentists do not recommend sugar-free languages, at least for their patients without patience.

No Comment

Of all the features ever introduced into programming languages, surely the ability to insert natural-language comments is the worst thought out.

Think about it: have you ever seen a comment of more than one line that wasn't out-of-date by the time you read it? Or, if the comment was more-or-less accurate, one that didn't at least contain distracting misspellings and mispunctuations?

An ideal programming language would let you write all comments in the language itself, so that the compiler could verify that comments are properly structured and consistent with the code they describe.

Now I realize this post is appearing just a few days after April 1st, but I'm not entirely joking. Static type checking is, in effect, a system of compiler-checked comments. Type checking, of course, has a role in avoiding errors—and I do find that I do make type errors that the compiler flags, and I appreciate the ability to correct those errors before runtime. But far more often than the compiler finds a type error in my code, I read the type annotations I've made, because from day to day I tend to forget the types I'm working with at any given point in the code. That is, type annotations—like pretty much everything else in programming language source code—are best thought of as more for human consumption than for the compiler.

One reason I enjoy working with Scala more than Haskell is precisely what many people consider to be a flaw in Scala, namely that Scala can't do type inference in many places where Haskell can. Scala code is consequently littered with type annotations in places where Haskell would omit them—but that means I don't have to look very far to be reminded what anything is. As with natural language, redundancy may take up more space or time in transmission, but if not overdone it's a great aid to comprehension.

I've written some Python, and I enjoy the speed and concision with which you can whip up some code when you don't have to bother with type annotations. But it's not a language I would use for code I planned to work on for a long time, or to share with other people; I don't think I could keep the types clear in my head long enough. Unless, of course, I wrote some natural-language comments to remind me. But then I'd really want the compiler to make sure those comments didn't get out of date.

I'm still looking forward to the compiler that will complain when I write a comment that says “here is an implementation of quicksort” when what I've actually coded is bubblesort. But perhaps, a few years from now, someone will announce such a thing. On April 1st.

Unknown Works of Charles Dickens

It was a little over a year ago that, having just finished up Andrew Ng's machine learning course on Coursera, I was inspired to build a little neural network of my own. I designed it to predict the next character of a sequence of input characters, given the previous 20 characters. Then I set it to work training itself on the text of Charles Dickens's A Christmas Carol, A Tale of Two Cities, and David Copperfield.

I was working on this while on vacation in Morocco. It took the little Atom-powered netbook I had brought with me about 36 hours to finish the training. When it was done, I set it to work generating more characters based on its own output—that is, taking the previous 20 characters of its own output, it would generate a next character, and then another given the trailing 19 characters of the original sequence followed by the newly generated character, and so on.

The result was a series of literary gems like this paragraph:

dodod aS mading a9 bRinoiceataid me cor s8 and tie howe, and the made the for, and said of tartat on dadi beat eo fore add, bow berinod, and was mn of thou in what he Sas, in hadd he baid was withing, mavedaisRoe d a. Ce isable gore and spo~ed ,o arind was Paid sai?,o a dase of be you in for had waice a+m, and I in the keed=ratld Whe, and sbate mawer Ag is, and sNow of the so it was it a fiid and xawis.d&o, with a dowther(ave qpine the wabe do ha d sasbed was of the worbere beAd, comce it hisaid the was bead was it of Bere, I and berq, Winder deadored w!thin the fireaceo fored w; I waacaing waid wor to in the be bor, ?

Has my netbook unearthed what Dickens really meant to say? And should Tolstoy be worried?

I Can See Right through You

I've been doing some reading and thinking about contracts and hybrid type checking, and there's something I haven't seen mentioned yet.

Those of us who use languages with decent support for abstraction are used to thinking of operations that can have different implementations—depending, for example, on the particular class associated with an object.

But there are some operations for which multiple implementations don't really make sense. For example, consider an interface for integers that supports even and odd operations. In a language with nominal typing, you can't get very specific about what these methods return:

  trait Integer {
    def isOdd: Boolean
    def isEven: Boolean
  }

But in a language where your contracts can be more specific, you could say something like:

  trait Integer {
    def isOdd: { _ % 2 == 1 }
    def isEven: { _ % 2 == 0 }
  }

That is, the contract of odd specifies that it returns whether its argument is odd, and similarly for even.

Assuming that you don't mind putting code in your interface, you can make sure that no override of these methods violates the contract by insisting on the implementation:

  trait Integer {
    final def isOdd: { _ % 2 == 1 } = this % 2 == 1
    final def isEven: { _ % 2 == 0 } = this % 2 == 0
  }

Holy redundancy, Batman! The type is the implementation! In fact, if these are pure functions, the types specify the only reasonable implementation of these operations (modulo optimizations, such as using a shift instead of a division operation).

If, like me, you tend to assume that everything you encounter is just a special case of some more general phenomenon, you might want to give this sort of function a name. I'm inclined to use the word transparent, because the function's type acts like a window that lets you see the whole inside of the function—although I'm not sure that term wouldn't lead to confusion with referential transparency, which is something else.

But if this phenomenon is indeed sufficiently common to receive a name, you might want to support it directly in a programming language, with something like:

  trait Integer {
    def isOdd transparently this % 2 == 1
    def isEven transparently this % 2 == 0
  }

On a related note, if a contract is a function, then that function might have a sort of transparency—that is, a reflection facility that let you inspect a contract might not just let you test whether the contract holds of a particular value, but also let you look directly at the code that specifies the contract. An alternative is to hide the contents of the contract, and reveal only whether one contract implies another; but since that is impossible to deduce in general, the reflection system would probably serve you better by giving you the raw code and letting you make of it what you will.

The Y Conspiracy

Some phenomena are so outlandish that to explain them seems to require a conspiracy by the powerful.

For example, consider the modern computer chip. Is it really believable that a tiny piece of slightly adulterated silicon can, when an electric current is passed through it, compute millions of digits of pi? Well, maybe you can swallow the pi, but doesn't it burst the bounds of credulity to accept that it can also show you videos of cute kittens dancing?

Surely there's a more plausible explanation for the technology we all enjoy, preferably an explanation involving wickedness and shadowy forces. Is it possible that the computer companies of the world have made a deal with Satan, and imprisoned damned souls inside their machines, forcing them to do billions of calculations per second under threat of intensified torment?

Alas, my theory doesn't stand up to examination. There are conspiracies in the world, but they don't explain all hard-to-believe phenomena. For a conspiracy theory to be plausible, the conspiracy has to have a small enough number of participants that its details could reasonably remain secret—or at any rate, that has to be more reasonable than the alternatives. Given how much difficulty most people I know have in keeping a secret, my minions-of-Satan hypothesis falls apart if more than about three people are involved in the computer industry. Lacking a better explanation, then, I'll just have to accept the information-processing abilities of dirty sand.

Even more mind-bending are the properties of fixpoint combinators. No matter how many times I step through a demonstration of the Y combinator turning a nonsensical up-by-its-own-bootstraps lambda expression into a tidy well-behaved function, I can't quite convince myself that it could ever really work.

The problem with disbelief in stuff that can be demonstrated mathematically is that you have no freedom to invoke a conspiracy. Not even the Trilateral Commission with a fleet of black helicopters could fool us into putting our faith in the Y combinator if it didn't actually perform as advertised.

I'll just have fall back on the idea that The Lambda Calculus Is Magic.

Landauer vs. the Fan

Darn that !@#$% laptop fan. Why is it running again?

Maybe because I took Stanford's free online courses in artificial intelligence and machine learning last quarter, and I've been running experiments with neural networks on and off since then.

Neural networks are fun and flexible ways of coming up with a function when you really have no clue how the outputs relate to the inputs, but it sure takes a lot of time and electricity to train them. I'm basically turning coal (or whatever the local power plant burns) into functions.

I suppose the fact that we recently put photovoltaic panels on our roof should salve my conscience a little, but it still seems as if it's going to take an awful lot of expensive electrons to train enough AIs to provide us all with robot maids and butlers. Can't we do any better?

A recent Scientific American article suggests that Fujitsu's K Computer has around 4 times as much computational power as a human brain, but uses about half a million times as much energy. There's plenty of room to argue that the K computer and the brain do types of processing that aren't comparable, and even if you ignored that, I imagine there's plenty of fudging in the figure the article cites for the brain. Still, we can probably say that the brain is several decimal orders of magnitude more efficient than a modern electronic computer.

What about the brain itself? Is it actually as efficient as possible, or does physics permit computational systems that use even less energy? Well, it was only recently that I discovered the Landauer limit, which describes the minimum energy required to change one bit of information. The Wikipedia article says that at room temperature, the Landauer limit requires at least 2.85 picowatts to record a billion bits of information per second. I'm not sure what that translates to in flops—maybe a single floating point operation requires recording a thousand bits of intermediate information? If so, a billion bits per second is a megaflop, or less than a billionth of a human brain, per the Scientific American article. If I've done the math right, that leaves the brain only a few orders of magnitude less efficient the room-temperature limit (but fortunately, Landauer says colder computers would do better).

At any rate, physics does leave some room for cooler computers. Maybe I won't have to listen to fan noise every time I hang out with Rosey and Mac after all.

Yes, I Have No Class

OK, I think I do kind of get what's going on with Beta. Yes, function activations are objects, and function bodies are object initializers. (I can find references to this being a concept that Beta inherited from Simula, but what I haven't found is any actual Simula documentation that says Simula does things this way. As far as I can see, Simula has rather conventional-looking, distinct syntaxes for declaring classes and procedures. But Beta has just one syntax for both.)

(There's some other stuff going on in Beta, like the ability to keep a function activation around and rerun it in the same activation frame. This is excusable as an optimization of tail recursion, but letting people do it by hand at arbitrary points in the program is a perfect example of the principle that just because you can think of something, you are not obliged to go off and implement it.)

Not Your Grandpappy's this

To illustrate the activation-as-object idea (without resorting to Beta syntax, which is baffling to the uninitiated), here's a bowdlerized version that I hope won't be too offensive to modern functional sensibilities. Consider a representation of binary expressions:

    def Binary (
        public left: Expr,
        public op: BinOp,
        public right: Expr) =
      this

using the usual ill-defined mongrel syntax. In this case, this is understood not to mean what it would in Java or Scala (the object that owns the function where this appears), but rather the current invocation (or call or activation) of the Binary function itself. So Binary is the name of a class. It's also the name of a function that constructs an instance of the class. We can tell Binary is a class because it returns this. (We could also make the return type of Binary explicit, as in:

    def Binary (
        public left: Expr,
        public op: BinOp,
        public right: Expr): Binary =
      this

but my imaginary compiler for this non-language is somehow smart enough to infer this.)

A class with no features is not very useful. Binary has three features, all functions (because the universe contains nothing except functions and activations of functions. Of course, the functions themselves must be activations of the function constructor function. Does my head hurt enough yet?). I've marked these functions (left, op, and right) with public, not the more Scalaish val, to emphasize that I'm specifying only the visibility of these features, not that they are variables (even constant variables) in the usual sense—because there are no variables in the usual sense, only functions that always return the same value. Things that look like variable bindings are just functions defined always to return the argument (a function activation) passed to them.

A fatter example:

    def Binary (
        public left: Expr,
        public op: BinOp,
        public right: Expr) = {
      def eval: Int =
        left.eval mumble mumble right.eval
      def show: String =
        "(" + left.show + " " + op.show + " " + right.show + ")"
      this
    }

where I suppose the defs should actually be publics for consistency, but this train of thought is still way too half-baked to merit consistency (or unmixed metaphors). Since eval doesn't return an eval, and show doesn't return a show, we know these aren't constructors; they're just plain old functions.

Calling a plain old function, like calling a constructor function, allocates an activation record for the function (at least conceptually). But if the activation never escapes, it becomes garbage as soon as the function returns. An execution environment with a lick of sense would put such a thing on a stack instead of a heap, but let's loftily dismiss that as a mere implementation detail.

Found: One Grail (Slightly Holy)

Anyway, yes, activation-as-object does offer a solution to the puzzle of constructors.

To recap, that puzzle is: what is an object before its constructor is called? Bytecode fans will recall that the JVM constructs an object in two phases, first allocating it with the new instruction, and then invokespecialing its class's <init> method. The JVM verifier ensures that you can't get a hold of the object in between new and <init>, because it's not valid then: it's not a proper instance of its class yet, but (because new had to refer to the class to allocate it), it's clearly not an instance of anything else. It's just a nonthing from which you must avert your eyes.

But function invocation, at least as far as we let ourselves know, is atomic. Once the arguments are prepared, boom!, you're executing the function, with its activation record all nicely laid out for you, and with not so much as an eyeblink in between (assembly language programmers may dissent, but our fingers are firmly in our ears and we can't hear a word they're saying). That means that when objects are activations, there is no object to wonder about before its constructor is called: the object is the call to the constructor.

Further Adventures of a Vague Idea

In this non-language that I'm not describing, every identifier that appears in an expression (as opposed to a type declaration) is the name of a function. If that identifier is followed by an open paren or nothing, it's a function invocation. So left.eval above invokes left, which returns the first argument passed to Binary, and then invokes the eval function that is a feature of left (and presumably of every Expr). An identifier followed by an underscore is a reference to the function itself, as in Scala.

Since classes are functions, Expr _ is properly the name of the type of instances of (activations of, calls to) Expr. But after a colon, the trailing underscore is implied, so we can say left: Expr instead of left: Expr _. You might need the underscore in other contexts, like if (foo.class == Expr _) ....

Another random observation is that in Scala, val and var have different meanings in classes and functions. Declarations in a class can refer to each other (so that functions can recurse, and so on); but variable definitions in a function can refer only to local identifiers declared earlier in the function, not later. Since Non-Language functions are both classes and functions, you'll need some kind of syntax to distinguish between letrec-like declarations and sequential declarations, unless you can persuade yourself that you can do without the latter (can you? I never thought about this).

Hey, Look at the Ducks!

Please distract yourself immediately, lest you come up with questions about how this scheme might relate to inheritance, or parametric types, or anything else complicated. If you must, consider these an exercise for the reader (or for Gilad Bracha, whose Newspeak also borrows ideas, but thankfully not syntax, from Beta).

A Funny Type of Contract

Alex Cruise posted the link on the Scala language mailing list to these slides by Benjamin Pierce (along with Nate Foster and Michael Greenberg). Pierce is the author of Types and Programming Languages (which I confess I'm still working my way through).

Even if you have absolutely no interest in type systems, these slides are worth a look for their punchy visuals. Perhaps Pierce should also teach a course on the effective use of PowerPoint.

What Pierce is getting at (if I understand right) is that type systems can get too heavyweight to be worth the trouble. He's looking at a particularly complex case, that of the Boomerang programming language, so perhaps the typechecking in your favorite language (if it's not Boomerang) may still be lightweight enough not to be under suspicion.

Pierce's conclusion seems to be that contracts (in the form of runtime assertion checks) may have to supplement compiletime typechecking to make the overall problem of verifying program correctness tractable.

I've been thinking for a while that it would be nice if there were some way that types and assertions could be unified. Types constitute a form of contract that is verified at compiletime (and/or loadtime, in languages that do loadtime verification), while assertions are verified at runtime. Runtime assertion checking is easy enough, so the difficulty in bridging the two is coming up with a general way to specify how contracts can be checked at compiletime: this requires giving your compiler and/or loader enough ammunition to do an automated proof, which is extremely hard except for the simplest cases (something like Java's nominal type system, before generics, constitutes a pretty simple case).

Eiffel is the only language I've seen that makes a big deal of method pre- and postconditions in a way that is analogous to typechecking on methods: that is, when you override a method m with a method m′, m′'s postconditions must be more specific than m's (covariantly), but its preconditions must be less specific (contravariantly).

It might be cool if a language had a sort of Third Way with respect to types and assertions, where you could tell the compiler to check a contract at compiletime if the compiler can figure out how (and it doesn't take too long), or at runtime otherwise. Runtime checking is generally inferior to compiletime checking, but most of us would settle for it if the compiletime check would take forever.

Always in Beta

My quest to understand What Programming Languages Are Made Of has led to me start reading the Beta Programming Language book. I've only gotten as far as Chapter 3 so far, but I've already seen enough quirks in the language to have repaid the time.

If I see the implications properly, it looks as if Beta unifies method calls and object construction. That is, the language has no functions or methods per se; rather, all code lives in what would Java or Scala would consider constructors or instance initialization. Instance variables play the role of local variables.

It's easy to observe that stack frames are like objects, in that both are usually laid out as structs accompanied (in languages with managed memory) by a pointer to some sort of descriptor. But it's a bold leap to say that stack frames are objects.

I haven't read far enough to be sure that my understanding is correct. It would also be interesting to see whether Beta has any notion of alternate constructors—which, when viewing Beta objects as functions, would have an effect something like default function arguments.

Is the Beta approach part of the answer to the puzzle of What Are Constructors Made Of? I haven't figured that out yet.

I've seen Beta mentioned a few times, but never heard of anyone using for it anything. I wonder whether it failed to gain traction because people always assumed it was still in beta.