Incidentally I did find a solution that fits into the type system and also
produces the correct result. This was done by making the global parameter
change type as well at each lambda so that it becomes a function with the
same arrity as the term. Unfortunately to evaluate these terms the program
needs fork and do redundant work at every application of lam (so it's a
major hack), though it does give me some confidence that a real solution is
possible perhaps by using dependent types?:
----
lam :: ((g->(g,a)) -> (g->(g',b))) -> (g->(a->g',a->b))
lam = (\ f -> \ g -> (\x -> fst $ (f (\ gv->(gv,x))) g,
\y -> snd $ (f (\ gv->(gv,y))) g ))
app :: (g->(a->g1,a->b)) -> (g->(g,a)) -> (g->(g1,b))
app = (\ eA eB -> \ gz -> let (gB, fB) = eB gz
in let (lgA, lfA) = eA gB
in (lgA fB, lfA fB) )
ext :: ((g1,a)->(g2,b))->(g0->(g1,a))->(g0->(g2,b))
ext = \f -> \a -> \g -> f (a g)
idCounter :: Num g => (g,a) -> (g, a)
idCounter = \(g, x) -> (g+1, x)
-- Example terms
trmA = lam (\x -> lam (\y -> app x y))
trmB = (lam (\y -> app trmC y))
trmC = (\g -> (\c->g,\c->c+3))
trmD = (\g -> (g,3))
trmE = app trmC trmD
trmF = (ext idCounter) trmD
trmG = app trmC (app trmC trmF)
trmH = app trmC trmE
---
Here's my original statement of the problem
http://hastebin.com/raw/bewiqihiyo
And here's all my code with new, http://hpaste.org/86273
Unfortunately, I don't know of a way to tell the compiler that essentially
the variables x and y in the lam function will always be applied to the
same value. Unfortunately, I've reached a limit of my understanding of how
pairs integrate with the type system in Haskell,
I've considered returning something other than a pair from my base function
(such as a function) but I have yet to figure that out.
Thanks for your insights,
Ian Bloom
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
