A Question About Types in ETCS In Rethinking set theory, in which an axiomatization of set theory called ETCS is introduced, Tom Leinster writes:

First we state the data to which our axioms
  will apply:
  • Some things called sets;
  • for each set X and set Y , some things called
  functions from X to Y

So, in ETCS there are some sorts (sometimes also called "types"). One sort is set.
In fully formal ETCS, Todd Trimble writes:

The usual presentation [of ETCS] involves two sorts, objects and morphisms.

Is it right that ETCS, then, has only the two types "set" and "function"?
Or, to be precise, is there a type "function from A to B" for each sets A, B? That is: Is there (for A, B sets) a separate type "function from A to B"?
Or, to put it in other words: Does ETCS has a infinite number of types or a finite number of types?
 A: The "number of types" is not an interesting question, since you can always compute new types. e.g. the typical two-sorted formulation of categories only names two types: $C_0$ the type of objects and $C_1$, the type of morphisms, but just from the data of the two-sorted theory you can construct lots more types, like $C_n$, the type of composable $n$-tuples of morphism. e.g. $C_2$ is the type of pairs $(x,y)$ satisfying the binary relation $\mathrm{dom}(x) = \mathrm{cod}(y)$.
The one-sorted formulation just uses $C_1$, but you can still recover the two-sorted formulation from it, with $C_0$ being the type of things satisfying the unary relation $x = \mathrm{dom}(x)$.
(a relevant idea along these lines is the syntactic site of a theory)

The question you are asking seems to be about the third formulation where a category consists of objects, and a family $\hom(A,B)$ of sets of morphisms for each pair of objects $A,B$.
The usual formulation of this idea in many-sorted logic (as I'm familiar with it) is essentailly indistinguishable from the two-sorted formulation, since one encodes the family $\hom$ as being a morphism $(\mathrm{dom}, \mathrm{cod}) : C_1 \to C_0 \times C_0$.
To formalize this approach directly, I think the right formalism is dependent type theory, something I'm mostly unfamiliar with.
A: If you want to set up ETCS in many-sorted first-order logic, you definitely don't want to use a sort "Sets" together with a bunch of sorts "Functions from $A$ to $B$" for each pair of sets $A$ and $B$. The reason is that there's no way to enforce via a first-order theory that every pair of sets (elements of the sort "Sets") there's a corresponding sort of functions (unless the "Sets" sort is finite). You can always use compactness to add new elements to the "Sets" sort, but the collection of function sorts is specified syntactically and can't grow. To put it another way, many-sorted first-order logic doesn't have a way of parameterizing sorts by elements of another sort - though dependent type theory does, as alluded to in Hurkyl's answer.
A better approach is to use two sorts ("Sets" and "Functions") and include functions symbols $\text{dom}\colon \text{Functions} \to \text{Sets}$ and $\text{cod}\colon \text{Functions} \to \text{Sets}$ which associate to each function its domain and codomain. Then, given any pair of elements $A$ and $B$ of sort Sets, you can define $\text{Fun}(A,B)$ by the formula $\varphi(x,A,B):(\text{dom}(x) = A\land \text{cod}(x) = B)$. This gives a parameterized family of definable subsets of the sort Functions which act exactly like the dependent sorts you had in mind.
