Denotational Design of a Stack API

StackDD.hs

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}

module DD where

newtype Stack a = S (Int -> a)

empty :: Stack a
empty = S (\case {})

push :: a -> Stack a -> Stack a
push a (S f) = S (\n -> if n == 1 then a else f (n + 1))

pop :: Stack a -> (a, Stack a)
pop (S f) = (f 1, S (\n -> f (n - 1)))

instance Functor Stack where
  fmap f (S s) = S (fmap f s)

instance Applicative Stack where
  pure a = S (pure a)
  (S sf) <*> (S sa) = S (sf <*> sa)

instance Monad Stack where
  return = pure
  (S u) >>= k = let f (S x) = x
    in S (u >>= f . k)

prog :: Num a => Stack a
prog = do
  let i = pure 1
  s <- push 1 i
  push (s + 5) i

class IsStack s where
  mu :: s a -> Stack a
  mu' :: Stack a -> s a

instance IsStack [] where
  mu [] = empty
  mu (h:t) = push h (mu t)

  mu' (S f) = aux f 1
    where
      aux f n = f n : aux f (n + 1)