Typechecking for justified nets

In the last post I wrote a program that attempts to normalise interaction nets with justifications.

data Tm a b
    = Link a
    | Opt b (Tm a b) (Tm a b)
    | On  b (Tm a b) (Tm a b)
    | Exp b (Tm a b)
    | At  b (Tm a b)
    | Fan b (Tm a b) (Tm a b)
    | Pair  (Tm a b) (Tm a b)
    | Index Bool (Tm a b)
    | Read       (Tm a b)
    | Drop
    deriving (Show, Eq)

-- Remember that each "Fan"
-- has been separately annotated with which duplicates it is constructing.

I'm not certain about few details with Danos-Regnier criterion and not sure how to implement it in Haskell. Therefore I'm likely not implementing the typechecking this time.

When examining the normaliser I noticed that if the justifications get interleaved it will cause the currently used duplication strategy to fail. I think this means that justifications have to "stack" over each other.

If you have a link x behind Opt a (Exp b x) ..., then every other link behind "Exp b" must be similarly behind "Opt a" as well. Though, this results in a very strict graph. If I have two products that are interacting, then another of them must split into two. Eg.

Opt a (On b _ _) (On c _ _),
On  a (Opt b _ _) (Opt c _ _)

This can be condensed into a rule: If justification has a parent justification, then that justification must be a parent for the justifications across the structure.

Once we assign types for every term, we can use Danos-Regnier criterion to verify whether it's a valid interaction net overall.

The type assignments would be the following:

Link          : a, when matching opposite link is a as well.
Fan j x y     : a, when (x : a) and (y : a)

Drop          : Unit

Opt j x y     : a&b, when (x : a) and (y : b)
Index False x : a+b, when (x : a)
Index True x  : a+b, when (x : b)
On j x y      : a, when (x : a) and (y : b)

Exp j x       : !a, when (x : a)
At j x        : ?a, when (x : ?a)
Read x        : ?a, when (x : a)
Drop          : ?a
Pair x y      : ?a, when (x : ?a) and (y : ?a)

Pair x y      : a ⊗ b, when (x : a) and (y : b)
Pair x y      : a ⅋ b, when (x : a) and (y : b)

There's still one rule with "Link": Each link must appear exactly twice and they have to appear within the same justification.

Similar posts