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