While this question is not research-level, I think many mathematicians would not know how to answer it. I propose we keep it.

In usual logic texts first-order logic is done over a single sort, i.e., we assume a fixed universe of discourse. Terms denote elements of the single universe. For example, in the theory of a group the universe is the group, in set-theory it is the class of all sets, etc.

But this need not be so, we can have a first-order logic with many sorts. A typical example is the theory of a module, where the two sorts are the ring and the module. Another example is the theory of a graph, where the two sorts are the vertices and the edges. In classical logic various tricks may be played that allow us to replace the sorts with their disjoint union (define operations arbitrarily when they don't make sense and fix the axioms appropriately). If one studies first-order theories in general this is a very useful trick, which is why logicians always stick to singe-sorted theories. But in particular cases it makes little sense to replace several natural sorts with a single unnatural one.

However, in computer-sciency applications such tricks are unacceptable. Therefore we keep many sorts. In fact we go a step further and organize sorts into a type theory (and call the sorts types). It is common for a type theory to have type constructors that generate infinitely many types.

To answer your question, suppose we want a first-order logic in which we are allowed to speak about functions $A \to B$ as well as functionals $(A \to B) \to C$. Then we work in simple type theory, whose type constructors are the cartesian products $\times$ and the function space $\to$. Only well-typed terms are admitted, and all quantifiers must range over specific types. Thus we can write things like $\forall F : (A \to B) \to (A \to B) . \exists f : A \to B . F(f) = f$. This is still first-order logic on top of a type theory.

You can read more about this kind of formal systems in Bart Jacobs's book "Categorical Logic and Type Theory". Constructive mathematicians also prefer formalizations of this sort, for example Peter Aczel has been advocating logic-enriched type-theory for a while.

While this question is not research-level, I think many mathematicians would not know how to answer it. I propose we keep it.

In usual logic texts first-order logic is done over a single sort, i.e., we assume a fixed universe of discourse. Terms denote elements of the single universe. For example, in the theory of a group the universe is the group, in set-theory it is the class of all sets, etc.

But this need not be so, we can have a first-order logic with many sorts. A typical example is the theory of a module, where the two sorts are the ring and the module. Another example is the theory of a graph, where the two sorts are the vertices and the edges. In classical logic various tricks may be played that allow us to replace the sorts with their disjoint union (define operations arbitrarily when they don't make sense and fix the axioms appropriately). If one studies first-order theories in general this is a very useful trick, which is why logicians always stick to singe-sorted theories. But in particular cases it makes little sense to replace several natural sorts with a single unnatural one.

However, in computer-sciency applications such tricks are unacceptable. Therefore we keep many sorts. In fact we go a step further and organize sorts into a type theory (and call the sorts types). It is common for a type theory to have type constructors that generate infinitely many types.

To answer your question, suppose we want a first-order logic in which we are allowed to speak about functions $A \to B$ as well as functionals $(A \to B) \to C$. Then we work in simple type theory, whose type constructors are the cartesian products $\times$ and the function space $\to$. Only well-typed terms are admitted, and all quantifiers must range over specific types. Thus we can write things like $\forall F : (A \to B) \to (A \to B) . \exists f : A \to B . F(f) = f$. This is still first-order logic on top of a type theory.

Such a logic would become higher-order if we included a type $\Omega$ of truth values and axioms which related formulas and functions mapping into $\Omega$. One would expect a comprehension-style schema which related formulas $\phi(x)$ with $x$ of type $A$ and functions $f : A \to \Omega$. Second-order quantification $\forall F . F(\dots)$ can then be expressed as $\forall f : A \to \Omega . f(\dots)$.

You can read more about this kind of formal systems in Bart Jacobs's book "Categorical Logic and Type Theory". Constructive mathematicians also prefer formalizations of this sort, for example Peter Aczel has been advocating logic-enriched type-theory for a while.