# 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.