[Haskell-cafe] Trying to write an Embedded DSL that threads a monad?

[Oleg]

> Thanks for pointing that out, this is my first time encountering
> tagless-final. The use of the :-> data constructor seems to solve a lot of
> problems.

It truth the :-> constructor does not bring anything new. When we
write Symantics defining the EDSL as

        class Symantics repr where
          lam :: (repr a -> repr b) -> repr (a->b)

then the first and the second occurrences of '->' refer to Haskell
functions. However, the last occurrence of '->', in repr (a->b),
refers to a function of the EDSL -- to the object function rather than
the meta-language function. It is convenient to use the same operator
'->' for both, but we should understand these are different
entities. The constructor :-> just makes the distinction clear.
This is similar to the idiomatic Haskell definition like

        newtype Foo a = Foo (a -> String)

where the two occurrences of Foo refer to different things: one is a
type constructor and the other is a data constructor.

Whereas the meaning of Haskell's '->' is fixed, the meaning of the
object language '->' is up to the interpreter. It could be a
function, it could be a monadic function, it could be anything that
takes two type arguments (and uses them in some way, or throws them
away).


> I'm wondering how to introduce a haskell function as an embedded
> value in such an EDSL but I think I will try it out.

First of all, lam above already showed how to turn a Haskell function,
of a particular type (repr a -> repr b), into the EDSL function. One
can `embed' any Haskell function, by adding to Semantics the method

        lift :: (a -> b) -> repr (a -> b)

for example. But your interpreters may need to implement it! It may be
simpler to restrict the class of functions you want to embed. Thus,
you will define methods of Semantics

        plus  :: repr (Int -> Int -> Int)
        minus :: repr (Int -> Int -> Int)

etc. Since one can add more methods at any time, we do not need to
imagine right upfront all the functions we may wish to embed. We can
add more as the need arises.

Finally, if all your are interested is counting operations (and
perhaps writing some logs), you don't need any monads. Tagless-Final
tutorials (and the JFP paper) demonstrated many interpreters that do
counting (the size of the term, the depth of the term, etc). If you
wish to count reductions, you will define the variation on the R
interpreter as shown below. Whether RCount is a monad or not, I don't
even care. There is nothing there that requires it.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

module Count where

class Symantics repr where
  int  :: Int -> repr Int
  plus :: repr (Int -> Int -> Int)
  lam  :: (repr a -> repr b) -> repr (a -> b)
  app  :: repr (a->b) -> (repr a -> repr b)

infixl 1 `app`
-- meta-circular interpreter with counting

type Count = Int


data RCount a = RCount (TC a) Count


type family TC a where
  TC (a -> b) = RCount a -> RCount b
  TC a        = a


instance Symantics RCount where
  int x = RCount x 0
  plus  = RCount (\ (RCount x cx) ->
            RCount (\ (RCount y cy) -> RCount (x+y) (cx+cy)) 0) 0
  lam f = RCount f 0
  app (RCount f cf) x = let (RCount v cv) = f x in
                        RCount v (cf+cv+1)


test1 = lam (\x -> plus `app` x `app`
                   (plus `app` x `app` int 1)) `app` (int 3)


test1R = let (RCount x c) = test1 in (x,c)
-- (7, 5)
-- There are indeed 5 occurrences of app in test1

test2 = lam (\x -> plus `app` x `app`
                   (plus `app` x `app` int 1)) `app`
        (plus `app` (int 3) `app` (int 4))
        

test2R = let (RCount x c) = test2 in (x,c)
-- (15, 9)
-- our semantics is CBName!