Embedding Logic in Haskell

Logic.hs

{-# Language DataKinds, TypeOperators, TypeFamilies, GADTs #-}
import Prelude hiding (Left,Right)

-- based of figure 1 of https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf

data a :* b = Product a b

data a :+ b = Left a | Right b

type family a :++ b where
 '[] :++ y = y
 (x ': xs) :++ y = x ': (xs :++ y)

data Logic assumtion conclusion where
 Identity :: Logic '[a] a
 ExchangeSwap :: Logic  (x ': y ': gamma) a -> Logic (y ': x ': gamma) a
 ExchangeRot :: Logic (x ': y ': z ': gamma) a -> Logic (y ': z ': x ': gamma) a
 Constraction :: Logic (a ': a ': gamma) b -> Logic (a ': gamma) b
 Weakening :: Logic gamma b -> Logic (a ': gamma) b
 IntroduceImplication :: Logic (a ': gamma) b -> Logic gamma (a -> b)
 EliminateImplication :: Logic gamma (a -> b) -> Logic delta a -> Logic (gamma :++ delta) b
 IntroduceProduct :: Logic gamma a -> Logic delta b -> Logic (gamma :++ delta) (a :* b)
 EliminateProduct :: Logic gamma (a :* b) -> Logic (a : b : delta) c -> Logic (gamma :++ delta) c
 IntroduceSumLeft :: Logic gamma a -> Logic gamma (a :+ b)
 IntroduceSumRight :: Logic gamma b -> Logic gamma (a :+ b)
 EliminateSum :: Logic gamma (a :+ b) -> Logic (a : delta) c -> Logic (b : delta) c -> Logic (gamma :++ delta) c

-- example from paper

example :: Logic '[a -> b, a] (a :* b)
example = ExchangeSwap $ Constraction $ ExchangeRot $ ExchangeSwap $ IntroduceProduct Identity $ EliminateImplication Identity Identity

Edit: This isn't actually complete. Exchange needs more combinators over the assumtion stack.