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)))
  

     (a0, a1, ..., aN) >= (b0, b1, ..., bM)
     iff (N >= M) and forall i=0 to M (ai = bi)

     Let T be a tuple representing the primary stack
     welltyped(f . g) iff 
       T >= PC(g) and  
       T - PC(g) + PP(g) >= PC(f)

     PC(f . g) = max(PC(g), PC(g) + (PC(f) - PP(g)))
     PP(f . g) = max((), (PP(g) - PC(f)) + PP(f))

     (a0, a1, ..., aN) >= (b0, b1, ..., bM)
>      iff (N >= M) and forall i=0 to M (ai = bi)
> 

     Let T be a tuple representing the primary stack
>      welltyped(f . g) iff 
>        T >= PC(g) and  
>        T - PC(g) + PP(g) >= PC(f)
> 

     PC(f . g) = max(PC(g), PC(g) + (PC(f) - PP(g)))
>      PP(f . g) = max((), (PP(g) - PC(f)) + PP(f))
> 

     PC(f . g) = max(PC(g), PC(g) + (PC(f) - PP(g)))
>      PP(f . g) = max((), (PP(g) - PC(f)) + PP(f))
> 

define f { 5 true } 

f : ()->(bool int)

f : ()->(int bool)

    define g { swap dup }
    Will have it's type inferred by the compiler as:
    g : (A:any B:any)->(B B A)

PP(f . g) = max((), (PP(g) - PC(f)) + PP(f))

    let Ta be a tuple (a0, a1, ..., aN)
    let Tb be a tuple (b0, b1, ..., bM)
    
    when N >= M, Ta - Tb = (a[M+1], ..., aN)
    when N < M, Ta - Tb is not defined