Type level DSL

TDSL.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module TDSL where

-- Our DSL
data Zero
data Succ a
data Add a b
data Mul a b

-- One way to interpret it, ie. evaluate
class Eval x where
  eval :: Int

instance Eval Zero where
  eval = 0

instance Eval a => Eval (Succ a) where
  eval = 1 + eval @a

instance (Eval a, Eval b) => Eval (Add a b) where
  eval = eval @a + eval @b

instance (Eval a, Eval b) => Eval (Mul a b) where
  eval = eval @a * eval @b

-- Another way to interpret it, ie. pretty print
class PP x where
  pp :: String

instance PP Zero where
  pp = "0"

instance PP a => PP (Succ a) where
  pp = "(1 + " <> pp @a <> ")"

instance (PP a, PP b) => PP (Add a b) where
  pp = "(" <> pp @a <> " + " <> pp @b <> ")"

instance (PP a, PP b) => PP (Mul a b) where
  pp = "(" <> pp @a <> " * " <> pp @b <> ")"

--

x_e :: Int
x_e = eval @(Mul (Add (Succ Zero) (Succ (Succ Zero))) (Succ (Succ Zero)))
-- 6

x_pp :: String
x_pp = pp @(Mul (Add (Succ Zero) (Succ (Succ Zero))) (Succ (Succ Zero)))
-- "(((1 + 0) + (1 + (1 + 0))) * (1 + (1 + 0)))"