[Haskell-cafe] Trying to write an Embedded DSL that threads a monad?
Oleg
oleg at okmij.org
Sat Oct 17 11:14:21 UTC 2015
> 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!
More information about the Haskell-Cafe
mailing list