One object kappa/zeta calculus, kind of like reflexive objects but also weird

onekappa.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
import Prelude hiding (id, (.))
import Control.Category
import Control.Monad.State hiding (lift)

class Category k => Terminal k where
  term :: k a ()

class Terminal k => Kappa k where
  -- | The higher order function here doesn't seem quite kosher at
  -- first except that we implicitly index over the category k so it's
  -- basically implicitly parametric higher order abstract
  -- syntax. Anyway this isn't formal or anything just exploring. It's
  -- Haskell not Agda.
  kappa :: (k () a -> k b c) -> k (a, b) c
  lift :: k () a -> k b (a, b)

class Terminal k => Zeta k where
  zeta :: (k () a -> k b c) -> k b (a -> c)
  pass :: k () a -> k (a -> b) b

newtype One m a b = One { one :: m }

instance Monoid m => Category (One m) where
  id = One mempty
  One f . One g = One (f <> g)
instance Nil u => Terminal (One u) where
  term = One nil
instance Lambda u => Zeta (One u) where
  zeta f = One (lam (one . f . One))
  pass (One x) = One (app x)
instance Stack u => Kappa (One u) where
  kappa f = One (pop (one . f . One))
  lift (One x) = One (push x)

instance Num u => Num (One u x Integer) where
  fromInteger n = One (fromInteger n)
  One x + One y = One (x + y)

class Monoid u => Nil u where
  nil :: u
class Nil u => Lambda u where
  lam :: (u -> u) -> u
  app :: u -> u
class Nil u => Stack u where
  pop :: (u -> u) -> u
  push :: u -> u

---

sample :: (forall x. Num (k x Integer), Kappa k) => k (Integer, (Integer, ())) Integer
sample =
  kappa $ \x ->
  kappa $ \y ->
  x + y

sampleDyn :: (forall x. Num u, Stack u) => u
sampleDyn = one sample

sampleResult :: Dyn
sampleResult = exec sampleDyn (Tuple (Z 1) (Tuple (Z 2) Nil))

sampleSource :: String
sampleSource = show (view sampleDyn)

---

view :: View -> View
view = id

newtype View = V (State Int String)
instance Show View where
  show (V x) = evalState x 0

instance Semigroup View where
  (<>) = mappend

instance Monoid View where
  mempty = V $ pure "{}"
  mappend (V f) (V g) = V $ pure (\f' g' -> "(" ++ f' ++ " ; " ++ g' ++ ")") <*> f <*> g

instance Nil View where
  nil = V $ pure "nil"

instance Lambda View where
  lam f = V $ do
    n <- get
    put (n + 1)
    let v = "v" ++ show n
    case f (V $ pure v) of
      V y -> pure (\y' -> "(lam " ++ v ++ ". " ++ y' ++ ")") <*> y
  app (V x) = V $ pure (\x' -> "(app " ++ x' ++ ")" ) <*> x

instance Stack View where
  pop f = V $ do
    n <- get
    put (n + 1)
    let v = "v" ++ show n
    case f (V $ pure v) of
      V y -> pure (\y' -> "(pop " ++ v ++ ". " ++ y' ++ ")") <*> y
  push (V x) = V $ pure (\x' -> "(push " ++ x' ++ ")" ) <*> x

instance Num View where
  fromInteger n = V $ pure (show n)
  V x + V y = V $ pure (\x' y' -> "(" ++ x' ++ " + " ++ y' ++ ")") <*> x <*> y

---

data Dyn = Z Integer | Fn (Dyn -> Dyn) | Tuple Dyn Dyn | Nil
data Prog = Prog { exec :: Dyn -> Dyn }

instance Show Dyn where
  show (Z n) = show n
  show (Tuple x y) = "<" ++ show x ++ ", " ++ show y ++ ">"
  show Nil = "()"
  show (Fn _) = "<fn>"
-- partial so not a real semantics or anything just exploring

instance Semigroup Prog where
  (<>) = mappend

instance Monoid Prog where
  mempty = Prog id
  mappend (Prog f) (Prog g) = Prog (f . g)

instance Nil Prog where
  nil = Prog $ \_ -> Nil
instance Lambda Prog where
  lam f = Prog $ \b -> Fn $ \a -> case f (Prog $ \_ -> a) of
    Prog g -> g b
  -- | warning, partial
  app (Prog x) = Prog $ \(Fn f) -> f (x Nil)
instance Stack Prog where
  -- | warning, partial
  pop f = Prog $ \(Tuple a b) -> case f (Prog $ \_ -> a) of
    Prog g -> g b
  push (Prog x) = Prog $ \y -> Tuple (x Nil) y

instance Num Prog where
  fromInteger n = Prog $ \_ -> Z n
  -- | warning, partial
  Prog x + Prog y = Prog $ \env -> case (x env, y env) of
    (Z x', Z y') -> Z (x' + y')