<p><a href="http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp98sixth.pdf">Okasaki's Functional Pearl, "Even Higher-Order Functions for Parsing or Why Would Anyone Ever Want To Use a Sixth-Order Function?"</a> answers this question with a type of order 6.</p>

CC BY-SA 3.0
2014-10-26T15:36:43.677Z
2014-10-26T15:36:43.677Z
jbapple
<p>This is a very interesting question! </p>

<p>Andrej Bauer wrote a very nice blog post, <a href="http://math.andrej.com/2006/03/21/interesting-higher-order-functionals/"><em>Interesting Higher Order Functionals</em></a>, which is precisely about this question. He defined a "genuine" function of order $n$ as one which is not expressible in terms of functions order $k &lt; n$ plus typed lambda-calculus. He points out there are only a few known examples of order 3, and he knows of <em>zero</em> examples of order 4. </p>

<p>He also mentions that Paul Taylor does use some very unusual fourth-order functions in his program of Abstract Stone Duality. These are not "genuine" in Andrej's sense, in that they are definable as typed lambda terms, but they are definitely not trivial stackings of known constructions. (In some sense ASD exists to give them intellectually sensible types.) </p>

CC BY-SA 3.0
2014-10-27T17:06:41.383Z
Right, I quickly read Bauer's post after cody mentioned it; it is indeed a nice one and I had somehow missed it, so thanks to both of you.
Basil
CC BY-SA 3.0
2014-10-27T13:01:50.747Z
2014-10-27T13:01:50.747Z
Neel Krishnaswami
<p>The <a href="https://hackage.haskell.org/package/mtl-1.1.0.2/docs/Control-Monad-Cont.html" rel="nofollow">continuation monad</a> in Haskell has got some nice order 3 examples</p>

<pre><code>withCont :: ((b -&gt; r) -&gt; a -&gt; r) -&gt; Cont r a -&gt; Cont r b
</code></pre>

<p>There's some discussion on <a href="http://math.andrej.com/2006/03/21/interesting-higher-order-functionals/" rel="nofollow">Andrej's blog</a>, but they don't really get past order 3...</p>

CC BY-SA 3.0
2014-10-26T17:21:34.780Z
2014-10-26T17:21:34.780Z
cody
<p>This is admittedly a rather naively put and vague question, and I'm not sure how much more specific I want or can make it, but I'll try.</p>

<p>By "practice" I mean surely in actual programming practice (of which I embarrassingly don't know much), but also in <em>mathematical</em> practice, whenever certain higher-type objects are employed as examples or counterexamples within arguments.</p>

<p>By the "height" of a type, I don't mean to include the obvious and natural arbitrariness involved in objects like, say, the fixpoint functional (in fact, in the spirit of the question, I would prefer to understand this as a type $2$ object "up to parameter types", so to speak). A better example of what I mean would be the well-known (from mathematical practice, at least) <em>fan functional</em>, of type $((\mathbb{N} \to \mathbb{B}) \to \mathbb{N}) \to \mathbb{N}$, given by
$$
\lambda f. \mu m. \forall_{\alpha, \beta}
\left(
\forall_{n &lt; m} \alpha(n) = \beta(n) \to f(\alpha) = f(\beta)
\right) \ ,
$$
where $f : (\mathbb{N} \to \mathbb{B}) \to \mathbb{N}$ and $\alpha, \beta : \mathbb{N} \to \mathbb{B}$.</p>

<p><strong>My questions</strong>: Are there any objects of yet higher type than $3$ (possibly "up to parameter types") that are naturally used in the literature? In practice?</p>

CC BY-SA 3.0
2014-10-27T05:26:55.623Z
It is also perhaps interesting to note that while the type might not be an higher than 3 or so (cody's example) that you might want to instantiate a quantified type varible in a 2nd or 3rd order function with other another 1st or 2nd order function  type thus creating, subtly if we are talking about Hindly Milner, somthing as large as a 5th order function. Kinda rare but I am sure I have done this at some point. 6th order is pretty insane though. I've accidentally made some huge order functions playing around with Church numerals if I recall as well
Jake
<reference-request><computability><type-theory>
How high are the higher types that appear in practice?
Basil
# How high are the higher types that appear in practice?

(Asked by: username_0 on 2014-10-26)

This is admittedly a rather naively put and vague question, and I'm not sure how much more specific I want or can make it, but I'll try.

By "practice" I mean surely in actual programming practice (of which I embarrassingly don't know much), but also in *mathematical* practice, whenever certain higher-type objects are employed as examples or counterexamples within arguments.

By the "height" of a type, I don't mean to include the obvious and natural arbitrariness involved in objects like, say, the fixpoint functional (in fact, in the spirit of the question, I would prefer to understand this as a type $2$ object "up to parameter types", so to speak). A better example of what I mean would be the well-known (from mathematical practice, at least) *fan functional*, of type $((\mathbb{N} \to \mathbb{B}) \to \mathbb{N}) \to \mathbb{N}$, given by
$$
\lambda f. \mu m. \forall\_{\alpha, \beta}
\left(
\forall\_{n < m} \alpha(n) = \beta(n) \to f(\alpha) = f(\beta)
\right) \ ,
$$
where $f : (\mathbb{N} \to \mathbb{B}) \to \mathbb{N}$ and $\alpha, \beta : \mathbb{N} \to \mathbb{B}$.

**My questions**: Are there any objects of yet higher type than $3$ (possibly "up to parameter types") that are naturally used in the literature? In practice?

**Tags:** reference-request, computability, type-theory
> **Comments:**
> **username_1**: It is also perhaps interesting to note that while the type might not be an higher than 3 or so (cody's example) that you might want to instantiate a quantified type varible in a 2nd or 3rd order function with other another 1st or 2nd order function  type thus creating, subtly if we are talking about Hindly Milner, somthing as large as a 5th order function. Kinda rare but I am sure I have done this at some point. 6th order is pretty insane though. I've accidentally made some huge order functions playing around with Church numerals if I recall as well  

---

## 3 answers

### Answer by username_2 on 2014-10-26. Score: 8 | Accepted answer

[Okasaki's Functional Pearl, "Even Higher-Order Functions for Parsing or Why Would Anyone Ever Want To Use a Sixth-Order Function?"](http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp98sixth.pdf) answers this question with a type of order 6.


---

### Answer by username_3 on 2014-10-27. Score: 6

This is a very interesting question!

Andrej Bauer wrote a very nice blog post, [*Interesting Higher Order Functionals*](http://math.andrej.com/2006/03/21/interesting-higher-order-functionals/), which is precisely about this question. He defined a "genuine" function of order $n$ as one which is not expressible in terms of functions order $k < n$ plus typed lambda-calculus. He points out there are only a few known examples of order 3, and he knows of *zero* examples of order 4.

He also mentions that Paul Taylor does use some very unusual fourth-order functions in his program of Abstract Stone Duality. These are not "genuine" in Andrej's sense, in that they are definable as typed lambda terms, but they are definitely not trivial stackings of known constructions. (In some sense ASD exists to give them intellectually sensible types.)

> **Comments:**
> **username_0**: Right, I quickly read Bauer's post after cody mentioned it; it is indeed a nice one and I had somehow missed it, so thanks to both of you.  

---

### Answer by username_4 on 2014-10-26. Score: 4

The continuation monad in Haskell has got some nice order 3 examples
withCont :: ((b -> r) -> a -> r) -> Cont r a -> Cont r b

There's some discussion on Andrej's blog, but they don't really get past order 3...


---

