8
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • $\begingroup$ 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 $\endgroup$
    – Jake
    Commented Oct 27, 2014 at 5:26

3 Answers 3

Reset to default
8
$\begingroup$

Okasaki's Functional Pearl, "Even Higher-Order Functions for Parsing or Why Would Anyone Ever Want To Use a Sixth-Order Function?" answers this question with a type of order 6.

Improve this answer
$\endgroup$
6
$\begingroup$

This is a very interesting question!

Andrej Bauer wrote a very nice blog post, 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.)

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Basil
    Commented Oct 27, 2014 at 17:06
4
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.