§ SSA as linear typed language

• Control flow is linear in a basic block: ie, we can have a sea of nodes representation, where each terminator instruction produces linear control flow tokens: br: token[-1] --> token[1]. brcond: token[-1] -> -> (token[1], token[1]), return: token[-1] -> (). This ensures that each branching only happens once, thereby "sealing their fate. On the other hand, reguar instructions also take a "control token", but don't consume it . so for example, add: token[0] -> (name, name) -> name.

• Next question: is dominance also somehow 'linear'?
• Answer: yes. We need quantitative types. When we branch from basic block Ainto blocks B, C, attach 1/2A to the control tokens from (%tokb, %tokc) = br cond %cond0 B, C. Now, if someone builds a token that's at a basic block D that is merged into by both B, C, they will receive a "full" A that they can use. Pictorially:

       A
       ...

   B        C
[1/2A]     [1/2A]
       D
       1A