Catacomb Composition Algorithm

catacomb.md

Composition

Composition is the act of taking a stack and a function, and producing the type signature of the resulting stack. It can also be equivalenty seen as the composition of two functions' execution.

1. Generate constraints from the stated type sigs of your functions.
2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
   • Base types: Fail if one is not a parent type of the other. Otherwise, move on.
   • Both function types: Add a constraint {a -- b} = {c -- d} and run step (4) early. If this produces an invalid constraint, try again by introducing a new variable x and adding constraints {x a -- x b} = {c -- d} and x = All* instead of the original one.
   • One is a variardic type: Run step (4) early to figure out the type of your variaric type. It should always be determinable from here (because finite types always come first). Expand the variadic type in question in-place, and try matching again.
   • Else: generate a constraint a = b and move on.
3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols. Save these for step (5).
4. Compute the closure of the constraint set. Here are some basic rules:
   • {A -- B} = {C -- D} to A = C and B = D
   • A?B = C?D to A = C and B = D
   • A = B and B = C to A = C
   • A = B to B = A (maybe? Is this an equality or subtyping relation?)
   • A = B A to B =
   • A B = C D to A = C IFF B and D are finite types
   • A B = C D to B = D IFF A and C are finite types
   • A B C = D and B = E to A E C = D (an extension of the transitive property above)
   • A B = A C to B = C
5. Find the combined signature of the first unification that succeeds. If you unify a -- b x and c x -- d, where x is the matched portion and b/c are unmatched ones, you get c a -- b d. Note that either b or c must be empty because of how matching works.
6. For each type variable, find all the consrtaints the mention it and find the most specific type among them. Replace.

Examples

UNIFY (-- {(?) -- Int?Int}.) AND (C A {C A -- C A?B} -- C B; *A; *B; *C.):
    CONSTRAINTS:
        A = All*
        B = All*
        C = All*
        MATCH {(?) -- (?)?Int} = {C A -- C A?B}
        (?) = C A
        (?)?Int = A?B
        (?) = A
        Int = B
        (?) = C (?)
        C = 
    WE KNOW:
        A = (?); B = Int; C = ;
    FINALLY:
        C A -- C B
        (?) -- Int

UNIFY (-- Int Int {Int Int -- Real}) AND (A {A -- B} -- B; *A; *B):
    CONSTRAINTS:
        A = All*
        B = All*
        MATCH {Int Int -- Real} = {A -- B}
        Int Int = A
        Real = B
    WE KNOW:
        A = Int Int; B = Real;
    FINALLY:
        -- B
        -- Real

UNIFY (-- {Int -- Real}) AND ({Int Int -- Int Real} --):
    CONSTRAINTS:
        MATCH {Int -- Real} = {Int Int -- Int Real}
            Int = Int Int
            Real = Int Real
            INVALID
        MATCH {A Int -- A Real} = {Int Int -- Int Real}; A = All*
            A Int = Int Int
            A Real = Int Real
            A = Int
            VALID
        WE KNOW:
            A = Int;
        FINALLY:
            --
            --

Problems

Function expansion of {a--b} to {c a--c b} is nice and all, and accurately reflects how functions work, but is it sound inside composition? Does it generate cases where the type signature informs the behavior of the function? That would be bad.