It's rather tangential to the main point of Ken's presentation, but I was very intrigued by Oleg's observations about "initial" and "final" embeddings. As I understood Oleg's intention, an "initial embedding" of a DSL simply uses an algebraic datatype matching the grammar of a DSL; a "final embedding" essentially replaces the algebraic datatype with a type parameter, and the constructors with smart constructors.
I can see that the "initial embedding" really is as an initial algebra in the categorical sense; is the claim that the "final embedding" is really as a terminal object in some category? For example, I could imagine that the "initial embedding" is initial in the sense that there is a suitable mapping *to* any other embedding. Dually, is there a embedding that is "final" in the sense that there is a suitable mapping *from* any other embedding to it?
[I had posted this earlier in another post before Ken put up his talk post.]
I absolutely loved your discussant presentation! Where does the initial/final embedding terminology come from? Can you provide a reference? (These forms seems to correspond to what is typically called deep/shallow embedding)?
* Slide 18 about variable ordering is new content not in the paper (but it should have been in the paper) * Slide 19 contains an updated performance number, including numbers for MLton.
Notes from Oleg:
Performance comparison with C/C++ show that the BDD embedding is efficient.
For SGCL embedding, smart constructors are provided to make the embedding prettier. Camlp4 could make it prettier still.
One interpreter is shown for the SGCL language, interpreting an SGCL term as a set of reachable states, efficiently represented using BDD. The interpreter is a non-standard,
One question: use the initial embedding for both DSL, or the final embedding for both. It makes sense indeed to try the final embedding for SGCL.
Alas, the paper was short on most interesting details of integrating BuDDy's own memory management with GC of ML. Such things are quite tricky and non-trivial. Could the region management help?
Performance comparison is quite stale: the paper used OCaml 3.04 whereas the current version is 3.11. I am very curious about the performance numbers for MLton.
The paper short-changes high-level languages when it comes to implementing BDD. ML systems have GC that is (much) better than refcounting. Mlton is very efficient. MLKit has regions management. Still, implementing a good BDD library is hard. It makes much more sense to interface to the existing good library than to write a BDD implementation from scratch.
The work by Monica Lam (embedding BDD in Datalog and use that for writing various program analyses) makes an excellent case for the paper and confirms the conclusions. (abstract, or symbolic) evaluator: sort of a model checker.
It's rather tangential to the main point of Ken's presentation, but I was very intrigued by Oleg's observations about "initial" and "final" embeddings. As I understood Oleg's intention, an "initial embedding" of a DSL simply uses an algebraic datatype matching the grammar of a DSL; a "final embedding" essentially replaces the algebraic datatype with a type parameter, and the constructors with smart constructors.
ReplyDeleteI can see that the "initial embedding" really is as an initial algebra in the categorical sense; is the claim that the "final embedding" is really as a terminal object in some category? For example, I could imagine that the "initial embedding" is initial in the sense that there is a suitable mapping *to* any other embedding. Dually, is there a embedding that is "final" in the sense that there is a suitable mapping *from* any other embedding to it?
[I had posted this earlier in another post before Ken put up his talk post.]
ReplyDeleteI absolutely loved your discussant presentation! Where does the initial/final embedding terminology come from? Can you provide a reference? (These forms seems to correspond to what is typically called deep/shallow embedding)?
[Posted for Ken by Walid]
ReplyDeleteNotes for Ken's slides:
* Slide 18 about variable ordering is new content not in the paper (but it should have been in the paper)
* Slide 19 contains an updated performance number, including numbers for MLton.
Notes from Oleg:
Performance comparison with C/C++ show that the BDD embedding is efficient.
For SGCL embedding, smart constructors are provided to make the embedding prettier. Camlp4 could make it prettier still.
One interpreter is shown for the SGCL language, interpreting an SGCL term as a set of reachable states, efficiently represented using BDD. The interpreter is a non-standard,
One question: use the initial embedding for both DSL, or the final embedding for both. It makes sense indeed to try the final embedding for SGCL.
Alas, the paper was short on most interesting details of integrating BuDDy's own memory management with GC of ML. Such things are quite tricky and non-trivial. Could the region management help?
Performance comparison is quite stale: the paper used OCaml 3.04 whereas the current version is 3.11. I am very curious about the performance numbers for MLton.
The paper short-changes high-level languages when it comes to implementing BDD. ML systems have GC that is (much) better than refcounting. Mlton is very efficient. MLKit has regions management. Still, implementing a good BDD library is hard. It makes much more sense to interface to the existing good library than to write a BDD implementation from scratch.
The work by Monica Lam (embedding BDD in Datalog and use that for writing various program analyses) makes an excellent case for the paper and confirms the conclusions. (abstract, or symbolic) evaluator: sort of a model checker.