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

[Brad Larsen]

Oleg,

On Thu, Sep 24, 2009 at 1:54 AM,  <oleg at okmij.org> wrote:
>
> 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