(See Defunctionalization at Work for a background on the defunctionalization technique, The reflexive CHAM and the join-calculus for a background on join calculus.) What I do is not really defunctionalization, but I miss the right term for that.
Lambda calculus can be encoded in join calculus (JC). Algebraic datatypes can be encoded in either. A decent functional PL (think ML) can be encoded in JC. Yesterday I had an idea of looking at the reversal of this encoding - take a JC term, and tell if it is an image of ML term under this encoding (similar in spirit to recovering user-lambdas from brutally CPSed terms). Better yet, take a JC term and split it into functional and (emmm...) superfunctional pieces.
Then I wandered into implementation ideas, and suddenly decided I need to explore some kind of first order JC. I mean, definitions in JC nest and form structures very similar in spirit to closures. What if I closure-convert JC semantics, tinker it a bit, and them put closures back?
I analyzed pages 5-6 of the JC paper, and started scribbling. Spoiled by UML, I didn't use sets or functions, only informal diagrams. "I'll validate it later", thought I.
Everything went fine, until I stumbled upon necessity to construct new instances. Need for elegant generation of fresh names and manifestedly safe references to them was what stopped me... Will have to check literature for inspiration.
Subscribe to:
Post Comments (Atom)
1 comment:
I think I have a nice hack for avoiding gensym-like state in the abstract machine - just use path on new-labels as object id.
I probably stole this from someone, but will keep it anyway (unless it does not work :) ).
Post a Comment