[<<][meta][>>][..]
Sun Feb 21 09:33:36 CET 2010

Tagless interpreters

I wonder if there's any benefit to using a tagless approach to
representing the Ai.hs code.

The main idea behind tagless interpreters is to replace algebraic data
types with type classes; i.e. shifting one level.  The benefit is that
the object language types can be encoded as metalanguage types.

For the dataflow language it is important to be able to distinguish
different types.  These are a minimum: bool, int, float|double.


Let's have another look at [1][2].  I'm starting with the class
definition in Fig. 3.  I do not need higher order functions; only
expressions.  Let's worry about abstraction later.  This means leave
out lam & app and concentrate on a rep with two types (int & bool),
primitive expressions and conditionals.

class Symantics repr where
    int   :: Int  -> repr Int;
    bool  :: Bool -> repr Bool;
    float :: Float -> repr Float;
    
    add :: repr Int -> repr Int -> repr Int
    mul :: repr Int -> repr Int -> repr Int
    leq :: repr Int -> repr Int -> repr Bool
    if_ :: repr Bool -> repr a -> repr a -> repr a

So, what is `repr'?  It's a type constructor taking one argument.
Let's take an arbitrary one: [].

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

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

This suggests that applicative functors can be used in general.

Can we simplify and make Symantics inherit from the number
typeclasses?  I don't really see how to do that though.  I tried
several things but ended up with a lot of kind errors on one path and
needing UndecidableInstances on another so I'm going to wait until I
understand why.

The simplest way to side-step the problem seems to be this:

class Symantics repr where
    -- Lift constants into the domain
    int   :: Int   -> repr Int;
    bool  :: Bool  -> repr Bool;
    float :: Float -> repr Float;
    
    -- Primitive operations
    bop :: Num a => (a -> a -> a)     -> repr a -> repr a -> repr a
    cop :: Ord a => (a -> a -> Bool)  -> repr a -> repr a -> repr Bool
    if_  :: repr Bool -> repr a -> repr a -> repr a


Here Symantics abstracts over the different functions and only
requires that each interpreter (repr) has lifting functions.

But that breaks what we inteded to create: it doesn't capture semantic
differences between + and *.  It looks like there is no way around
somehow relating Symantics and the number typeclasses.  This could be
done as merely an interface, i.e. (+) from Num delegates to add from
Symantics.

Again:

  * Symantics class encodes object language + type.

  * Symantics instance encodes language interpreter.

  * It's possible to build the Ai.hs style interpretation on top of
    this by relating the numeric type classes to Symantics.

Now try the latter in a concrete way, then try to generalize the
layering or composition of different types.

I wonder: why is it not possible to embed MetaOCaml in Haskell this
way?  In [3] line 163 it says "we never pattern-match on bytecode".
So it seems that indeed this allows a lot of the features of MetaOCaml
to carry over to Haskell, but probably not all.  How are they
different?

The conversion to ByteCode in [3] instantiates to typed GADT.
However, it seems it's useful to convert the (type-checked!) language
constructs into an untyped form if the form is never inspected no type
errors can be injected.

Conclusion: it's possibly useful to write a typed layer _on top of_
the Term data type in Ai.hs; this layer would then ensure static type
safety.


[1] entry://../compsci/20090823-121637
[2] http://okmij.org/ftp/tagless-final/APLAS.pdf
[3] http://okmij.org/ftp/tagless-final/Incope.hs



[Reply][About]
[<<][meta][>>][..]