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.