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