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

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][>>][..]