What is the formal definition of a variable? What is a variable? 
I know that a ($n$-ary) connective can be thought of as a function from $\{ 0,1 \}^n$ to $\{ 0,1 \}$.
And a quantifier over $M$ can be thought of as a set of subsets of $M$. 
What is the corresponding way to think of a variable ranging over $M$ ?

You can see Categorial grammar and, in detail : Sara Negri & Jan von Plato, Structural Proof Theory (2001), Appendix A.2 : CATEGORIAL GRAMMAR FOR LOGICAL LANGUAGES [page 221].

In propositional logic, no structure at all is given to atomic propositions, but these are introduced just as pure parameters $P, Q, R$,..., with the categorizations
$P : Prop, Q : Prop, R : Prop$, ...
Connectives are functions for forming new propositions out of given ones. We have the constant function $\bot$, called falsity, for which we simply write $\bot : Prop$.
Next we have negation, with the categorization :
$Not: (Prop)Prop$.

And so on ...

We can put predicate logic into [this] framework [...] if we assume for simplicity that we deal with just one domain $\mathcal D$. The objects, individual constants, are denoted by $a, b, c$,.... Instead of the propositional constants $P, Q, R$,..., atomic propositions can be values of propositional functions over $\mathcal D$, thus categorized as $P : (\mathcal D)Prop, Q : (\mathcal D)(\mathcal D)Prop$, and so on. Next we have individual variables $x, y, z$ , . . . taking values in $\mathcal D$. Following the usual custom,
  we permit free variables in propositions. Propositions with free variables are understood as propositions under assumptions, say, if $A : (\mathcal D)Prop$, then $A(x) : Prop$ under the assumption $x : \mathcal D$. Terms $t,u,v$,... are either individual parameters or variables. The language of predicate logic is obtained by adding to propositional logic the quantifiers Every and Some, with the categorizations
$Every : ((\mathcal D)Prop)Prop$
$Some : ((\mathcal D)Prop)Prop$.
These are relative to a given domain $\mathcal D$. Thus, for each domain $\mathcal D$, a quantifier over that domain is a function that takes as argument a one-place propositional
  function $A : (\mathcal D)Prop$ and gives as value a proposition, here either $Every(A)$ or
  $Some(A)$.

