What are benefits of foundations with more than one sort of objects? Amongst different foundations of mathematics, $ZF$ and $NF$ are talking about "sets" but $MK$ and $GB$ are talking about two sorts of objects "sets" and "classes".
What are benefits of studying the axiomatic systems with more than one sort of objects even if they are conservative relative to $ZF$? Is it just because theorems about proper classes have simpler forms in such systems in comparison with corresponding theorem schemas in $ZF$ or it is because we lose some useful information and power of the theorems on proper classes when we reduce them to $ZF$? If the last is true, what are the examples of such harmful reductions? Does the same phenomenon happen for sets as same as proper classes too? In the other words, do $GB$ or $MK$ in some sense tell us "more" about sets and proper classes than $ZF$?  
 A: The premise of the question seems undercut by the fact that both GB and MK have formulations solely in terms of classes, that is, in terms of only one kind of object. In these formulations, one can define the sets simply to be those classes that are $\in$-related to another object.
Some set theorists finds these single-object-type presentations to be more elegant, but many other set theorists prefer the two-sorted presentations, simply because they are more naturally related to and extend the ZFC account.
A: I would like to address the part of the question about whether allowing classes beyond those that are definable over the model adds to our understanding of the properties of sets/classes. For instance, the famous Kunen inconsistency showing that there cannot be an elementary embedding $j:V\to M$ is nearly trivial to prove if we assume that $j$ is definable. Kunen's sophisticated argument is required to show that there cannot be such a class embedding in any model of ${\rm GBC}$. The existence of classes beyond those that are definable can also be useful in model theoretic ultrapower constructions. If $M$ is a (set) model of ${\rm GBC}$, we can construct ultrapowers of $M$ by using an ultrafilter on its proper classes. In particular, this method allows us to build end-extensions of models of set theory. By controlling what types of classes exist in $M$, we can obtain end extensions with different desired properties. 
