Quick question about your talk: Can you do dynamic programs that use memoization efficiently? For example, can you do a memoized version of your fib function efficiently?
As an aside, you mention someone suggested doing this in Agda. Another middle alternative would be Concoqtion. It would match your goal of using the stronger types in the library, and not letting them show outside the library.
How easy or hard is it to express a context-dependent rewrite rule that would work on such terms (terms with a "let" that acts as a global store). See a concrete example of how such a rewrite is expressed could help answer this.
Here I'm wondering about the impact on the overall source code used to describe the rewrites, as well as how efficiently such rewrites can be executed. Commenting on how the example is executed could also help here too.
Rewriting and strategies are important tools for the engineering of different part of the DSL tool chain and Andy's paper present a snapshot of where the his Haskell-based system is right now. He has done a great job in implementing this strongly typed prototype which can express and execute rewrites and more complex startegies depending on context. (There are still a few issues - also mentioned in the paper: performance and conceptual complexity.)
One question I had was how much struggle it was to massage the "well typed rewriting" into the Haskell type system.
Another question is the relationship to other rewriting papers ([Noort et al. A lightweight approach to datatype-generic rewriting, WGP2008?]) and generic programming libraries (Smash, Uniplate, CompOs, ...)
Walid, if I have understood your question correctly, you might enjoy the paper [1] that uses Stratego-style rewriting to evaluate various versions of lambda calculus including variants with explicit substitutions and sharing.
I presume something similar could be encoded in KURE. A version we did using our Kiama library for Scala is at:
E.g., ReduceSubst.scala shows explicit substitutions represented by lets. In this case it is doing multiple traversals but later versions optimise this more (see [1]).
cheers, Tony
[1] Dolstra, E., and Visser, E. Building interpreters with rewriting strategies. In Proceedings of the 2nd Workshop on Language Descriptions, Tools and Applications (2002), vol. 65 of Electronic Notes in Theoretical Computer Science, pp. 57–76. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.2565
Q1: The struggle with the type system. Well, this has been fought, and adding a single instance for each datatype is quite straightforward, now. There is also kure-your-boilerplate, which uses template haskell to generate the instance for you.
It was a fight at the time, but more with the *design*, and leting this settle.
Walid: it shows how the binding of (possibly shared) values can be represented explicitly in the terms and then used in rewrites. So the lets are not a "global store" but a scoped one. It's quite a natural encoding, I think. To make this more concrete, see the ReduceSubst.scala link I sent earlier for real code.
Regarding efficiency, it depends on the strategy that controls the traversal. In the paper the simplest case they consider does a complete traversal of the tree to search for each redex. Their better versions use more sophisticated strategies to avoid re-substituting and implement sharing (again via an explicit term).
Again, I think it's quite natural for this problem at least, but there will be some penalty for copying bindings down to where they are needed. Arguably this is better done with a data structure to the side or via a higher-level mechanism such as reference attributes.
Hi Andy,
ReplyDeleteQuick question about your talk: Can you do dynamic programs that use memoization efficiently? For example, can you do a memoized version of your fib function efficiently?
As an aside, you mention someone suggested doing this in Agda. Another middle alternative would be Concoqtion. It would match your goal of using the stronger types in the library, and not letting them show outside the library.
Great talk!
Yes, if you add a 'Let' to the syntax tree being rewritten, to store the shared binding at runtime.
ReplyDeleteHow easy or hard is it to express a context-dependent rewrite rule that would work on such terms (terms with a "let" that acts as a global store). See a concrete example of how such a rewrite is expressed could help answer this.
ReplyDeleteHere I'm wondering about the impact on the overall source code used to describe the rewrites, as well as how efficiently such rewrites can be executed. Commenting on how the example is executed could also help here too.
Thank you!
Rewriting and strategies are important tools for the engineering of different part of the DSL tool chain and Andy's paper present a snapshot of where the his Haskell-based system is right now. He has done a great job in implementing this strongly typed prototype which can express and execute rewrites and more complex startegies depending on context. (There are still a few issues - also mentioned in the paper: performance and conceptual complexity.)
ReplyDeleteOne question I had was how much struggle it was to massage the "well typed rewriting" into the Haskell type system.
Another question is the relationship to other rewriting papers ([Noort et al. A lightweight approach to datatype-generic rewriting, WGP2008?]) and generic programming libraries (Smash, Uniplate, CompOs, ...)
Walid, if I have understood your question correctly, you might enjoy the paper [1] that uses Stratego-style rewriting to evaluate various versions of lambda calculus including variants with explicit substitutions and sharing.
ReplyDeleteI presume something similar could be encoded in KURE. A version we did using our Kiama library for Scala is at:
http://code.google.com/p/kiama/source/browse/#hg/src/kiama/example/lambda
E.g., ReduceSubst.scala shows explicit substitutions represented by lets. In this case it is doing multiple traversals but later versions optimise this more (see [1]).
cheers,
Tony
[1] Dolstra, E., and Visser, E. Building interpreters with rewriting strategies. In Proceedings of the
2nd Workshop on Language Descriptions, Tools and Applications (2002), vol. 65 of Electronic Notes in
Theoretical Computer Science, pp. 57–76.
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.2565
Q1: The struggle with the type system. Well, this has been fought, and adding a single instance for each datatype is quite straightforward, now. There is also kure-your-boilerplate, which uses template haskell to generate the instance for you.
ReplyDeleteIt was a fight at the time, but more with the *design*, and leting this settle.
Thanks Anthony!
ReplyDeleteCan you give me an idea of what answers it gives to my questions (or if they clarification)?
Walid: it shows how the binding of (possibly shared) values can be
ReplyDeleterepresented explicitly in the terms and then used in rewrites. So the
lets are not a "global store" but a scoped one. It's quite a natural
encoding, I think. To make this more concrete, see the
ReduceSubst.scala link I sent earlier for real code.
Regarding efficiency, it depends on the strategy that controls the
traversal. In the paper the simplest case they consider does a
complete traversal of the tree to search for each redex. Their better
versions use more sophisticated strategies to avoid re-substituting
and implement sharing (again via an explicit term).
Again, I think it's quite natural for this problem at least, but there will be some penalty for copying bindings down to where they are needed. Arguably this is better done with a data structure to the side or via a higher-level mechanism such as reference attributes.
Tony