Lambda Calculus to CCC in Purescript

Main.purs

module Main where

import Prelude (Unit, ($), (+), (<>), (<$>), (<*>), (==), (>), discard)
import Effect (Effect)
import Effect.Console (log)
import Control.Category
import Control.Semigroupoid
import Data.Leibniz
import Data.Maybe
import Data.Exists
import Data.Show
import Data.Tuple (Tuple(..))
import Unsafe.Coerce

class Category k <= Cartesian (k :: Type -> Type -> Type) (tensor :: (Type -> Type -> Type) -> Type -> Type -> Type) where
  -- | product introduction and elimination terms
  fork :: forall a c d. k a c -> k a d -> k a (tensor k c d)
  exl :: forall a b. k (tensor k a b) a
  exr :: forall a b. k (tensor k a b) b

-- | A Cartesian-closed category is a Category k, together with...
class Cartesian k tensor <= CCC (k :: Type -> Type -> Type) (tensor :: (Type -> Type -> Type) -> Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) where
  -- | evaluation morphisms,
  eval :: forall a b. k (tensor k (hom k a b) a) b
  -- | currying and uncurring operations,
  curry :: forall a b c. k (tensor k a b) c -> k a (hom k b c)
  uncurry :: forall a b c. k a (hom k b c) -> k (tensor k a b) c

data LC (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) a
  = LCLam (Lam k hom a)
  | LCAp (Ap k hom a)
  | LCLift (Lift k hom a)
  | LCVar Int -- ^ Internal use only (for inspecting the code held inside the lambda in Lam)

-- LCD: Pure data representation of LC
data LCD (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) a
  = LCDLam (LamD k hom a)
  | LCDAp (ApD k hom a)
  | LCDLift (Lift k hom a)
  | LCDVar Int

data Lam (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c = Lam (Exists (LamF k hom c))

data LamF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c a = LamF (Exists (LamFF k hom c a))

data LamFF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c a b = LamFF (LC k hom a -> LC k hom b) (c ~ hom k a b)

data LamD (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c = LamD (Exists (LamDF k hom c))

data LamDF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c a = LamDF (Exists (LamDFF k hom c a))

data LamDFF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c a b = LamDFF Int (LCD k hom b) (c ~ hom k a b)

data Ap (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) b = Ap (Exists (ApF k hom b))

data ApF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) b a = ApF (LC k hom (hom k a b)) (LC k hom a)

data ApD (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) b = ApD (Exists (ApDF k hom b))

data ApDF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) b a = ApDF (LCD k hom (hom k a b)) (LCD k hom a)

data Lift (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c = Lift (Exists (LiftF k hom c))

data LiftF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c a = LiftF (Exists (LiftFF k hom c a))

data LiftFF (k :: Type -> Type -> Type) (hom :: (Type -> Type -> Type) -> Type -> Type -> Type) c a b = LiftFF (k a b) (c ~ hom k a b)

to_lcd :: forall k hom a. LC k hom a -> LCD k hom a
to_lcd lc = let Tuple x _ = to_lcd' lc 0 in x

to_lcd' :: forall k hom a. LC k hom a -> Int -> Tuple (LCD k hom a) Int

to_lcd' (LCLam (Lam x)) v0 =
  runExists go1 x
  where
    go1 :: forall b. LamF k hom a b -> Tuple (LCD k hom a) Int
    go1 (LamF y) = runExists go2 y
    go2 :: forall b c. LamFF k hom a b c -> Tuple (LCD k hom a) Int
    go2 (LamFF f leibniz) =
      let param = v0
          v1 = v0 + 1
          (Tuple body v2) = to_lcd' (f (LCVar param)) v1
      in
      Tuple (runLeibniz (symm leibniz) $ LCDLam (LamD $ mkExists $ LamDF $ mkExists $ LamDFF param body identity)) v2

to_lcd' (LCAp (Ap x)) v0 =
  runExists
    (\(ApF y z) ->
      let Tuple f v1 = to_lcd' y v0
          Tuple a v2 = to_lcd' z v1
      in
      Tuple (LCDAp (ApD $ mkExists (ApDF f a))) v2
    )
    x

to_lcd' (LCLift x) v0 = Tuple (LCDLift x) v0

to_lcd' (LCVar x) v0 = Tuple (LCDVar x) v0

lcd_subst :: forall k hom b. (forall a. (LCD k hom a -> LCD k hom a)) -> LCD k hom b -> LCD k hom b

lcd_subst f (LCDLam (LamD x)) =
  f $ runExists
    (\(LamDF y) ->
      runExists
        (\(LamDFF param body leibniz) ->
          LCDLam $ LamD $ mkExists $ LamDF $ mkExists $ LamDFF param (f body) leibniz
        )
        y
    )
    x

lcd_subst f (LCDAp (ApD x)) =
  f $ runExists
    (\(ApDF f2 a) ->
      LCDAp (ApD $ mkExists (ApDF (lcd_subst f f2) (lcd_subst f a)))
    )
    x

lcd_subst f this = f this

-- | An untyped representation of terms in a CCC formed from the above.
-- This is useful if we want to print out terms for debugging.
data Untyped
  = Eval
  | Curry Untyped
  | Uncurry Untyped
  | Fork Untyped Untyped
  | Exl
  | Exr
  | Id
  | Compose Untyped Untyped

-- | A 'CCC' instance for our untyped terms.
data KDebug a b = KDebug Untyped

instance semigroupoidKDebug :: Semigroupoid KDebug where
  compose (KDebug f) (KDebug g) = KDebug (Compose f g)

instance categoryKDebug :: Category KDebug where
  identity = KDebug Id

instance cartesianKDebug :: Cartesian KDebug tensor where
  fork (KDebug f) (KDebug g) = KDebug (Fork f g)
  exl = KDebug Exl
  exr = KDebug Exr

instance cccKDebug :: CCC KDebug tensor hom where
  eval = KDebug Eval
  curry (KDebug f) = KDebug (Curry f)
  uncurry (KDebug f) = KDebug (Uncurry f)

class Show3 k where
  show3 :: forall a b. k a b -> String

instance show3KDebug :: Show3 KDebug where
  show3 a = prettyPrint a

instance showKDebug :: Show (KDebug a b) where
  show a = prettyPrint a

-- | A simple 'showsPrec' style pretty printer for terms.
prettyPrint :: forall a b. KDebug a b -> String
prettyPrint (KDebug u) = go 0 u where
  go _ Exl             = "fst"
  go _ Exr             = "snd"
  go _ Id              = "id"
  go d Eval            = "uncurry id"
  go d (Curry e)       = parensIf (d > 10) ("curry " <> go 11 e)
  go d (Uncurry e)     = parensIf (d > 10) ("uncurry " <> go 11 e)
  go d (Fork e1 e2)    = parensIf (d > 3)  (go 4  e1 <> " &&& " <> go 3 e2)
  go d (Compose e1 e2) = parensIf (d > 9)  (go 10 e1 <> " . "   <> go 9 e2)

  parensIf true s = "(" <> s <> ")"
  parensIf _    s = s

lcd_to_str :: forall k hom a. (Show3 k) => LCD k hom a -> String

lcd_to_str (LCDLam (LamD x)) =
  runExists
    (\(LamDF y) ->
      runExists
        (\(LamDFF param body leibniz) ->
          "(\\v" <> (show param) <> " -> " <> (lcd_to_str body) <> ")"
        )
        y
    )
    x

lcd_to_str (LCDAp (ApD x)) =
  runExists
    (\(ApDF f a) ->
      "(" <> (lcd_to_str f) <> " " <> (lcd_to_str a) <> ")"
    )
    x

lcd_to_str (LCDLift (Lift x)) =
  runExists
    (\(LiftF y) ->
      runExists
        (\(LiftFF k leibniz) ->
          show3 k
        )
        y
    )
    x

lcd_to_str (LCDVar v) = "v" <> (show v)

instance showLCD :: Show3 k => Show (LCD k hom a) where
  show = lcd_to_str

instance showLC :: Show3 k => Show (LC k hom a) where
  show lc = show $ to_lcd lc

data TensorPhantom (a :: (Type -> Type -> Type) -> Type -> Type -> Type) = TensorPhantom

lcd_lift :: forall k tensor hom a b. CCC k tensor hom => TensorPhantom tensor -> k a b -> LCD k hom (hom k a b)
lcd_lift _ k = LCDLift $ Lift $ mkExists $ LiftF $ mkExists $ LiftFF k identity

lcd_fst :: forall k tensor hom a b. CCC k tensor hom => TensorPhantom tensor -> LCD k hom (hom k a (hom k b a))
lcd_fst tensorPhantom =
  let x1 = exl :: k (tensor k a b) a
  in
  lcd_lift tensorPhantom (curry x1)

lcd_snd :: forall k tensor hom a b. CCC k tensor hom => TensorPhantom tensor -> LCD k hom (hom k a (hom k b b))
lcd_snd tensorPhantom =
  let x1 = exr :: k (tensor k a b) b
  in
  lcd_lift tensorPhantom (curry x1)

lcd_to_ccc :: forall k tensor hom a b. CCC k tensor hom => LCD k hom (hom k a b) -> Maybe (k a b)
lcd_to_ccc = lcd_to_ccc' (TensorPhantom :: TensorPhantom tensor)

lcd_to_ccc' :: forall k tensor hom a b. CCC k tensor hom => TensorPhantom tensor -> LCD k hom (hom k a b) -> Maybe (k a b)

lcd_to_ccc' _ (LCDLam (LamD x)) =
  runExists go1 x
  where
    go1 :: forall c. LamDF k hom (hom k a b) c -> Maybe (k a b)
    go1 (LamDF y) = runExists go2 y

    go2 :: forall c d. LamDFF k hom (hom k a b) c d -> Maybe (k a b)
    go2 (LamDFF param (body :: LCD k hom d) (leibniz :: hom k a b ~ hom k c d)) =
      let leibniz2 = lowerLeibniz leibniz :: b ~ d
          leibniz3 = lowerLeibniz1of2 leibniz :: a ~ c
          leibniz4 = liftLeibniz2of2 leibniz2 :: k c b ~ k c d
          leibniz5 = liftLeibniz1of2 leibniz3 :: k a b ~ k c b
          x1 = go3 param body :: Maybe (k c d)
          x2 = (coerceSymm leibniz4 <$> x1) :: Maybe (k c b)
          x3 = (coerceSymm leibniz5 <$> x2) :: Maybe (k a b)
      in
      x3

    go3 :: forall c d. Int -> LCD k hom d -> Maybe (k c d)

    go3 param (LCDLam (LamD x)) =
      runExists (\(LamDF y) -> runExists go3_1 y) x
      where
        go3_1 :: forall e f. LamDFF k hom d e f -> Maybe (k c d)
        go3_1 (LamDFF param2 body leibniz) =
          let body2 = lcd_subst go3_2 body
              newLam = LCDLam $ LamD $ mkExists $ LamDF $ mkExists $ LamDFF param body2 identity
              x1 = lcd_to_ccc' (TensorPhantom :: TensorPhantom tensor) newLam
          in
          unsafeCoerce x1
          where
            go3_2 :: forall e. LCD k hom e -> LCD k hom e
            go3_2 this@(LCDVar ident) =
              if ident == param then
                let fst' = (lcd_fst (TensorPhantom :: TensorPhantom tensor)) :: LCD k hom (hom k _ (hom k _ _))
                in
                (unsafeCoerce $ LCDAp $ ApD $ mkExists $ ApDF fst' (LCDVar param)) :: LCD k hom e
              else if ident == param2 then
                let snd' = (lcd_snd (TensorPhantom :: TensorPhantom tensor)) :: LCD k hom (hom k _ (hom k _ _))
                in
                (unsafeCoerce $ LCDAp $ ApD $ mkExists $ ApDF snd' (LCDVar param)) :: LCD k hom e
              else
                this

            go3_2 this = this

    go3 param (LCDAp (ApD x)) =
      runExists go3_1 x
      where
        go3_1 :: forall e. ApDF k hom d e -> Maybe (k c d)
        go3_1 (ApDF f a) =
          let lcdf = (LCDLam $ LamD $ mkExists $ LamDF $ mkExists $ LamDFF param f identity) :: LCD k hom (hom k c (hom k e d))
              lcda = (LCDLam $ LamD $ mkExists $ LamDF $ mkExists $ LamDFF param a identity) :: LCD k hom (hom k c e)
              f2 = (lcd_to_ccc' (TensorPhantom :: TensorPhantom tensor) lcdf) :: Maybe (k c (hom k e d))
              a2 = (lcd_to_ccc' (TensorPhantom :: TensorPhantom tensor) lcda) :: Maybe (k c e)
              x1 = (fork <$> f2 <*> a2) :: Maybe (k c (tensor k (hom k e d) e))
              x2 = ((eval <<< _) <$> x1) :: Maybe (k c d)
          in
          x2

    go3 param (LCDLift (Lift x)) =
      runExists
        (\(LiftF y) ->
          runExists
            go3_1
            y
        )
        x
      where
        go3_1 :: forall e f. LiftFF k hom d e f -> Maybe (k c d)
        go3_1 (LiftFF (k :: k e f) (leibniz :: d ~ hom k e f)) =
          let x1 = exr :: k (tensor k c e) e
              x2 = (k <<< exr) :: k (tensor k c e) f
              x3 = curry x2 :: k c (hom k e f)
              leibniz2 = liftLeibniz leibniz :: k c d ~ k c (hom k e f)
              x4 = coerceSymm leibniz2 x3
          in
          Just x4

    go3 param (LCDVar ident) =
      if param == ident then
        let k = identity :: k d d
        in
        (Just $ ((unsafeCoerce k) :: k c d))
      else
        Nothing
    go3 param _ = Nothing

lcd_to_ccc' _ (LCDLift (Lift x)) =
  runExists go1 x
  where
    go1 :: forall c. LiftF k hom (hom k a b) c -> Maybe (k a b)
    go1 (LiftF y) = runExists go2 y
    go2 :: forall c d. LiftFF k hom (hom k a b) c d -> Maybe (k a b)
    go2 (LiftFF (k :: k c d) (leibniz :: hom k a b ~ hom k c d)) =
      let leibniz2 = (lowerLeibniz leibniz) :: b ~ d
          leibniz3 = (lowerLeibniz1of2 leibniz) :: a ~ c
          leibniz4 = (liftLeibniz1of2 leibniz3) :: k a d ~ k c d
          leibniz5 = (liftLeibniz2of2 leibniz2) :: k a b ~ k a d
          k2 = (coerceSymm leibniz4 k) :: k a d
          k3 = (coerceSymm leibniz5 k2) :: k a b
      in
      Just k3

lcd_to_ccc' _ _ = Nothing

lam_to_ccc :: forall k tensor hom a b. CCC k tensor hom => Int -> LCD k hom b -> Maybe (k a b)
lam_to_ccc param body = unsafeCoerce 0

lc_to_ccc :: forall k tensor hom a b. CCC k tensor hom => LC k hom (hom k a b) -> Maybe (k a b)
lc_to_ccc lc = lcd_to_ccc' (TensorPhantom :: TensorPhantom tensor) $ to_lcd lc

lam :: forall k hom a b. (LC k hom a -> LC k hom b) -> LC k hom (hom k a b)
lam f = LCLam (Lam (mkExists (LamF (mkExists (LamFF f identity)))))

ap :: forall k hom a b. LC k hom (hom k a b) -> LC k hom a -> LC k hom b
ap f a = LCAp (Ap (mkExists (ApF f a)))

mkTest :: forall hom a b. LC KDebug hom (hom KDebug a b) -> String
mkTest lc = maybe "" show ((lc_to_ccc lc) :: Maybe (KDebug _ _))

test1 :: String
test1 = mkTest $ lam (\x -> x)
-- > id

test2 :: String
test2 = mkTest $ lam (\x -> lam (\y -> x))
-- > uncurry id . (curry (curry fst . snd) &&& id)

main :: Effect Unit
main = do
  log test1
  log test2