Implementing linear logic (double negation, ...) in linear haskell using linear-base

LinearLogic.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- Quick demonstration that linear-base is enough to implement linear logic

import Data.Array.Destination
import Data.Array.Polarized.Pull
import Prelude.Linear hiding (fst, snd)

data Iso a b = Iso
  { to :: a %1 -> b,
    from :: b %1 -> a
  }

-- This is the linear negation
-- It represents a "a slot for an a", "an obligation to provide an a"
-- or "a way to get rid of an a"
type Not a = a %1 -> ()

-- Double negation can be interpreted as:
-- The only way to get rid of an "a-slot" is to provide an a
double :: Iso a (Not (Not a))
double = Iso to_double from_double
  where
    to_double :: a %1 -> Not (Not a)
    to_double x = ($ x)
    -- This is the most important part!
    -- Works because alloc is already most of the way there
    -- alloc 1 ::  (DArray a -> ()) -> Vector a
    --         ::  (Not (Darray a))     -> Vector a
    --        "::" Not (Not a) -> a
    --         (last line needs some massaging of types)
    from_double :: Not (Not a) %1 -> a
    from_double nnx = case asList $ fromVector $ alloc 1 $ \darr -> nnx (`fill` darr) of
      [y] -> y

-- Negation is a contravariant equivalence of categories
notFn :: Iso (a %1 -> b) (Not b %1 -> Not a)
notFn = Iso to_notFn from_notFn
  where
    to_notFn :: (a %1 -> b) %1 -> Not b %1 -> Not a
    to_notFn f nb = nb . f
    from_notFn :: (Not b %1 -> Not a) %1 -> a %1 -> b
    from_notFn nf a = double.from (to_notFn nf (double.to a))

notIso :: Iso (Iso a b) (Iso (Not a) (Not b))
notIso = Iso to_notIso from_notIso
  where
    to_notIso :: Iso a b %1 -> Iso (Not a) (Not b)
    to_notIso Iso {to = t, from = f} = Iso (notFn.to f) (notFn.to t)
    from_notIso :: Iso (Not a) (Not b) %1 -> Iso a b
    from_notIso Iso {to = t, from = f} = Iso (notFn.from f) (notFn.from t)

-- Literally called the iso-mix rule in linear logic
isoMix :: Iso () (Not ())
isoMix = Iso to_Not from_Not
  where
    to_Not :: () %1 -> Not ()
    to_Not () () = ()
    from_Not :: Not () %1 -> ()
    from_Not f = f ()


-- Double negation makes it possible to define Par!
-- I'm not sure If there is a good way to "visualize" Par a b.
-- I imagine it as a pair (a, b), but you're not allowed to use
-- information from the lhs to modify the rhs and vice versa.
-- For example 'Par (Not a) b' will be the same as 'a -> b'.
-- If you use the 'b' to modify the 'Not a' you'd use the output
-- of a function to modify the input, which shouldn't be possible.
-- In other words the a and b in 'Par a b' have to be consumed in *par*allel.
newtype Par a b = Par (Not (Not a, Not b))

-- Same as (a, b) -> Par a b, so it's the mix rule
-- With the above interpretation this means that if I have a pair (a, b)
-- I can just "ban" you from transferring information between them
toPar :: a -> b -> Par a b
toPar x y = Par \(nx, ny) -> nx x <> ny y

-- The par - function iso I mentioned earlier
fnPar :: Iso (a %1 -> b) (Par (Not a) b)
fnPar = Iso to_Par from_Par
  where
    to_Par :: (a %1 -> b) %1 -> Par (Not a) b
    to_Par f = Par \(x, ny) -> ny $ f $ double.from x

    from_Par :: Par (Not a) b %1 -> (a %1 -> b)
    from_Par (Par p) x = double.from (\ny -> p (($ x), ny))

-- These two are the "linear distribution" functions
-- (Making (LinHask, (,), Par) a linearly distributive category)
pairFst :: a %1 -> Par b c %1 -> Par (a, b) c
pairFst a (Par p) = Par \(nab, nc) -> p (\b -> nab (a, b), nc)

pairSnd :: Par a b %1 -> c %1 -> Par a (b, c)
pairSnd (Par p) c = Par \(na, nbc) -> p (na, \b -> nbc (b, c))


-- This is the product in LinHask ((,) is the monoidal product)
-- Can this be defined without using double negation?
newtype Choose a b = Choose (Not (Either (Not a) (Not b)))
-- Choose is a bit weird, you can imagine it as kind of like Either
-- but the consumer chooses which case it is, instead of the producer
-- Because it's the product, some functions on (,) in usual haskell
-- translate to Choose in LinHask

-- The consumer chooses the first one
fst :: Choose a b %1 -> a
fst (Choose nab) = double.from (nab . Left)

-- The consumer chooses the second one
snd :: Choose a b %1 -> b
snd (Choose nab) = double.from (nab . Right)

-- When interpreting Ur as ! (bang), this is the conjunctive exponential rule from linear logic.
-- Means: If I can choose arbitrarily often between a and b
--        then I can produce an arbitrary amount of both a's and b's
-- (and also in reverse)
conjunctiveExp :: Iso (Ur (Choose a b)) (Ur a, Ur b)
conjunctiveExp = Iso to_h from_h
  where
    to_h :: Ur (Choose a b) %1 -> (Ur a, Ur b)
    to_h (Ur x) = (Ur (fst x), Ur (snd x))
    from_h :: (Ur a, Ur b) %1 -> Ur (Choose a b)
    from_h (Ur x, Ur y) =
      Ur
        ( Choose \case
            (Left nx) -> nx x
            (Right ny) -> ny y
        )

-- This is ?, also called "why not". I don't know if it has a better name.
-- Can be interpreted as a "pile of a's" that you have to deal with (in parallel)
newtype Some a = Some (Not (Ur (Not a)))

-- disjunctive exponential rule
-- Means: Having a pile of things which are either a's or b's   (that have to be consumed in parallel)
--        is the same as having a pile of a's and a pile of b's (which have to be consumed in paralle)
disjunctiveExp :: Iso (Some (Either a b)) (Par (Some a) (Some b))
disjunctiveExp = Iso to_h from_h
  where
    to_h :: Some (Either a b) %1 -> Par (Some a) (Some b)
    to_h (Some nun_ab) = Par \(ns_a, ns_b) ->
      case (double.from (ns_a . Some), double.from (ns_b . Some)) of
        (Ur na, Ur nb) -> nun_ab (Ur \ab -> either na nb ab)
    from_h :: Par (Some a) (Some b) %1 -> Some (Either a b)
    from_h (Par p) = Some \(Ur n_ab) ->
      p
        ( \(Some nun_a) -> nun_a $ Ur (n_ab . Left),
          \(Some nun_b) -> nun_b $ Ur (n_ab . Right)
        )