Funny stacks

Stack.hs

{-#
LANGUAGE
  GHC2021, BlockArguments, DataKinds, TypeFamilies, RequiredTypeArguments
#-}

module Stack (
  Stack, run,
  push, dup, rot,
  apply, plus, minus, times,
) where

-- base
import Prelude hiding (id, (.))
import Data.Kind (Type)
import Control.Category (Category(..), (>>>))

type Fun :: [Type] -> Type -> Type
type family Fun xs y where
  Fun '[    ] y = y
  Fun  (x:xs) y = x -> Fun xs y


-- | An operation on a stack of @xs@, concluding with a stack of @ys@.
newtype Stack xs ys = MkStack (forall s -> Fun ys s -> Fun xs s)

instance Category Stack where
  id = MkStack \_ x -> x
  MkStack f . MkStack g = MkStack \s x -> g s (f s x)

run :: forall a. Stack '[] '[a] -> a
run (MkStack f) = f a id

push :: x -> Stack xs (x:xs)
push x = MkStack \_ f -> f x

dup :: Stack (x:xs) (x:x:xs)
dup = MkStack \_ f x -> f x x

rot :: Stack (w:x:y:zs) (y:w:x:zs)
rot = MkStack \_ f w x y -> f y w x

apply :: Stack ((x -> y):x:zs) (y:zs)
apply = MkStack \_ f g x -> f (g x)

binop :: (x -> y -> z) -> Stack (x:y:zs) (z:zs)
binop f = push f >>> apply >>> apply

plus, minus, times :: Num x => Stack (x:x:xs) (x:xs)
plus  = binop (+)
minus = binop (-)
times = binop (*)


_test :: Int
_test = run (push 1 >>> push 2 >>> plus >>> push 3 >>> times)

-- $> _test