(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();whereas the second will return immediately, but with an exception rather than a value:

(* waiting a long time... *)

- fail();(There are some additional complaints about the

uncaught exception Fail [Fail: inconsistent!?]

raised at: stdIn:2.3-3.5

*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 voidThere 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;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:

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

(* ... *)

- fun letcc f = callcc (fn k => f (fn x => throw k x));Using letcc, we can derive the law of excluded middle, ∀α.α ∨ ¬α. To represent this type, we first introduce a type constructor for disjunctions:

val letcc = fn : (('a -> 'b) -> 'a) -> 'a

data ('a,'b) either = Left of 'a | Right of 'bNow 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;And now, in contrast to what happened above with the evaluation of loop() and fail(), here we actually get a value!

val it = Right fn : (a,a -> void) either

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:

val it = Right fn : (a,a -> void) eitherThat 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.

## 5 comments:

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?

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.)

(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.)

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....

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

Post a Comment