No subject
Wed Apr 10 17:18:51 CEST 2013
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
--089e01293fe2df7f7f04dae5f785
Content-Type: text/html; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr">Hi,<br><br>I've been working on this problem for some =
time and I was hoping for some feedback. I'm trying to implement an emb=
edded language that can thread a global structure through the evaluation of=
a term.<br>
<br>A mini version of this language only includes three functions, lam, app=
and ext (lambda, apply and extension respectively). The only difference be=
tween this and other embedded languages is that terms embedded in an extens=
ion have access to a global variable that is invisible to the terms themsel=
ves.<br>
<br>The writer of a term in this language can only access the global variab=
le by applying an extension. The writer extensions insures that the effect =
of evaluation on the global variable is commutative and insures that the ef=
fect of the global variable on terms is constant regardless of the order of=
evaluation.<br>
<br>For example the global variable could be a map with some sort of lazy p=
rocessing. An extension that queries the map for an element might cause a c=
hange 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 informatio=
n is returned about elements regardless of the order of evaluation then the=
concept is safe.<br>
<br>My motivation for experimenting with such a language comes from a belie=
f that certain complicated programs would be easier to express in such a la=
nguage 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.<br>
<br>However I have yet to properly implement a language in Haskell and so I=
decided to post what I have and look for comments.<br><br>Basically the la=
nguage takes a common form of embedded languages; a lambda expression such =
as<br>
<br>\x y->x y<br><br>would have the form:<br><br>lam (\x -> lam (\y -=
> app x y))<div><br>however in order to evaluate an expression the need =
to also apply it to a global term:<br><br>lam (\x -> lam (\y -> app x=
y)) global<br>
<br>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 t=
he term:<br><br>lam (\x -> lam (\y -> app x y)) is something like g -=
> (g, (a -> b) -> a -> b) where g is the type of global.<br>
<br>From that came the first idea of the types of the evaluator functions:<=
/div><div><br>lam :: ( (g->(g,a)) -> (g->(g,b)) )-> (g->(g, =
a->b))<br>app :: (g->(g,a->b)) -> (g->(g, a)) -> (g->(=
g,b))</div>
<div><br>with some additional parenthesis for sake of clarity. Each sub-ter=
m has the type g->(g,t)<br><br>any function can be included as an extens=
ion as long as the function has the type:<br>(g->(g,a)) -> (g->(g,=
b))<br>
<br>This seems to work well except that it seems to be impossible (as far a=
s 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:<br>
<br>app :: (g->(g,a->b)) -> (g->(g,a)) -> (g->(g,b))<br>a=
pp =3D (\ eA eB -> \ g0 -> let =A0 =A0 (gB, fB) =3D eB g0<br>=A0=A0 =
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 in let =
(gA, fA) =3D eA gB<br>=A0=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =
=A0 =A0 =A0 =A0 =A0 =A0 in =A0 =A0 (gA, fA fB) )<br>
<br>but so far the definition of lam has eluded me. This is the closest I&#=
39;ve come:<br><br>lam :: ((g->(g,a)) -> (g->(g,b))) -> (g->=
(g,a->b))<br>lam =3D (\ f -> \ g0 -> (g0, \x -> snd $ (f (\ gv-=
>(gv,x))) g0 ))<br>
<br>This fits the type but I fear this definition does not return the prope=
rly modified version of global.<br><br>I tried some other iterations of thi=
s idea. In one effort the first argument of a function is extracted into th=
e 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:<br>
<br>lam2 :: ((g->(g,a)) -> (g->(g,b))) -> (g->a->(g,b))<b=
r>lam2 =3D (\ f -> \ g x -> (f (\ gv -> (gv, x))) g)</div><div><br=
>app2 :: (g->a->(g,b)) -> (g->(g,a)) -> (g->(g,b))<br>app=
2 =3D (\ eA eB -> \ g0 -> let (gB, fB) =3D eB g0<br>
=A0=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =
=A0 in =A0eA gB fB )</div><div><br></div><div>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 -&g=
t; lam (\y -> app x y)). In other words this language can only express u=
nary and nullary functions.</div>
<div>Just to help clarify this for myself I created to addition functions l=
am2Helper and app2Helper:</div><div><br></div><div><div>lam2Helper :: (g-&g=
t;a->(g,b)) -> (g->(g,a->b))</div><div>lam2Helper =3D (\f ->=
\g -> (g, \a -> snd $ f g a))</div>
<div>app2Helper :: (g->(g,a->b)) -> (g->a->(g,b))</div><div>=
app2Helper =3D (\f -> \g a-> let (g1, f1) =3D f g</div><div>=A0=A0 =
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 in (g1, f1 a))</div><div><b=
r></div><div>these allow me to create the term:</div>
<div>lam2 (\x -> lam2Helper $ lam2 (\y -> app2 (app2Helper x) y))<br>=
</div><div><br></div><div>but just like the original definition of lam from=
my first try, there is no way to construct lam2Helper without improperly p=
assing the global as I've done in my attempt.</div>
<div><br></div><div>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))</div><br><div><div>lam3 :: ((g->()->(g=
,a)) -> (g->()->(g,b))) -> (g->a->(g,b))</div>
<div>lam3 =3D (\ f -> \ g x -> (f (\ gv () -> (gv, x))) g () )</di=
v><div>app3 :: (g->a->(g,b)) -> (g->()->(g,a)) -> (g->=
()->(g,b))</div><div>app3 =3D (\ eA eB -> \ gz () -> let (gB, fB) =
=3D eB gz ()</div>
<div>=A0=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0in =A0eA=
gB fB )</div></div><div><br></div><div>This allows me to construct the ter=
m:</div><div>lam (\x -> lam (\y -> app x y))</div><div>but only by th=
rowing out important type information...</div>
<div><br></div><div>A compilable example of this is available here:=A0</div=
><div><a href=3D"http://hpaste.org/86273">http://hpaste.org/86273</a><br></=
div><div><br></div><div>And with source candy here:</div><div><a href=3D"ht=
tp://hpaste.org/86274">http://hpaste.org/86274</a><br>
</div><div><br></div><div>My goal at this point is just to understand the p=
roblem better. I feel I'm at the edge of my understanding of type syste=
ms 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 la=
nguage and to construct a proof that it maintains the types of terms and th=
at the global variable is evaluated once by every subterm.</div>
<div><br></div><div>I appreciate any insight, interest or help.</div><div><=
br></div><div>Thanks,</div><div>Ian Bloom</div><div><a href=3D"mailto:ianmb=
loom at gmail.com">ianmbloom at gmail.com</a></div><div><br></div><div><br></div>
<div><br></div>
<div><br></div></div></div>
--089e01293fe2df7f7f04dae5f785--
More information about the Haskell-Cafe
mailing list