Monday, November 16, 2009

What is the logic of ML values?

Before approaching the question, "What is the logic of ML values?", I first want to explain why there is more subtlety to the question than is often assumed.

(Warning: this is a long post on something which most people probably care very little about. On the other hand, there are 19 google hits for "logic changed my life".)

In general, how does one interpret the question, "What is the logic of X?", for some programming language X? A standard response is that the logical theorems are exactly the inhabited types, i.e., types τ such that there is a closed term t:τ. But what are the "terms"? The answer is obvious enough in simple formal systems where there is only one typing judgment, and so we can say things like, "The inhabited types of simply-typed lambda calculus are exactly the theorems of minimal implicational logic". Yet, real programming languages usually have many different typing judgments, since programs are composed out of many different syntactic objects. In ML, in particular, a program includes some let-bound values and expressions, some function definitions, and a result expression (in addition to datatype definitions, module definitions, etc., which are classified by different kinds of "types").

(In this post, "ML" is meant in a slightly fuzzy but essentially unambiguous way, as a call-by-value language with effects. To settle a concrete interpretation, I will be giving examples in Standard ML of NJ, which notably provides the control operator callcc. "Value" is meant in the standard operational sense, i.e., a value is a fully evaluated ML expression. We can similarly ask, "What is the logic of Haskell values?", but that is a different, trickier question, to which I'm still not sure of the answer.)

When answering the question, "What is the logic of ML?" (or "What is the logic of Haskell?"), the standard approach is to gloss over these different syntactic categories, and assume we are talking about expressions. This makes some sense, insofar as this is the largest syntactic category: all values and functions are also expressions. And expressions also have easy-to-understand principles of composition. For example, the rule of application—from two expressions e₁:σ→τ and e₂:σ, we can form the expression (e₁ e₂):τ—witnesses the logical principle of modus ponens. Whereas from two values v₁:σ→τ and v₂:σ, the application (v₁ v₂):τ is no longer a value.

Yet, I believe it is a mistake to define "the" logic of a programming language in this way, without realizing there is finer structure. That is why I phrased the question, "What is the logic of ML values?", rather than full-stop, "What is the logic of ML?" And so how does the logic of ML values differ from the logic of ML expressions?

Well, it is often claimed that ML (and likewise Haskell) defines an inconsistent logic. This is a statement about the logic of expressions. For example, non-terminating expressions such as

fun loop() = loop()
inhabit every type, as do exception-raising expressions, such as
fun fail() = raise (Fail "inconsistent!?")
(Note: the expressions here are loop() and fail(). Here and below, I assign names to expressions by declaring them as thunks.) But none of these are values. Indeed, evaluation of the first expression will never yield a result,
- loop();
(* waiting a long time... *)
whereas the second will return immediately, but with an exception rather than a value:
- fail();
uncaught exception Fail [Fail: inconsistent!?]
raised at: stdIn:2.3-3.5
(There are some additional complaints about the value restriction when evaluating these polymorphic expressions, but for our purposes we can ignore them here.) In fact, the logic of ML values is consistent, as we can see by defining the empty type:
data void = Void of void
There are no values of type void, since the only way to construct one is by already having one. Note, though, that all bets are off "under a lambda"—we can still build a value inhabiting any function type σ→τ, for example
fun fnfail() = fn _ => raise (Fail "inconsistent!?")
Let's try to be a bit more precise about what happens before we reach that point.

Another folk theorem about "the logic of ML" is that insofar as it is consistent (i.e., if you avoid things like unrestricted recursion and exceptions), with the addition of control operators it becomes classical. We can import the relevant SML/NJ library and see what they mean:

- open SMLofNJ.Cont;
opening SMLofNJ.Cont
type 'a cont = 'a ?.cont
val callcc : ('a cont -> 'a) -> 'a
val throw : 'a cont -> 'a -> 'b
val isolate : ('a -> unit) -> 'a cont
(* ... *)
As first observed by Griffin, the type of callcc corresponds logically to the classical principle of Peirce's Law. We can make this a bit easier to see by defining another control operator letcc, which essentially does the same thing as callcc but with first-class ML functions, rather than values of the cont type:
- fun letcc f = callcc (fn k => f (fn x => throw k x));
val letcc = fn : (('a -> 'b) -> 'a) -> 'a
Using letcc, we can derive the law of excluded middle, ∀α.α ∨ ¬α. To represent this type, we first introduce a type constructor for disjunctions:
Now we can witness excluded middle as follows:
fun excluded_middle() : ('a,'a -> void) either =
letcc (fn k => Right (fn x => k (Left x)))

So what happens when we attempt to evaluate this expression? (To avoid complaints about the value restriction, we instantiate the type variable 'a at some arbitrary type a.)

- excluded_middle() : (a,a -> void) either;
val it = Right fn : (a,a -> void) either
And now, in contrast to what happened above with the evaluation of loop() and fail(), here we actually get a value!

So can we say that the logic of ML values really is classical? Well, we evidently can under the "bag of tautologies" view of logic. But that is not necessarily the most useful view.

If we look up at the above ML session, a shockingly anti-classical principle is already staring back down at us. After evaluating excluded_middle(), we got back this value:

That is, not only is this a proof of α ∨ ¬α, but in fact it contains a proof of the right side of the disjunct, ¬α. This is an instance of the intuitionistic disjunction principle, that a proof of a disjunction is a proof of one of the two disjuncts.

The punchline, I would say, is that the logic of ML values is not unsound, and not classical, but simply constructive. What is an ML value of type τ? Just an intuitionistic proof of τ—but in a non-empty context. This context includes the current continuation of type ¬τ, as well as all of the other effects that can be invoked underneath a lambda, i.e., in values of functional type.

Okay, so what have we brushed over here? Well first, the restriction that effects are only invoked underneath lambdas can actually be enforced by CPS translation. Functions σ→τ are interpreted as ¬(σ∧¬τ), where ¬(-) denotes minimal negation, i.e., ¬τ = τ→β, for some fixed parameter β, the return type. Effectful operations are encoded as things that return β. Second, I said that a value of (a CPS translated) type τ is an intuitionistic proof of τ (in a non-empty context of effects), but are all such intuitionstic proofs values? Well, no, because some proofs involve "detours". To be concrete, if M₁ and M₂ are proofs of σ and τ, then π₁(M₁, M₂) is a proof of σ—yet, #1 ("hello", "world") is typically not considered to be a value (it evaluates to "hello"). (Some people like to call expressions like #1 ("hello", "world") "valuable".) Third, to say that there is a "logic" of ML values, we really do have to explain what its composition principles are, and not just which principles fail. I might revisit some of these points in another post.

Finally, the whole idea of a "logic of ML values" is very close to the idea of the realizability interpretation of ML. Some people believe that realizability is a distinct and very different alternative to Curry-Howard as a constructive interpretation of logic. My point with this post was mainly to suggest that Curry-Howard need not exclude realizability-like interpretations, once we realize (so to speak) that there is more than one syntactic category of proofs.


Andrej Bauer said...

If you consider ML values as proof terms for some unknown logic, then it looks like you will get a restricted form of implication elimination (modus ponens), since an application need not result in a value, as you observe. Have you or someone else thought about what this form is?

Noam said...

Hello Andrej. So if we ignore the second point, and just view "values" as "valuable expressions" (let's call them values*), then we can literally interpret values of type τ as identical to intuitionistic proofs of τ* (in a context of effects), where τ* is defined as:

(σ × τ)* = σ* ∧ τ*
(σ + τ)* = σ* ∨ τ*
(σ → τ)* = σ → (τ → β) -> β

(This translation is sound for proper values as well.)

Expressions of type τ, on the other hand, we interpret as proofs of β, abstract in a continuation of type τ* → β.

So the difference between "the logic of values" and "the logic of expressions" is a single double-negation.

The rest is an exercise in CPS. For example, the left-to-right pairing construct on expressions takes k:σ*→β.E₁ and k:τ*→β.E₂ and builds k:(σ*∧τ*)→β.E₁[k := λx.E₂[k := λy.k(x,y)]]. We can similarly describe application of one expression to another, with left-to-right evaluation. But we can also describe application of one value to another, building an expression. Intuitionistically, given v₁:σ* and v₂:σ*→(τ*→β)→β, we can form k:τ*→β.v₂ v₁ k.

We can also derive some composition principles that just involve values. For example, given v₁:σ* and v₂:τ* we can form (v₁,v₂):σ*∧τ*. Given v₁:σ* and x:σ*.v₂:τ* (a value abstract in a value variable), we can substitute v₂[x := v₁] and the result is still a value.

(We might consider *internalizing* this substitution principle as another type constructor, representing a pure function space on values. This is something we don't have in ML, and I don't understand very well. But Alex Simpson has looked at this recently...see his POPL09 talk.)

Noam said...

(It looks like I second-guessed the terminology "values*" there, probably for the best...)

And non-termination is of course important too. I think a good way to model ML is to say that we are allowed to introduce cycles when building "proofs" of β. (In call-by-push-value, we can use recursion when defining computations. In polarized type theory, we can use recursion to define values of negative type.)

Neel Krishnaswami said...

Hi Noam,

Your translation of functions reminds me of something about System F I have always found curious: any type A is isomorphic to forall α. (A -> α) -> α.

To go backwards, you can just instantiate α with A, and then pass the identity function. Because of this impredicativity, the isomorphism is stable under basically any type constructors you feel like adding to the language.

So the sense in which you are holding β abstract has to be subtly different from type abstraction in the System F sense. It's not "you must be parametric over any choice of result", but rather "there is a globally unique choice of result which you must not look at".

Speculating wildly, I wonder if this might suggest some way to find some constructive content in Hilbert's choice operator....

Noam said...

Neel, all I can say is that yes, that seems like a very important point, and I've been thinking about it...