Oleg,
On Thu, Sep 24, 2009 at 1:54 AM,
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)" -}
Thank you for this example code. Using the technique you show here (and that others have mentioned in discussion in these two threads), i.e., lifting type parameters into the class head, one is able to put constraints on that type when defining instances, and hence modularly define tagless EDSLs. I have played around a bit with this technique and it seems to work well. I need to experiment more, and construct a more substantial EDSL to really evaluate this approach. Sincerely, Brad