## Naive Question? Definition of "Higher Order"

The more papers I read, the more I see the term "higher order" applied to seemingly anything. We have HO (high order) programming, HO programming languages, HO functions, HO modules. Those readily come to mind, although I am confident I can find other applications of HO to other terms in computer science.

So what *is* the exact meaning of "higher order." Does it have one precise definition? Or maybe one broader, generally applicable definition? Or is the term simply misused?

Thanks much.

Scott

## Comment viewing options

To my knowledge, the terms "first order" and "higher order" originate in logic.

In that context, "first order" refers to a system where propositions are built from atoms and quantification ranges over the universe of atoms. A logic is "higher order" if it allows quantification to range over objects derived from the first (or subsequent) order, i.e. more complex than atoms.

You can see how this would generalize. Start with some basic objects and build a first order of objects from them. When you go to build something new from the parts you built in the first order, you have moved to a higher order.

(Incidentally, this is conceptually very similar to how Hofstadter uses the term "meta" in GEB; each higher level allows you to "comment" on the level below it.)

### I've had a similar intuition

I've had a similar intuition to that, + the post below about.

Also, if something is first class, it is of the highest order (that the language supports)? The relation between these two terms is fuzzy: I use both frequently, but never saw a precise definition.

... though I'm not sure that more precision than the existing intuition is useful for understandable use :)

### not quite, but good work!

Sometimes, the hardest part of solving a problem is asking the right question. I would never have thought to ask myself whether the words "first class" and "high-order" were related. So thank you for doing the hard work!

Now, the easy part. No, I do not think that "first class" means "of the highest order available". This just doesn't match with the current use of the word "first class". Functions are first class because they can be manipulated as values, not because they can manipulate other functions as values. In a first-order language without any higher-order anything, functions cannot take other functions as input. Yet functions, like everything else in the language, are first-order, the highest order supported by the language. This still doesn't make them first class.

Now, the reason why I think your question is interesting is because even though your intuition was incorrect, it points in a new and promising direction. If, before I encountered your question, I was asked to define the word "first class", I would have said that a construct was first class if it could be passed as an argument, returned as a value, and stored in a variable. This might be true, but it's a very limiting definition! For one thing, you can only apply it to languages that have arguments, return values, and variables.

Now that I have encountered your question, however, I would try to define "first class" in terms of first-order and high-order constructs. Let me try that now.

A construct is first class if there is another construct that can manipulate it. Therefore in a first-order language, only the atoms are first class. In a language with higher-order constructs, each construct (of level n) can be manipulated by a higher-order construct (of level n+1), therefore the constructs of all levels are first class. If the language supports different ways of manipulating things (passing as arguments, returning as values, storing in variables...), a construct is only deemed first-class if it can be manipulated in all the available ways.

### Ah, right, I was going for,

Ah, right, I was going for, more succinctly, "if something is first-class, it may be manipulated by something of a higher-order." Not sure your "all" quantification is necessary -- in a language mixing functions and relations, it seems enough for a value to be used with at least one of them.

I'm unclear on ordering. A first-order function can't manipulate functions, only atoms. A second-order function can only manipulate atoms and functions over atoms, right? What happens when we hit infinity? Can we go higher -- aleph-order? Is this even useful?

### One, two, infinity...

What happens when we hit infinity? Can we go higher -- aleph-order? Is this even useful?

While in principle you could go to infinity, in practice you probably want a small finite number.

The normal count of orders is "first order, higher order" or "first order, second order, higher order": it would seem that thinking about too many levels at once leads to confusion.

For usefulness as a logic, you want the number of levels to be finite, since you want to have finite derivations for all objects.

For an interesting example of higher order constructions of arbitrary size, consider the Type type in Coq. Though you don't actually notate it, it is assumed that a type that is defined over a term of Type n is itself of Type n+1.

Great example!

### Example

In ML:

  datatype foo = Bool of b | Fun of (foo -> bool)


A function that accepts a foo does not have a well-defined order. We can view a recursive type as its unfolding, and so a program that accepts a foo has to be ready for potentially unbounded unrollings of foo, which can give you arbitrarily left-nested arrows in your type.

### Large-cardinal type theory

An omega-order has all finite types, but no transfinite types. You can go higher, by adding predicative universes in the sense of Martin-LÃ¶f's type theory. These are the same as adding predicative quantification over types, i.e., quantifiers over types which, at rank 1, only range over types without quantifiers, and at rank n>1, range over types whose highest rank quantifier is no more than n-1.

You get a kind of ordinal hierarchy this way, with each rank of type quantification introducing a new limit ordinal. The ordinal type of this type system, with quantifiers at all ranks, and all functions over these types, will be omega^2 (I think; this isn't the usual ordinal measure on universes).

By allowing functions that return universes as arguments, you can get much higher ranks: Erik Palmgren's contribution "On universes in type theory" to 25 Years of Constructive Type Theory describes how, following work of Michael Rathjen, you can provide constructions analogous to the construction of Mahlo sets in Kripke Platek set theory. I don't think this is available for download, but Anton Setzer (1998) explained the idea in Extending Martin-LÃ¶f's set theory by one Mahlo universe.

### Most of it's fairly

Most of it's fairly predictable derivatives of the higher order in higher order functions. When I see "higher order programming [language]", I think of programming using higher order functions. Similarly, we have higher order module systems where functors (as an analogue of functions) can act on functors.

I'm leaving aside the application to logic here though - someone else can cover that.

### Nth-order logic

First-order logic is by convention a predicate logic that quantifies over a specified universe of individuals; second-order logic, by a weaker convention, permits, in addition, quantification over sets of individuals; third-order then allows quantification over sets of sets of individuals.

For higher-order logic, quantification over sets can be replaced by quantification over many-placce relations or over functions. Leon Henkin proposed a logic, many-sorted logic that allows all of these to be mixed together, with a semantics based on the lambda-calculus. Many-sorted logic is essentially (non-constructive) type theory in disguise.

It's not hard to see the connection to nth-order in functional programming.