Lambda the Ultimate

A flaw of that WP article is that it doesn't deal with what is usually meant by the simply typed lambda calculus (STLC): it treats Church's simple theory of types, whose type atoms are the base types and with one type constructor for function types, but no kind of polymorphism (except type-indexed definition schemes for terms). But usually the STLC allows Hindley-Milner polymorphism.

Hence there is no type rank in the WP article for the apply combinator, app: A => (A => B) => B, since A and B may have higher type, while this is a term of Hindley-Milner STLC of rank 2.

I can see how this would confuse users of WP.

Sorry, but that is simply wrong. The very meaning of "simply typed" is no polymorphism. The STLC is exactly what the article describes. There is no such thing as a "Hindley-Milner STLC" either. A lambda calculus with H-M-style implicit let polymorphism is typically just called ML in the PL literature. In contrast, "polymorphic lambda calculus" usually refers to something like System F, which is quite different from H-M.

It's true that when people talk about STLC types they often write down type "schemes" like A->B->B. But that is meta notation, and A and B are meta-level variables standing for an arbitrary simple type.

Also, I don't understand what you are saying with the app example. "Rank" is yet another notion, it usually refers to the amount of quantifier nesting in a polymorphic type, and consequently, it does not belong into an article on the STLC. Either way, the apply function does not have higher rank, it's perfectly rank 1.

The very meaning of "simply typed" is no polymorphism

I don't think this assertion is defensible. Church-style typing decorates lambda terms with enough type annotations so that each typable term has exactly one non-schematic type. Whereas Curry-style typing does not provide type information to lambda terms, being in a sense underspecified, which means that typable terms may admit many possible type assignments. With the benefit of the Hindley-Milner algorithm, we see that there is a principal type, and this is the type obtained from algorithm W.

The original reference for the simply-typed lambda calculus is Curry & Feys (1958), which used Curry-style typing — this was natural since they wanted to model Hilbert-style proof theory, which uses a precisely analogous form of formula scheme.

There is no such thing as a "Hindley-Milner STLC" either.

I invented the term, because I thought Hindley-Milner polymorphism would be more immediately comprehensible than the explanation I gave above about Church-style and Curry-style typing. I should have made this clear.

A lambda calculus with H-M-style implicit let polymorphism is typically just called ML in the PL literature

Note that this is a more sophisticated form of polymorphism. The Church style vs. Hindley-Milner-style STLC are exactly equivalent in terms of the lambda terms they define. Whereas terms with ML-style let statements cannot be translated into the STLC without blowing up the size of the term.

So ML-style polymorphism, and system F, don't have much to do with the point I was making.

It's true that when people talk about STLC types they often write down type "schemes" like A->B->B. But that is meta notation, and A and B are meta-level variables standing for an arbitrary simple type.

Both Church-style and Curry-style formalisms use schemes. One is polymorphic, the other isn't.

"Rank" is yet another notion

I have often been careless about the conventions regarding use of the terms rank, order, and degree: I apologise for any confusion that might result.

Either way, the apply function does not have higher rank, it's perfectly rank 1.

The app function I defined has order two according to the definition of order in the WP article you cited.

Postscript — I now think I see, following Derek Dreyer's post, what the reference to ML-style and system-F-style polymorphism was doing: the idea is that there is no polymorphism without explicit quantification over types.

With the benefit of the Hindley-Milner algorithm, we see that there is a principal type, and this is the type obtained from algorithm W.

Except this principal type isn't itself expressible in the STLC. Suppose we have this (use the usual encoding of let, a and b are metavariables):

let id = \x.x in                      -- id :: a -> a
  let tru = \x y.x in                 -- tru :: a -> b -> a
    tru (id 1) (id "Goodbye world!")  -- type error

It doesn't type because the term id would have to hold two different types simultaneously and STLC won't express that. It doesn't have 'many forms', it has exactly one which we're free to pick to suit its use sites.

You've nicely explained why encoding ML's let construction in the STLC requires a blow-up in size. The reference to algorithm W in my post was not concerning its application to ML, but to the STLC.

I'm not aware of any encoding short of copying the term fresh for each variable use, and I'd be hard pressed to call that an encoding of the ML semantics for the definition. My point stands: the STLC still doesn't have any meaningful degree of polymorphism.

It is exactly the copying translation I meant — I hoped the repeated mention of the size blow-up would make that clear. You can define a relational semantics between the two classes of term.

I'm not going to argue about "meaningful" again. Well, at least I hope not.

Church-style typing decorates lambda terms with enough type annotations so that each typable term has exactly one non-schematic type. Whereas Curry-style typing does not provide type information to lambda terms, being in a sense underspecified, which means that typable terms may admit many possible type assignments. With the benefit of the Hindley-Milner algorithm, we see that there is a principal type, and this is the type obtained from algorithm W.

<RANT>
The distinction is pretty commonly made, but I don't think "Church-style vs Curry-style" is actually well-defined. Well, yes, it is used often in the concrete sense of saying something very specific about type annotations—but in those cases I don't think it's a particularly relevant distinction for programming languages. On the one hand, we know that always placing annotations on lambdas is overkill for STLC, but on the other hand we know that for type systems even slightly more expressive than STLC, at least some annotations are needed for type checking. So both Church and Curry are the "wrong" approaches to typechecking (unsurprising since they were invented many decades ago, and not for typechecking).

So for the sake of argument assuming equal treatment of type annotations, the more informal distinction people are interested in is whether the "meaning" of a term depends on its type, or whether types are a way of classifying these type-free meanings. Reynolds calls this "intrinsic" vs "extrinsic" semantics. But this is actually a false dichotomy: you can always build a more refined extrinsic semantics on top of an intrinsic semantics (what's called "refinement typing", "soft typing", etc.), and conversely you can always see at least a very coarse intrinsic layer underneath an extrinsic semantics, if you squint hard enough (e.g., the "uni-typed" lambda calculus). So we shouldn't be setting Church and Curry against each other—they can get along just fine.

See in particular Frank Pfenning's Church and Curry: Combining Intrinsic and Extrinsic Typing.
</RANT>

...and to tie Pfenning's paper back to your remark, I think what you're claiming (and I kind of agree with) is that Hindley-Milner polymorphism should be treated as "infinitary intersection", which is an extrinsic view. But I'm not sure that this is what is usually meant by STLC.

The fact that in a Curry-style formulation there are multiple types that may be assignable to a term, and that there is a principal type scheme of which all those types are instances, has zero to do with whether the language supports polymorphism.

I'll agree with you that you are using what I take to be the normal usage of the term "polymorphism", but I find Charles' interpretation quite interesting nonetheless.

Consider the term λx.x in a Curry-style type assignment. Doesn't it have to be implicitly quantified over all types, sort of the way that first-order free variables are implicitly quantified in the untyped case?

Not quite the same as the explicit polymorphism you are referring to, but possibly an interesting way to look at it.

I don't understand what you mean by "implicitly quantified". The typing *rule* for lambda terms is of course a rule schema that is quantified over the argument and result types of the lambda, but lambda terms themselves are just pieces of syntax -- they're not quantified over anything.

Moreover, under Charles' "interpretation" of polymorphism, is there any non-trivial type system that does *not* (under a Curry-style formulation) "support polymorphism"? If not, then his interpretation renders "polymorphism" meaningless.

I don't understand what you mean by "implicitly quantified"

The idea is that invoking a rule schema is implicitly quantifying over something. (What indexes the instances of the schema?) It's implicit because the formal system doesn't necessarily specify a quantification over what explicitly.

Moreover, under Charles' "interpretation" of polymorphism, is there any non-trivial type system that does *not* (under a Curry-style formulation) "support polymorphism"?

My understanding, based on what he said, would be that this kind of implicit polymorphism is characteristic of the Curry-style formulation. I understand him to be making a bigger distinction between Curry and Church than merely when typing occurs.

It's not the way I have usual thought about it (I've tended to see "six of one, half a dozen of the other" in Curry vs. Church), but I still find it an interesting way to think about it. It's made me stop and consider it, which I appreciate.

If not, then his interpretation renders "polymorphism" meaningless.

I wouldn't say meaningless, just making a different distinction. It's not like "polymorphism" isn't already a heavily overloaded term. ;-)

If you want a real and interesting distinction between Church and Curry style presentations of the lambda calculus consider the following exercise from "Lectures on the Curry-Howard Isomorphism."

The eta reduction rule for pairs is as follows (using a Haskell-like notation): (fst p, snd p) ~> p

Show that the simply typed lambda calculus (in Andreas' understanding) with pairs and eta reduction in a Curry-style presentation does not have the subject reduction property, while in a Church-style presentation it does. Subject reduction means that if E has type T then if E reduces to E' then E' has type T.

under Charles' "interpretation" of polymorphism, is there any non-trivial type system that does *not* (under a Curry-style formulation) "support polymorphism"? If not, then his interpretation renders "polymorphism" meaningless.

What is the "under a Curry-style formulation" qualification doing? There are plenty of non-polymorphic languages out there, and so the distinction between polymorphic and non-polymorphic languages is perfectly meaningful.

To "support (or allow) polymorphism" means to have universally quantified types like Forall a. T in the language. Thus, the STLC, by definition, does not support polymorphism.

I've twice now been told I am wrong by definition; neither time were sources cited.

Strachey, 1967, Fundamental Concepts in Programming Languages, which introduced the notion of parametric polymorphism, nowhere talks of formal operations of quantification over types, let alone types built out of type quantifiers. Is parametric polymorphism, to avoid speaking of ad-hoc polymorphism, by definition not polymorphism?

Actually, it was always my impression that Strachey intended "parametric" to mean any polymorphism in which a single definition is understood as applying to parameters of more than one type — as opposed to separate definitions for different types, which he called "ad hoc polymorphism" (for which I'm inclined to use the non-pejorative "selection polymorphism" rather than "ad hoc"). So that everything he (or I) could think of that qualifies as polymoprhism would be, by definition, either parametric or ad hoc. When Cardelli and Wegner came out in 1985, it seemed to me that it was (whether through error or intent) promoting an unfortunate redefinition of Strachey's term "parametric polymoprhism". The distinction between error and intent being rather murky in that situation, since a true believer in OO might, without conscious connivance, tend to perceive things in a way that would "show" that OO fundamentally differs from all that preceded it.

The currently relevant point being, I suppose, that it is not necessarily safe to treat Strachey's terminology and Cardelli and Wegner's terminology as if they are both subsets of a single consistent whole.

Though not as historic, one standard reference would be Barendregt's 1992 handbook chapter on Lambda Calculi with Types. It clearly identifies "polymorphic" with the presence of quantified types, and "simply-typed" with their absence. (It also introduces both the Curry-style and the Church-style formulation of the polymorphic lambda calculus.)

OK, we are getting somewhere. Two things:

First, Barendregt mentions intersection types, which fall outside his classification of simply typed vs. polymorphic. Therefore, it is not clear to me that he can have intended his distinction to be taken generally, as opposed to a distinction he was making for his purposes of this article.

Secondly, his definition of types for the STLC uses free type variables, not predetermined base types, so that type schemas are themselves types, and so the type system contains the principal types for all terms. This is not the case for the system described in the WP article, and this difference between these two formulations of the STLC was one of the two that I originally remarked upon. And it is this difference that I distinguished by using the term polymorphic.

It's been instructive for me to see that there could be such disagreement among us over the meaning of such a widely used and technical term as "polymorphic".

He is a logician, so he uses variables where more PL-oriented presentations (like the WP article) use base types. You need either notion for the STLC to actually be able to form types. Formally, both amount to the same thing in the STLC.

It's been instructive for me to see that there could be such disagreement among us over the meaning of such a widely used and technical term as "polymorphic".

Indeed. :-) I still maintain that I haven't seen any text using "polymorphism" in conjunction with a simply-typed language, like you do. Strachey's paper is not really a counter-example, as it does not formally present any type system to start with. That's not surprising, as it comes from a time before polymorphic types where fully understood (Girard's and Reynold's works inventing the polymorphic lambda calculus came later).

Berghofer and Nipkow (2000, Proof terms for simply typed higher-order logic) use the term schematic polymorphism for exactly the polymorphism I describe.

This seems like reasonable terminology to me. The term is not widespread, though. One could contrast schematic polymorphism to the fully fledged functional polymorphism, where types may be functions from types to types. If we liked this distinction, we might get carried away and call ML-style polymorphism, nested schematic polymorphism.

There may be some scientific culture issue going on, as well. I attended a talk by Samson Abramsky which sketched his view of what theorists of programming languages were up to; he talked of subtyping in OO languages being a kind of polymorphism, but not one that should be called ad hoc.

Note that universal types are not "functions from types to types". Those would be type constructors, or higher-kinded types. That's yet another concept different from parametric polymorphism - you can have each without the other. (That said, type constructors like list are often informally called "polymorphic types", but strictly speaking that is inaccurate.)

Re OO: "subtype polymorphism" indeed is common terminology. IIRC, there is an old paper by Cardelli that explains different forms of polymorphism (parametric, subtype, ad-hoc, etc), but I don't have a link right now. Either takes you out of the realm of "simply-typed".

You may be thinking of Cardelli and Wegner 1985, which is the paper I was saying I thought used "parametric" in a sense different than Strachey's (but I haven't reread it in years). It's available on Cardelli's site, here. If that's not it, perhaps you're thinking of one of the others of these.

I'm not entirely sure it was the one I had in mind, but likely. Thanks for repeating the pointer.

Note that universal types are not "functions from types to types". Those would be type constructors, or higher-kinded types.

I understand the distinction you are making, but I can't help but wonder if this is an absolute conceptual necessity, or merely some hoop-jumping needed to avoid impredicativity.

This distinction would seem more fundamental to me if you could never "instantiate" a universal type. For example, with ∀τ:τ→τ (necessarily the identity), if you never "filled the τ" to a more specific typed identity.

In the "Theorems for Free" sense, the parametric type constructors and the universal types pattern together in putting strong constraints on what can inhabit them, so it doesn't seem unreasonable to have a term that unites them. (Which, as you say, is informally "parametric polymorphism"; perhaps informal usage is on to something.)

Other than preserving predicativity, the only other formal advantage I can see to this scheme is that it preserves the paradigm of the type cube and the hierarchy it implies, and disallows Charles' usage, which has a rival paradigm. ;-)

This distinction would seem more fundamental to me if you could never "instantiate" a universal type. For example, with ∀τ:τ→τ (necessarily the identity), if you never "filled the τ" to a more specific typed identity.

I don't see how you would typecheck terms if universal types would never be instantiated?

If you are suggesting that the distinction just is a more or less random design choice on part of old type system designers, then no. It is fundamental. When you try to build a model, at the latest, you see that universals and lambdas have totally different logical/semantic meaning.

There may be some scientific culture issue going on, as well. I attended a talk by Samson Abramsky which sketched his view of what theorists of programming languages were up to; he talked of subtyping in OO languages being a kind of polymorphism, but not one that should be called ad hoc.

I bet he just meant it literally. My (partial & incomplete) understanding of the history there goes like this:

Back in the 1980s, Reynolds and Oles introduced functor category models of stack allocation, and then it was noticed (I don't know by who) that there was an analogy between "subtyping as record extension" and stack allocation extending the stack. Ma (another of Reynolds's students, who had studied polymorphism) then made use of this analogy to give an embedding of System F into a system with subtyping and intersection types.

Meanwhile there was a bunch of work on bounded quantification going on, and Plotkin and his collaborators synthesized the 'Penn view' of bounded quantification as coercion insertion to turn Ma's work backwards and explain subtyping as a use of polymorphism. (I am definitely not mentioning a lot of important people and their work here -- don't take this as a proper scientific history.) At the same time, guys like O'Hearn, Tennent, and Reddy were pushing the original local allocation stuff further, to exploit the analogy between polymorphism and natural transformations to formally model encapsulation in OO languages as a form of parametricity.

So it's not totally crazy to think that OO polymorphism (at least for some idealized OO language) really is honest polymorphism suitably construed. But this whole line of research seems to have fizzled out; I suspect it just was too mathematically sophisticated/heavyweight for its own good.

Does your intuition correspond to the depth of the most-nested arrow, left-nested or otherwise? The left-nesting convention is common because of currying - a series of right-nested arrows is equivalent to a function taking an n-tuple.

My intuition actually agrees with the recursive function definition where the order is the most left-nested arrow of the left and right types of the initial function. Below I give an example. The "most left-nested" ignoring the right part of the type does not seem intuitive to me as I show in the example because it completely ignores the output.

The recursive formula presented and the next sentence are not equivalent to my understanding. Because it only refers to the left part of the function and not the right.

Not sure what exactly you mean, but admittedly, the wiki sentence is a bit terse. It says "most left-nested". That means, how deep are function arrows maximally nested left-hand of the arrow? Or try drawing types as a tree. Then "most left-nested" means: how often can I maximally go left in the tree (not necessarily in consecutive steps) before I reach a leaf?

Now just try out the order formula on a couple of examples and see how it coincides with that intuition.

So imaging we are using First-Order Logic with Lambda Calculus and we have a expression of the type:

( e -> (( e -> t) -> t) ) FO: lambda-x.lambda-P.(P@Bob /\ person(x))

My intuition tells me that this expression is second order since P has a function as input.
If we look at the "most left-nested", we have "e" and therefore this is a first order expression.
If we use the recursive function, then since the right hand of the arrow is a second order type, then the whole function is second order.
So the recursive function and the text next to it give different orders.

I hope this example helped to make more clear what I mean.
Thanks.

According to the definition on wikipedia? (Just glanced at it). [Forget it]

It is second order according to the recursive function defined there, but not regarding the text explaining it right next to it.

By the way, I am thinking about just defining my own definition based on intuition and referencing some other similar definitions.

You are confusing "most left-nested" with "nested left-most". ;-)

Note again: "most left-nested" means: how often can I maximally go left in the tree (not necessarily in consecutive steps) before I reach a leaf? That does not imply that I may only go left on that path. So, in your example, you go R-L-L to reach the inner e.

So looks like that was the key of the question :)
Thank you for clarifying that little language misunderstanding. (Clapping!)

So now that my intuition is pretty clear, the only thing left is to formalize it, explain the intuition and put examples since I won't have anything to reference to.

Thanks.