Tagless Final EDSL

{-# LANGUAGE NoMonomorphismRestriction #-}

class Symantics r where
  int  :: Int -> r Int
  bool :: Bool -> r Bool
  add  :: r Int -> r Int -> r Int
  mul  :: r Int -> r Int -> r Int
  leq  :: r Int -> r Int -> r Bool
  if_  :: r Bool -> r a -> r a -> r a
  app  :: r (a -> b) -> r a -> r b
  lam  :: (r a -> r b) -> r (a -> b)
  fix  :: (r a -> r a) -> r a

newtype MetaValue a = M { result :: a }

instance Symantics MetaValue where
  int  i          = M i
  bool b          = M b
  add (M a) (M b) = M (a + b)
  mul (M a) (M b) = M (a * b)
  leq (M a) (M b) = M (a <= b)
  if_ (M p) a b   = if p then a else b
  app (M f) (M a) = M (f a)
  lam f           = M (\x -> let M b = f (M x) in b)
  fix f           = f (fix f)

newtype Length a = L { lresult :: Int }

instance Symantics Length where
  int  i                = L 1
  bool b                = L 1
  add (L a) (L b)       = L (a + b + 1)
  mul (L a) (L b)       = L (a + b + 1)
  leq (L a) (L b)       = L (a + b + 1)
  if_ (L p) (L a) (L b) = L (p + a + b + 1)
  app (L f) (L a)       = L (f + a + 1)
  lam f                 = L (let L a = f (L 0) in a + 1)
  fix f                 = L (let L a = f (L 0) in a + 1)

newtype PrettyPrint a = P { presult :: String }

instance Symantics PrettyPrint where
  int  i                = P (show i)
  bool b                = P (show b)
  add (P a) (P b)       = P ("(+ " ++ a ++ " " ++ b ++ ")")
  mul (P a) (P b)       = P ("(* " ++ a ++ " " ++ b ++ ")")
  leq (P a) (P b)       = P ("(<= " ++ a ++ " " ++ b ++ ")")
  if_ (P p) (P a) (P b) = P ("(if " ++ p ++ " " ++ a ++ " " ++ b ++ ")")
  app (P f) (P a)       = P ("(" ++ f ++ " " ++ a ++ ")")
  lam f                 = P (let P a = f (P "x") in "(fn [x] " ++ a ++ ")")
  fix f                 = P (let P a = f (fix f) in a)

main = do
  let program = app (lam (\x -> if_ x (int 1) (int 2))) (bool True)
  print $ result  program
  print $ lresult program
  print $ presult program