[Haskell-cafe] Implementing an embedded language that threads a global structure.
Ian Bloom
ianmbloom at gmail.com
Tue Apr 23 17:16:39 CEST 2013
I'm probably not the best person to answer your questions but here is a try:
I refer to my language as a mini language because I'm only showing lamda,
application and extension. You might choose to add other features like
symbol definitions, fixed points, pattern matching etc. which in the more
extensive versions of my code, I have.
The state monad would essentially be application only, it would not include
the very powerful lambda. I imagine you could implement such a language
using monads but it would just be the same thing, yet more difficult to
read and understand. By implementing the language embedded in Haskell you
can "piggyback" on Haskell's parser and type-checker.
This is the first paper I read about embedded languages. Compiling Embedded
Languages - CiteSeerX<http://www.google.com/url?sa=t&rct=j&q=compiling%20embedded%20languages&source=web&cd=2&ved=0CEMQFjAB&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.31.9782%26rep%3Drep1%26type%3Dpdf&ei=ABR2UdiHL7LB4APU7YH4Ag&usg=AFQjCNExxKJDQyFkNseb5ty09cLVYgpJ7w&sig2=_qJcPXKNp7GTEUme7BGCFw&bvm=bv.45512109,d.dmg>
You might think of embedded languages as a style or design pattern. It's
purpose is to abstract an entire category of behavior and simplify the task
of a person programming in the embedded language even if they are somehow
limited.
It seems like an embedded language would be a good option.
In the code sample below, if you add a string parameter to LambdaExtension
to include pieces of Perl code and make a version of the instance Pr for
printing perl code into a string you might be well on your way:
module Main (
main,
lam, app, ext,
trmA, trmB, trmC, trmD, trmE, trmF
) where
data LambdaExtension f = LExtend String f
int_ :: Integer -> LambdaExtension Integer
int_ x = LExtend (show x) x
add_ :: Num a => LambdaExtension (a -> a -> a)
add_ = LExtend "+" (+)
mul_ :: Num a => LambdaExtension (a -> a -> a)
mul_ = LExtend "*" (*)
leq_ :: Ord a => LambdaExtension (a -> a -> Bool)
leq_ = LExtend "<=" (<=)
not_ :: LambdaExtension (Bool -> Bool)
not_ = LExtend "not" not
class Calculus repr where
lam :: String -> (repr gl a -> repr gl b) -> repr gl (a->b)
def :: String -> repr gl a -> repr gl a
app :: repr gl (a->b) -> repr gl a -> repr gl b
fix :: String -> (repr gl a -> repr gl a) -> repr gl a
ext :: LambdaExtension e -> repr gl e
-- R is the evaluator
data R gl t = R t deriving Show
unR (R x) = x
instance Calculus R where
lam _ f = R (\z -> unR (f (R z)))
def _ f = R (unR f)
app e1 e2 = R ( (unR e1) (unR e2) )
fix _ f = R (fx (unR . f. R)) where fx f = f (fx f)
ext (LExtend _ f) = R f
-- Pr is the printer
newtype Pr g a = Pr String
unPr (Pr f) = f
instance Calculus Pr where
lam vN f = Pr(let var = Pr vN
body = unPr (f var)
in "\\"++ vN ++"->"++ body)
def dN f = Pr (dN ++ " = " ++ unPr f)
app e1 e2 = Pr(let e1b = unPr e1
e2b = unPr e2
in "(" ++ e1b ++ " " ++ e2b ++ ")")
fix vN f = Pr(let var = Pr vN
body = unPr (f var)
in "fix\\" ++ vN ++ "->" ++ body)
ext (LExtend s _) = Pr s
app2 f x y = (app (app f x) y)
app3 f x y z = (app (app2 f x y) z)
app4 f x y z w = (app (app3 f x y z) w)
-- Sample Terms
trmA = lam "x" (\x -> lam "y" (\y -> app x y))
trmB = lam "y" (\y -> app trmC y)
trmC = lam "c" (\c-> app2 (ext add_) c (ext (int_ 1)))
trmD = (ext (int_ 3))
trmE = app trmC trmD
trmF = app trmC trmE
main = do
putStrLn "Hello!"
putStrLn $ show $ unPr (trmA)
putStrLn $ show $ unPr (trmF)
putStrLn "**************"
Cheers,
Ian
On Tue, Apr 23, 2013 at 11:12 AM, Ian Bloom <ianmbloom at gmail.com> wrote:
> I'm probably not the best person to answer your questions but here is a
> try:
>
> I refer to my language as a mini language because I'm only showing lamda,
> application and extension. You might choose to add other features like
> symbol definitions, fixed points, pattern matching etc. which in the more
> extensive versions of my code, I have.
>
> The state monad would essentially be application only, it would not
> include the very powerful lambda. I imagine you could implement such a
> language using monads but it would just be the same thing, yet more
> difficult to read and understand. By implementing the language embedded in
> Haskell you can "piggyback" on Haskell's parser and type-checker.
>
> This is the first paper I read about embedded languages. Compiling
> Embedded Languages - CiteSeerX<http://www.google.com/url?sa=t&rct=j&q=compiling%20embedded%20languages&source=web&cd=2&ved=0CEMQFjAB&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.31.9782%26rep%3Drep1%26type%3Dpdf&ei=ABR2UdiHL7LB4APU7YH4Ag&usg=AFQjCNExxKJDQyFkNseb5ty09cLVYgpJ7w&sig2=_qJcPXKNp7GTEUme7BGCFw&bvm=bv.45512109,d.dmg>
> You might think of embedded languages as a style or design pattern. It's
> purpose is to abstract an entire category of behavior and simplify the task
> of a person programming in the embedded language even if they are somehow
> limited.
>
> It seems like an embedded language would be a good option.
> In the code sample below, if you add a string parameter to LambdaExtension
> to include pieces of Perl code and make a version of the instance Pr for
> printing perl code into a string you might be well on your way:
>
> module Main (
> main,
> lam, app, ext,
> trmA, trmB, trmC, trmD, trmE, trmF
> ) where
>
> data LambdaExtension f = LExtend String f
>
> int_ :: Integer -> LambdaExtension Integer
> int_ x = LExtend (show x) x
>
> add_ :: Num a => LambdaExtension (a -> a -> a)
> add_ = LExtend "+" (+)
>
> mul_ :: Num a => LambdaExtension (a -> a -> a)
> mul_ = LExtend "*" (*)
>
> leq_ :: Ord a => LambdaExtension (a -> a -> Bool)
> leq_ = LExtend "<=" (<=)
>
> not_ :: LambdaExtension (Bool -> Bool)
> not_ = LExtend "not" not
>
> class Calculus repr where
> lam :: String -> (repr gl a -> repr gl b) -> repr gl (a->b)
> def :: String -> repr gl a -> repr gl a
> app :: repr gl (a->b) -> repr gl a -> repr gl b
> fix :: String -> (repr gl a -> repr gl a) -> repr gl a
> ext :: LambdaExtension e -> repr gl e
>
> -- R is the evaluator
> data R gl t = R t deriving Show
> unR (R x) = x
>
> instance Calculus R where
> lam _ f = R (\z -> unR (f (R z)))
> def _ f = R (unR f)
> app e1 e2 = R ( (unR e1) (unR e2) )
> fix _ f = R (fx (unR . f. R)) where fx f = f (fx f)
> ext (LExtend _ f) = R f
>
> -- Pr is the printer
>
> newtype Pr g a = Pr String
> unPr (Pr f) = f
>
> instance Calculus Pr where
> lam vN f = Pr(let var = Pr vN
> body = unPr (f var)
> in "\\"++ vN ++"->"++ body)
> def dN f = Pr (dN ++ " = " ++ unPr f)
> app e1 e2 = Pr(let e1b = unPr e1
> e2b = unPr e2
> in "(" ++ e1b ++ " " ++ e2b ++ ")")
> fix vN f = Pr(let var = Pr vN
> body = unPr (f var)
> in "fix\\" ++ vN ++ "->" ++ body)
> ext (LExtend s _) = Pr s
>
>
> app2 f x y = (app (app f x) y)
> app3 f x y z = (app (app2 f x y) z)
> app4 f x y z w = (app (app3 f x y z) w)
>
> -- Sample Terms
> trmA = lam "x" (\x -> lam "y" (\y -> app x y))
> trmB = lam "y" (\y -> app trmC y)
> trmC = lam "c" (\c-> app2 (ext add_) c (ext (int_ 1)))
> trmD = (ext (int_ 3))
> trmE = app trmC trmD
> trmF = app trmC trmE
>
> main = do
> putStrLn "Hello!"
> putStrLn $ show $ unPr (trmA)
> putStrLn $ show $ unPr (trmF)
> putStrLn "**************"
>
> Cheers,
> Ian
>
> On Tue, Apr 23, 2013 at 12:42 AM, C K Kashyap <ckkashyap at gmail.com> wrote:
>
>> Hi Ian,
>> I have a couple of questions for you -
>>
>> 1. Could you explain why a lambda calculus like language embedded in
>> Haskell would be useful - I ask this because, the way I understand, Haskell
>> is already such a language - one could easily chose to restrict oneself to
>> just function definition and application. Perhaps an example problem which
>> can be expressed more clearly in your described embedded language but not
>> in Haskell would help me understand your point of view better.
>>
>> 2. Have you considered using the state monad?
>>
>> I am personally attempting to figure out a way to embed Perl in Haskell -
>> as in, describe Perl like code (but statically checked) in Haskell and then
>> generate Perl that I could use to execute on server farms which run on old
>> Linux kernels where I cannot run Haskell code.
>>
>> I totally get that "edge of understanding" feeling :)
>>
>> Regards,
>> Kashyap
>>
>>
>>
>>
>> On Mon, Apr 22, 2013 at 3:22 AM, Ian Bloom <ianmbloom at gmail.com> wrote:
>>
>>> Hi,
>>>
>>> I've been working on this problem for some time and I was hoping for
>>> some feedback. I'm trying to implement an embedded language that can thread
>>> a global structure through the evaluation of a term.
>>>
>>> A mini version of this language only includes three functions, lam, app
>>> and ext (lambda, apply and extension respectively). The only difference
>>> between this and other embedded languages is that terms embedded in an
>>> extension have access to a global variable that is invisible to the terms
>>> themselves.
>>>
>>> The writer of a term in this language can only access the global
>>> variable by applying an extension. The writer extensions insures that the
>>> effect of evaluation on the global variable is commutative and insures that
>>> the effect of the global variable on terms is constant regardless of the
>>> order of evaluation.
>>>
>>> For example the global variable could be a map with some sort of lazy
>>> processing. An extension that queries the map for an element might cause a
>>> change in the state of the map and return some information about an
>>> element, but as long as the change in state are commutative and the same
>>> information is returned about elements regardless of the order of
>>> evaluation then the concept is safe.
>>>
>>> My motivation for experimenting with such a language comes from a belief
>>> that certain complicated programs would be easier to express in such a
>>> language and that there might be very useful code transformations that
>>> could eventually be applied to such a language that would be possible
>>> because of the constraints on the behavior of extensions.
>>>
>>> However I have yet to properly implement a language in Haskell and so I
>>> decided to post what I have and look for comments.
>>>
>>> Basically the language takes a common form of embedded languages; a
>>> lambda expression such as
>>>
>>> \x y->x y
>>>
>>> would have the form:
>>>
>>> lam (\x -> lam (\y -> app x y))
>>>
>>> however in order to evaluate an expression the need to also apply it to
>>> a global term:
>>>
>>> lam (\x -> lam (\y -> app x y)) global
>>>
>>> Ideally the result of evaluating this would be a (global', \x y-> x y),
>>> a modified version of global paired with the term. So the type of the term:
>>>
>>> lam (\x -> lam (\y -> app x y)) is something like g -> (g, (a -> b) -> a
>>> -> b) where g is the type of global.
>>>
>>> From that came the first idea of the types of the evaluator functions:
>>>
>>> lam :: ( (g->(g,a)) -> (g->(g,b)) )-> (g->(g, a->b))
>>> app :: (g->(g,a->b)) -> (g->(g, a)) -> (g->(g,b))
>>>
>>> with some additional parenthesis for sake of clarity. Each sub-term has
>>> the type g->(g,t)
>>>
>>> any function can be included as an extension as long as the function has
>>> the type:
>>> (g->(g,a)) -> (g->(g,b))
>>>
>>> This seems to work well except that it seems to be impossible (as far as
>>> I've tried) to construct a definition for the lam function that both fits
>>> this type and properly passes the global through the entire evaluation. For
>>> example it's easy to define app like this:
>>>
>>> app :: (g->(g,a->b)) -> (g->(g,a)) -> (g->(g,b))
>>> app = (\ eA eB -> \ g0 -> let (gB, fB) = eB g0
>>> in let (gA, fA) = eA gB
>>> in (gA, fA fB) )
>>>
>>> but so far the definition of lam has eluded me. This is the closest I've
>>> come:
>>>
>>> lam :: ((g->(g,a)) -> (g->(g,b))) -> (g->(g,a->b))
>>> lam = (\ f -> \ g0 -> (g0, \x -> snd $ (f (\ gv->(gv,x))) g0 ))
>>>
>>> This fits the type but I fear this definition does not return the
>>> properly modified version of global.
>>>
>>> I tried some other iterations of this idea. In one effort the first
>>> argument of a function is extracted into the type of a term. So a term of
>>> type a->b has the type (g->a->(g,b)). And a term of type a has the type
>>> (g->((g, a)) such that:
>>>
>>> lam2 :: ((g->(g,a)) -> (g->(g,b))) -> (g->a->(g,b))
>>> lam2 = (\ f -> \ g x -> (f (\ gv -> (gv, x))) g)
>>>
>>> app2 :: (g->a->(g,b)) -> (g->(g,a)) -> (g->(g,b))
>>> app2 = (\ eA eB -> \ g0 -> let (gB, fB) = eB g0
>>> in eA gB fB )
>>>
>>> This seems like a step in the right direction unfortunately because the
>>> return type of lam is now (g->a->(g,b)) and not (g->(g->c)) we cannot type
>>> the term lam (\x -> lam (\y -> app x y)). In other words this language can
>>> only express unary and nullary functions.
>>> Just to help clarify this for myself I created to addition functions
>>> lam2Helper and app2Helper:
>>>
>>> lam2Helper :: (g->a->(g,b)) -> (g->(g,a->b))
>>> lam2Helper = (\f -> \g -> (g, \a -> snd $ f g a))
>>> app2Helper :: (g->(g,a->b)) -> (g->a->(g,b))
>>> app2Helper = (\f -> \g a-> let (g1, f1) = f g
>>> in (g1, f1 a))
>>>
>>> these allow me to create the term:
>>> lam2 (\x -> lam2Helper $ lam2 (\y -> app2 (app2Helper x) y))
>>>
>>> but just like the original definition of lam from my first try, there is
>>> no way to construct lam2Helper without improperly passing the global as
>>> I've done in my attempt.
>>>
>>> Finally on my third try I attempted to make every term have type
>>> (g->a->(g,b) by allowing embedded nullary functions to have the type
>>> (g->()->(g,t))
>>>
>>> lam3 :: ((g->()->(g,a)) -> (g->()->(g,b))) -> (g->a->(g,b))
>>> lam3 = (\ f -> \ g x -> (f (\ gv () -> (gv, x))) g () )
>>> app3 :: (g->a->(g,b)) -> (g->()->(g,a)) -> (g->()->(g,b))
>>> app3 = (\ eA eB -> \ gz () -> let (gB, fB) = eB gz ()
>>> in eA gB fB )
>>>
>>> This allows me to construct the term:
>>> lam (\x -> lam (\y -> app x y))
>>> but only by throwing out important type information...
>>>
>>> A compilable example of this is available here:
>>> http://hpaste.org/86273
>>>
>>> And with source candy here:
>>> http://hpaste.org/86274
>>>
>>> My goal at this point is just to understand the problem better. I feel
>>> I'm at the edge of my understanding of type systems and arity and I'm
>>> unsure if what I want to do is possible in Haskell. My goal would
>>> eventually be to construct a working prototype of such a language and to
>>> construct a proof that it maintains the types of terms and that the global
>>> variable is evaluated once by every subterm.
>>>
>>> I appreciate any insight, interest or help.
>>>
>>> Thanks,
>>> Ian Bloom
>>> ianmbloom at gmail.com
>>>
>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>>
>>
>
>
> --
> 718.755.5483
> http://ianbloom.com/
>
--
718.755.5483
http://ianbloom.com/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130423/52a58e99/attachment.htm>
More information about the Haskell-Cafe
mailing list