[Haskell-cafe] Beginning of a meta-Haskell [was: An issue with the ``finally tagless'' tradition]

[oleg at okmij.org]

The topic of an extensible, modular interpreter in the tagless final
style has come up before. A bit more than a year ago, on a flight from
Frankfurt to San Francisco I wrote two interpreters for a trivial
subset of Haskell or ML (PCF actually), just big enough for Power,
Fibonacci and other classic functions. The following code is a
fragment of meta-Haskell. It defines the object language and two
interpreters: one is the typed meta-circular interpreter, and the
other is a non-too-pretty printer. We can write the expression once:

> power =
>   fix $ \self ->
>   lam $ \x -> lam $ \n ->
>     if_ (n <= 0) 1
>         (x * ((self $$ x) $$ (n - 1)))

and interpret it several times, as an integer

> -- testpw :: Int
> testpw = (unR power) (unR 2) ((unR 7)::Int)
> -- 128

or as a string

> -- testpwc :: P.String
> testpwc = showQC power

{-
 "(let self0 = (\\t1 -> (\\t2 -> (if (t2 <= 0) then 1 else (t1 * ((self0  t1)  (t2 - 1)))))) in self0)"
-}

The code follows. It is essentially Haskell98, with the exception of
multi-parameter type classes (but no functional dependencies, let
alone overlapping instances).

{-# LANGUAGE NoMonomorphismRestriction, NoImplicitPrelude #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

-- A trivial introduction to `meta-Haskell', just enough to give a taste
-- Please see the tests at the end of the file

module Intro where

import qualified Prelude as P
import Prelude (Monad(..), (.), putStrLn, IO, Integer, Int, ($), (++),
                (=<<), Bool(..))
import Control.Monad (ap)
import qualified Control.Monad.State as S

-- Definition of our object language
-- Unlike that in the tagless final paper, the definition here is spread
-- across several type classes for modularity

class QNum repr a where
    (+) :: repr a -> repr a -> repr a
    (-) :: repr a -> repr a -> repr a
    (*) :: repr a -> repr a -> repr a
    negate :: repr a -> repr a
    fromInteger :: Integer -> repr a
infixl 6 +, -
infixl 7 *

class QBool repr where
    true, false :: repr Bool
    if_ :: repr Bool -> repr w -> repr w -> repr w

class QBool repr => QLeq repr a where
    (<=) :: repr a -> repr a -> repr Bool
infix 4 <=

-- Higher-order fragment of the language

class QHO repr  where
    lam  :: (repr a -> repr r) -> repr (a -> r)
    ($$) :: repr (a -> r) -> (repr a -> repr r)
    fix  :: (repr a -> repr a) -> repr a
infixr 0 $$

-- The first interpreter R -- which embeds the object language in
-- Haskell. It is a meta-circular interpreter, and so is trivial.
-- It still could be useful if we wish just to see the result
-- of our expressions, quickly
newtype R a = R{unR :: a}

instance P.Num a => QNum R a where
    R x + R y = R $ x P.+ y
    R x - R y = R $ x P.- y
    R x * R y = R $ x P.* y
    negate      = R . P.negate . unR
    fromInteger = R . P.fromInteger

instance QBool R where
    true  = R True
    false = R False
    if_ (R True)  x y = x
    if_ (R False) x y = y

instance QLeq R Int where
    R x <= R y = R $ x P.<= y

instance QHO R where
    lam f      = R $ unR . f . R
    R f $$ R x = R $ f x
    fix f      = f (fix f)

-- The second interpreter: pretty-printer
-- Actually, it is not pretty, but sufficient

newtype S a = S{unS :: S.State Int P.String}

instance QNum S a where
    S x + S y = S $ app_infix "+" x y
    S x - S y = S $ app_infix "-" x y
    S x * S y = S $ app_infix "*" x y
    negate (S x) = S $ (return $ \xc -> "(negate " ++ xc ++ ")") `ap` x
    fromInteger = S . return . P.show

app_infix op x y = do
  xc <- x
  yc <- y
  return $ "(" ++ xc ++ " " ++ op ++ " " ++ yc ++ ")"

instance QBool S where
    true  = S $ return "True"
    false = S $ return "False"
    if_ (S b) (S x) (S y) = S $ do
                                bc <- b
                                xc <- x
                                yc <- y
                                return $ "(if " ++ bc ++ " then " ++ xc ++ 
                                         " else " ++ yc ++ ")"
instance QLeq S a where
    S x <= S y = S $ app_infix "<=" x y

newName stem = do
  cnt <- S.get
  S.put (P.succ cnt)
  return $ stem ++ P.show cnt
  
instance QHO S where
 S x $$ S y = S $ app_infix "" x y

 lam f = S $ do
             name <- newName "t"
             let xc = name
             bc <- unS . f . S $ return xc
             return $ "(\\" ++ xc ++ " -> " ++ bc ++ ")"

 fix f = S $ do
             self <- newName "self"
             let sc = self
             bc <- unS . f . S $ return sc
             return $ "(let " ++ self ++ " = " ++ bc ++ " in " ++ sc ++ ")"

showQC :: S a -> P.String
showQC (S m) = S.evalState m (unR 0)

-- ------------------------------------------------------------------------
--   Tests

-- Perhaps the first test should be the power function...
-- The following code can be interpreted and compiled just as it is...

power =
  fix $ \self ->
  lam $ \x -> lam $ \n ->
    if_ (n <= 0) 1
        (x * ((self $$ x) $$ (n - 1)))

-- The interpreted result
-- testpw :: Int
testpw = (unR power) (unR 2) ((unR 7)::Int)
-- 128

-- The result of compilation. 
-- testpwc :: P.String
testpwc = showQC power
 
{-
"(let self0 = (\\t1 -> (\\t2 -> (if (t2 <= 0) then 1 else (t1 * ((self0  t1)  (t2 - 1)))))) in self0)"
-}