SelfLC.hs

{-# LANGUAGE RankNTypes, GADTs #-}

import Data.Void

newtype Maybe' a = Maybe { unMaybe :: forall r. r -> (a -> r) -> r }

v0 :: LC (Maybe' a)
v0 = var nothing
v1 :: LC (Maybe' (Maybe' a))
v1 = var $ just nothing
v2 :: LC (Maybe' (Maybe' (Maybe' a)))
v2 = var $ just $ just nothing
v3 :: LC (Maybe' (Maybe' (Maybe' (Maybe' a))))
v3 = var $ just $ just $ just nothing
v4 :: LC (Maybe' (Maybe' (Maybe' (Maybe' (Maybe' a)))))
v4 = var $ just $ just $ just $ just nothing

nothing :: Maybe' a
nothing = Maybe $ \nothing just -> nothing

nothing' :: LC a
nothing' = lam $ lam v1

just :: a -> Maybe' a
just x = Maybe $ \nothing just -> just x

just' :: LC a
just' = lam $ lam $ lam $ v0 `app` v2

newtype LC a = LC { unLC :: forall p. (forall a. a -> p a) -> (forall a. p a -> p a -> p a) -> (forall a. p (Maybe' a) -> p a) -> p a }

var :: a -> LC a
var v = LC $ \var app lam -> var v

var' :: LC a
var' = lam $ lam $ lam $ lam $ v2 `app` v3

app :: LC a -> LC a -> LC a
app f x = LC $ \var app lam -> app (unLC f var app lam) (unLC x var app lam)

app' :: LC a
app' = lam $ lam $ lam $ lam $ lam $ v1 `app` (v4 `app` v2 `app` v1 `app` v0) `app` (v3 `app` v2 `app` v1 `app` v0)

lam :: LC (Maybe' a) -> LC a
lam b = LC $ \var app lam -> lam (unLC b var app lam)

lam' :: LC a
lam' = lam $ lam $ lam $ lam $ v0 `app` (v3 `app` v2 `app` v1 `app` v0)

newtype K a = K { unK :: forall b. (a -> b) -> LC b }

lmap :: (a -> b) -> LC a -> LC b
lmap w x = unK (unLC x lmapVar lmapApp lmapLam) w
  where
    lmapVar v = K $ \w -> var $ w v
    lmapApp f x = K $ \w -> app (unK f w) (unK x w)
    lmapLam b = K $ \w -> lam (unK b $ \v -> unMaybe v nothing (\v -> just $ w v))

lmap' :: LC a
lmap' = lam $ lam $ v0 `app` lmapVar' `app` lmapApp' `app` lmapLam' `app` v1
  where
    lmapVar' = lam $ lam $ var' `app` (v0 `app` v1)
    lmapApp' = lam $ lam $ lam $ app' `app` (v2 `app` v0) `app` (v1 `app` v0)
    lmapLam' = lam $ lam $ lam' `app` (v1 `app` (lam $ v0 `app` nothing' `app` (lam $ just' `app` (v2 `app` v0))))

newtype M a = M { unM :: forall b. (a -> LC b) -> LC b }
newtype F a = F { unF :: LC a }

bind :: (a -> LC b) -> LC a -> LC b
bind w x = unM (unLC x bindVar bindApp bindLam) w
  where
    bindVar v = M $ \w -> w v
    bindApp f x = M $ \w -> app (unM f w) (unM x w)
    bindLam b = M $ \w -> lam (unM b (\m -> unF $ unMaybe m (F $ var nothing) (\l -> F $ lmap just (w l))))

bind' :: LC a
bind' = lam $ lam $ v0 `app` bindVar' `app` bindApp' `app` bindLam' `app` v1
  where
    bindVar' = lam $ lam $ v0 `app` v1
    bindApp' = lam $ lam $ lam $ app' `app` (v2 `app` v0) `app` (v1 `app` v0)
    bindLam' = lam $ lam $ lam' `app` (v1 `app` (lam $ v0 `app` (var' `app` nothing') `app` (lam $ lmap' `app` just' `app` (v2 `app` v0))))

newtype L a = L { unL :: L a -> a }

y :: (a -> a) -> a
y f = (\x -> f (unL x x)) (L $ \x -> f (unL x x))

y' :: LC a
y' = lam $ (lam $ v1 `app` (v0 `app` v0)) `app` (lam $ v1 `app` (v0 `app` v0))

newtype J a = J { unJ :: forall r. (a -> r) -> (LC a ->  LC a -> r) -> (LC (Maybe' a) -> r) -> r }

match :: LC a -> (a -> r) -> (LC a -> LC a -> r) -> (LC (Maybe' a) -> r) -> r
match t = unJ $ unLC t matchVar matchApp matchLam
  where
    matchVar v = J $ \var' _ _ -> var' v
    matchApp f x = J $ \_ app' _ -> app' (unJ f var app lam) (unJ x var app lam)
    matchLam b = J $ \_ _ lam' -> lam' (unJ b var app lam)

match' :: LC a
match' = lam $ v0 `app` matchVar' `app` matchApp' `app` matchLam'
  where
    matchVar' = lam $ lam $ lam $ lam $ v2 `app` v3
    matchApp' = lam $ lam $ lam $ lam $ lam $ v1 `app` (v4 `app` var' `app` app' `app` lam') `app` (v3 `app` var' `app` app' `app` lam')
    matchLam' = lam $ lam $ lam $ lam $ v0 `app` (v3 `app` var' `app` app' `app` lam')

newtype H = H { unH :: forall a. LC a -> LC a }

whnf :: LC a -> LC a
whnf = unH $ y $ \whnf' -> H $ \t -> match t var (\f x -> match (unH whnf' f) (\v -> var v `app` x) (\g y -> g `app` y `app` x) (\b -> unH whnf' $ bind (\m -> unMaybe m x var) b)) lam

whnf' :: LC a
whnf' = y' `app` (lam $ lam $ match' `app` v0 `app` var' `app` (lam $ lam $ match' `app` (v3 `app` v1) `app` (lam $ app' `app` (var' `app` v0) `app` v1) `app` (lam $ lam $ app' `app` (app' `app` v1 `app` v0) `app` v2) `app` (lam $ v4 `app` (bind' `app` (lam $ v0 `app` v2 `app` var') `app` v0))) `app` lam')

i :: LC a
i = lam $ var nothing
k :: LC a
k = lam $ lam $ var $ just nothing
s :: LC a
s = lam $ lam $ lam $ app (app (var $ just $ just nothing) (var nothing)) (app (var $ just nothing) (var nothing))

i' :: LC a
i' = lam' `app` (var' `app` nothing')
k' :: LC a
k' = lam' `app` (lam' `app` (var' `app` (just' `app` nothing')))
s' :: LC a
s' = lam' `app` (lam' `app` (lam' `app` (app' `app` (app' `app` (var' `app` (just' `app` (just' `app` nothing'))) `app` (var' `app` nothing')) `app` (app' `app` (var' `app` (just' `app` nothing')) `app` (var' `app` nothing')))))

newtype R b a = R { unR :: (a -> LC b) -> LC b }

reflectWith :: (a -> LC b) -> LC a -> LC b
reflectWith w t = unR (unLC t reflectVar reflectApp reflectLam) w
  where
    reflectVar v = R $ \w -> var' `app` w v
    reflectApp f x = R $ \w -> app' `app` unR f w `app` unR x w
    reflectLam b = R $ \w -> lam' `app` unR b (\m -> unMaybe m nothing' (\v -> just' `app` w v))

reflect :: LC Void -> LC a
reflect = reflectWith absurd

data LCTag = VarTag | AppTag | LamTag deriving Show
data VarTag = NothingTag | JustTag deriving Show

reify :: Show a => LC a -> LC Void
reify t = reifyTree (\v -> error $ "reify var: " <> printTerm v)
  (lmap Right t `app` var (Left VarTag) `app` var (Left AppTag) `app` var (Left LamTag))
  where
    reifyTree :: Show a => (LC (Either VarTag (Either LCTag a)) -> b) -> LC (Either LCTag a) -> LC b
    reifyTree w t = match (whnf t)
      (\v -> error $ "reify: " <> printTerm (var v))
      (\f x -> match (whnf f)
        (\v -> case v of
          Left VarTag -> var $ w $ lmap Right x
          Left LamTag -> lam $ reifyTree (reifyVar w) x
          _ -> error $ "reify: " <> printTerm (app (var v) x))
        (\g y -> match (whnf g)
          (\v -> case v of
            Left AppTag -> app (reifyTree w y) (reifyTree w x)
            _ -> error $ "reify: " <> printTerm (app (app (var v) y) x))
          (\h z -> error $ "reify: " <> printTerm (app (app (app h z) y) x))
          (\b -> error $ "reify: " <> printTerm (app (app (lam b) y) x)))
        (\b -> error $ "reify: " <> printTerm (app (lam b) x)))
      (\b -> error $ "reify: " <> printTerm (lam b))
    reifyVar :: Show a => (LC (Either VarTag (Either LCTag a)) -> b) -> LC (Either VarTag (Either LCTag a)) -> Maybe' b
    reifyVar w t = match (whnf $ t `app` var (Left NothingTag) `app` var (Left JustTag))
      (\v -> case v of
        Left NothingTag -> nothing
        _ -> error $ "reify var: " <> printTerm (var v))
      (\f x -> match (whnf f)
        (\v -> case v of
          Left JustTag -> just $ w x
          _ -> error $ "reify var: " <> printTerm (app (var v) x))
        (\g y -> error $ "reify var: " <> printTerm (app (app g y) x))
        (\b -> error $ "reify var: " <> printTerm (app (lam b) x)))
      (\b -> error $ "reify var: " <> printTerm (lam b))

newtype P a = P { unP :: (Int -> a -> ShowS) -> Int -> Int -> ShowS }

printTerm :: Show a => LC a -> String
printTerm t = unP (unLC t (\v -> P $ \p _ d -> p d v) (\f x -> P $ \p n d -> showParen (d > 9) $ unP f p n 9 . showString " " . unP x p n 10) (\b -> P $ \p n d -> showParen (d > 0) $ showString "\\" . shows n . showString ". " . unP b (\d m -> unMaybe m (shows n) (p d)) (n + 1) 0)) showsPrec 0 0 ""

instance Show a => Show (LC a) where
  show = printTerm