Skip to content

Instantly share code, notes, and snippets.

@clinuxrulz
Last active August 31, 2023 19:38
Show Gist options
  • Save clinuxrulz/e1ae4eb86a833afe582e3cd2e55e180a to your computer and use it in GitHub Desktop.
Save clinuxrulz/e1ae4eb86a833afe582e3cd2e55e180a to your computer and use it in GitHub Desktop.
Lambda Calculus to CCC in Purescript
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment