In programming languages with records, objects, or traits, it is common to
have operators that allow dropping, updating or renaming some components. These operators
are useful for programmers to explicitly deal with conflicts and
override or update some components. While such operators have been
studied for record types, little work has been done to generalize and study their
theory for other types.

This paper shows that, given subtyping and disjointness relations, we
can specify and derive algorithmic implementations for
a general type difference operator that works for other types,
including function
types, record types and intersection types. When defined in this way, the type difference algebra
has many desired properties that are expected from a subtraction
operator. Together with a generic \emph{merge} operator, using type
difference we can generalize many operations on records formalized in the
literature. To illustrate the usefulness of type difference we create
an intermediate calculus with a rich set of operators on expressions of arbitrary type, and
demonstrate applications of these operators in \emph{CP}, a prototype language
for \emph{Compositional Programming}. The
semantics of the calculus is given by elaborating into a
calculus with \emph{disjoint intersection types} and a merge operator. We
have implemented type difference and all the operators % presented in this paper
in the CP language. Moreover, all the calculi and related proofs
are mechanically formalized in the Coq theorem prover.