4 ms·

> Why? Because I care about soundness. And especially soundness for combinations of under-specified semantic models, because eDSLs are useful exactly when the

• sklogic 11y ago
  > Because I care about soundness. And what's the problem with soundness? I can even derive formal proofs for simple DSLs when I have too. I never had any issues with mixing semantic properties of DSLs on any level of abstraction - and the higher the abstraction level, the easier it is to mix without caring at all about the underlying semantics. For example - I've got a generic PEG frontend language. I can mix it into nearly any combination of execution semantics, because it's high level enough, and it has an intermediate representation which can be trivially mapped into pretty much anything at a very little cost (because of simplicity of requirements). Why should I care about soundness of the whole mix while I can easily prove correctness of this very last step of translation, and this is enough to ensure the rest. > There are a ridiculous number of ways to combine these things in ways that totally kill type soundness, confluence, etc. Then do not combine these things in the unsound ways. As simple as that. For example, this is how I'm using Prolog embedded in an eager somewhat-functional host: the host DSL is used to define transforms over ASTs, including simple flattening transforms that derive sequences of equations (i.e., Prolog terms). Then the Prolog code is used to ask questions about these systems of equations. This way many typical internal compiler tasks are dead simple but yet reasonably efficient (and for some of the most important things I can even use Datalog instead, with all its cool optimisations). The only point where the Prolog world is interacting with the rest of the system is via these lists of equations, so I do not have to care how to reason about WAM interaction with a memory-managed eager functional semantics, all is well compartmentalised. > None of these three assumptions are true for most of the eDSLs engineers might want to write down in general. How is it so? Everything is still boiling down to one of the "fundamental" execution models. Higher level semantics are added as sequences of well-understood, provable, trivial transforms all the way down to such fundamental blocks, for which, as you said, we have at least 30-60 years worth of understanding. The very high level semantics are added independently of any fundamental blocks, with a transform to a specific execution model being added at the very last moment and it is always trivial enough. > a framework that lets you get unsound bullcrap from two perfectly sound things If the source language is sound, each of the target languages are sound, and all the transforms in between are sound, then the result is sound and robust. > isn't a solution to the (e)DSL problem In my practice it is a solution indeed. Every eDSL I design is dead simple in implementation and very rarely I have to add something new to my current toolbox. With problem domains ranging from 3D CAD applications to hardware design.
  • nmrm2 11y ago
    > And what's the problem with soundness? You can definitely not provide any guarantee for arbitrary DSLs implemented in your system, but claim you do. > I can even derive formal proofs for simple DSLs when I have too. Am I looking at the correct thing on GitHub? CombinatoryLogic? I can't find any code here that would suggest you're interfacing with a theorem prover, much less the incredibly amount of machinery that must be involved in taking two correctness proofs and producing a correctness proof for their combination. > Then do not combine these things in the unsound ways. As simple as that. I think this pretty much sums up the contribution here. It's a framework that doesn't face any problems with compositions because you've chosen not to write down things that don't compose well. > If the source language is sound, each of the target languages are sound, and all the transforms in between are sound, then the result is sound and robust. To repeat myself once again, your framework doesn't force any of these to be true. It's just as easy to write down unsound things as to write down sound things. The fact that you choose to write down sound things is nice I guess, but it's not a demonstration of the capacity of the framework or methodology to preserve soundness. It's just a demonstration of your own capabilities... we hope. That works fine and well when DSLs don't get inter-leaved in unexpected ways and are only developed by a small set of developers. But then, we've known how to design DSLs in those cases for a long time. There's no REAL composition going on -- just the sort of combination that's always happened. The actually interesting question is how to support an open world of DSLs. Where composing DSL1 with DSL2 won't break some guarantee that the writer of DSL2 worked hard to achieve. And where even changes to DSLA, which DSL2 depends on, also won't break those guarantees. And where the authors of all three languages never even know each other exist. And not just "if you don't write down the wrong thing", but "because the framework prohibits it". You don't solve this problem. In fact, I can't even figure out how to state some specification of a DSL, much less that it's preserved under a transformation... Again, your framework might be a great setting for doing DSL engineering. And I don't doubt that you designed a tool that's useful for you. But you're making some pretty extreme and apparently over-stated claims beyond "nice framework solving a few practical implementation problems". (Which is a shame because your tool seems nice, but your comments come across (to me) a bit snake-oily, so I'm not sure how seriously I should take the tool / approach. I think if you re-stated your claims so that they're a more accurate representation of the problems you do (and don't) solve, you might get a better reception.)