-- Tagless interpreters.  Represent a language syntax as the member
-- functions of a type class Symantics.  Instances of the type class
-- add meaning.  Main benefit: the represented language can be typed
-- with its types embedded in the metalanguage.

-- Derived from http://okmij.org/ftp/tagless-final/Incope.hs

import Control.Applicative

-- LANGUAGE

class Symantics repr where
    -- Lift constants into the domain
    int   :: Int   -> repr Int;
    bool  :: Bool  -> repr Bool;
    float :: Float -> repr Float;
    
    -- Primitive operations
    add :: Num a => repr a -> repr a -> repr a
    mul :: Num a => repr a -> repr a -> repr a

    leq :: Ord a => repr a -> repr a -> repr Bool
    if_ :: repr Bool -> repr a -> repr a -> repr a

-- Utilities
if' :: Bool -> a -> a -> a
if' b t e = if b then t else e


-- PROGRAMS
test1 () = add (int 1) (int 2)


-- INTERPRETERS

-- ------------------------------------------------------------------------
-- The interpreter
-- It is a typed, tagless interpreter: R is not a tag. The interpreter
-- never gets stuck, because it evaluates typed terms only

newtype R a = R a deriving Show
unR (R x) = x

instance Symantics R where
    int x = R x
    bool b = R b
    float f = R f

    add e1 e2 = R( (unR e1) + (unR e2) )
    mul e1 e2 = R( (unR e1) * (unR e2) )
    leq e1 e2 = R( (unR e1) <= (unR e2) )
    if_ be et ee = R( if (unR be) then unR et else unR ee )

compR = unR

mkitest f = compR (f ())

itest1 = mkitest test1


-- HACKS

-- 0. Direct interpretation
-- instance Num a => Symantics (Num a)


-- 1. Lists as an example of applicative functors wrapping basic
-- types.
instance Symantics [] where
    int   = pure
    bool  = pure
    float = pure
    add   = liftA2 (+)
    mul   = liftA2 (*)
    leq   = liftA2 (<=)
    if_   = liftA3 if'


-- 2. Binary vectors.  Another example of applicative.
data Bin a = a :* a deriving (Show, Eq)
infixr 5 :*

instance Functor Bin where
    fmap f (x :* x') = (f x :* f x')

instance Applicative Bin where
    pure x = x :* x
    (f :* f') <*> (x :* x') = (f x) :* (f' x')

instance Symantics Bin where
    int   = pure
    bool  = pure
    float = pure
    add   = liftA2 (+)
    mul   = liftA2 (*)
    leq   = liftA2 (<=)
    if_   = liftA3 if'