![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
higher-order snowclones
Oct. 18th, 2010 12:50 amoccasionally you'll hear someone ask, "are higher-order functions 'higher-order' in the same sense as higher-order logic?" here is a possible answer.
from my understanding of current logical diction, something like the following story is true:
once upon a time, humans invented lambda calculus. they said, "a function that takes a functional argument (or returns a functional value) is a higher-order function." they wrote that definition down, and then two different humans read it.
the first said, "ah! a 'higher-order' function is one that operates on a function. so, in general, for something to be 'higher-order' means it operates over functions."
the second said, "ah! a higher-order function is a function over functions. to generalize, a higher-order X is an X that operates over other Xes."
error! and from their teachings sprang many logician progeny of both lineages, and the confusion remains.
some examples:
- higher-order abstract syntax. "lam : (tm -> tm) -> tm" is higher order in that "oh look there's a left nested arrow", i.e. we're describing syntax in terms of function types (and for that reason may be better deserving of the abstract higher-order syntax coin).
- higher-order judgment. in twelf lingo we use this to mean, again, a judgment over open terms (like (tm -> tm) -> type) rather than what you might think following generalization (2), a judgment about judgments (i.e. a metatheorem).
- higher-order logic. if we squint for the sake of uniformity and pretend that by "logic" we mean "predicates", then i think it's accurate to interpret this as an instance of generalization (2), predicates over predicates. it certainly doesn't mean "logic about functional data", which is just propositional logic.
despite my NPOV efforts, it might be coming through that i'm a little annoyed with generalization 1. it just seems a little bit provincial or narrow-sighted, like the only thing that we could possibly want to get fancy with is the types of the things we describe, rather than the (quite literally) more judgmental-methodology-motivated notions of our system. of course, in practice, i use the jargon that will get me understood, but if i got to prescriptively reinvent it i'd change the word for generalization 1 to something like "functional" (where of course in this perfect universe, "functional programming" would be renamed to "value programming").
from my understanding of current logical diction, something like the following story is true:
once upon a time, humans invented lambda calculus. they said, "a function that takes a functional argument (or returns a functional value) is a higher-order function." they wrote that definition down, and then two different humans read it.
the first said, "ah! a 'higher-order' function is one that operates on a function. so, in general, for something to be 'higher-order' means it operates over functions."
the second said, "ah! a higher-order function is a function over functions. to generalize, a higher-order X is an X that operates over other Xes."
error! and from their teachings sprang many logician progeny of both lineages, and the confusion remains.
some examples:
- higher-order abstract syntax. "lam : (tm -> tm) -> tm" is higher order in that "oh look there's a left nested arrow", i.e. we're describing syntax in terms of function types (and for that reason may be better deserving of the abstract higher-order syntax coin).
- higher-order judgment. in twelf lingo we use this to mean, again, a judgment over open terms (like (tm -> tm) -> type) rather than what you might think following generalization (2), a judgment about judgments (i.e. a metatheorem).
- higher-order logic. if we squint for the sake of uniformity and pretend that by "logic" we mean "predicates", then i think it's accurate to interpret this as an instance of generalization (2), predicates over predicates. it certainly doesn't mean "logic about functional data", which is just propositional logic.
despite my NPOV efforts, it might be coming through that i'm a little annoyed with generalization 1. it just seems a little bit provincial or narrow-sighted, like the only thing that we could possibly want to get fancy with is the types of the things we describe, rather than the (quite literally) more judgmental-methodology-motivated notions of our system. of course, in practice, i use the jargon that will get me understood, but if i got to prescriptively reinvent it i'd change the word for generalization 1 to something like "functional" (where of course in this perfect universe, "functional programming" would be renamed to "value programming").
