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!