linear_something.hs

{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE DataKinds #-}

import GHC.Base (Multiplicity(Many))

data Bang a where
    Bang :: a %Many -> Bang a

data With a b where
    With :: u %1 -> (u %1 -> a) %Many -> (u %1 -> b) %Many -> With a b

data Par a b where
    ParInit :: a %Many -> b %Many -> Par a b
    ParStep :: Par x y %1 -> Par (x %1 -> a) (y %1 -> b) %1 -> Par a b

type a ⋅ b = (a, b)
type a & b = With a b
type a ⅋ b = Par a b
type a + b = Either a b

type Possibly a = a & ()

runPar :: a ⅋ b %1 -> a ⋅ b
runPar (ParInit a b) = (a, b)
runPar (ParStep gam step) =
    case runPar step of
        (f, g) -> case runPar gam of
            (x, y) -> (f x, g y)

wFst :: a & b %1 -> a
wFst (With u f _) = f u

wSnd :: a & b %1 -> b
wSnd (With u _ g) = g u

wBang :: Bang (a & b) -> Bang a ⋅ Bang b
wBang (Bang tup) = (Bang (wFst tup), Bang (wSnd tup))