## Type Checking and Type Inference

This section provides a description of the algorithm for checking
well-typedness and inferring types of Cat functions.

The primary and auxiliary stacks in Cat can be viewed as a pair
of tuples. Every function
expresses a mapping from a pair of a tuples to another pair of tuples.
We can express the consumption and production of a function type
using the following short hand notation, where index 0 represents
the type at the top of the stack.

primary consumption = PC = (pc0, pc1, ..., pcN)
auxiliary consumption = AC = (ac0, ac1, ..., acN)
primary production = PP = (pp0, pc1, ..., pcN)
auxiliary production = AP = (ap0, ap1, ..., apN)

From this notation the types of two functions can be expressed as:
f : (PC(f), AC(f)) -> (PP(f), AP(f))
g : (PC(g), AC(g)) -> (PP(g), AP(g))

The superset relation of tuples as follows:
(a0, a1, ..., aN) >= (b0, b1, ..., bM)
iff (N > M) and forall i=0 to M (ai = b0)

A Cat function is well typed according to the following
function definition:
welltyped(f . g) iff
PC(g) >= PP(f) or PP(f) >= PC(g)

Consider the following definitions of addition and subtraction:
(a0, a1, ..., aN) + (b0, b1, ..., bM)
= (a0, a1, ..., aN, b0, b1, ..., bM)
(a0, a1, ..., aN) - (b0, b1, ..., bM)
= M > N | (b[N+1], b[N+2], ..., bM)
M <= N | ()

Using these definition we can define the consumption and
production of the compose of the two functions as follows:
PC(f . g) = PC(f) + (PC(g) - PP(f))
AC(f . g) = AC(f) + (AC(g) - AP(f))
PP(f . g) = PP(g) + (PP(f) - PC(g))
AP(f . g) = AP(g) + (AP(f) - AC(g))

Putting this together the type of two consecutive functions is:
f . g : (PC(f) + (PC(g) - PP(f)), AC(f) + (AC(g) - AP(f)))
-> (PP(g) + (PP(f) - PC(g)), AP(g) + (AP(f) - AC(g)))

That is all there is to it. I know it's a bit dense, but hopefully it can still be of some use. If you have some suggestions on how I can make it more clear, and use more standardized language or notation I would be very appreciative. Even if you just point out the confusing bits, that would be very helpful!