On 7/18/2010 2:30 AM, joel falcou wrote: > Eric Niebler wrote: >> Joel, why write it in ML first? >> > Two reasons: > > - ML is actually my first language so I can be quite productive with it. > C++ is just my second one ;) > > - ML has a strong type checker than help you not writing erroneous > functions. > A classical thing is the match construct. > > this is a function computing the size of a list. > > let rec len x = match x with > | [] -> 0 > | x::xs -> 1 + len xs; > > it's basically a listing of alternatives depending on how you parse the > input thansk to the match ... with directive.
I'm pretty sure I understand this. I briefly looked into OCaml, so this is familiar. Are the alternates tried in order or is there some notion of "best match" like with template specialzations? > If you "forgot" a case that make the function not working, ML will > complain and in some case give you the missing case. How in the world is that computable in general? Is match...with restricted to list-like thingies? > Which means when your function is typed by ML, it has no more obvious > error and should work ;) Cool. So you're using this to validate your semantic actions? > Now, look at this again and replace let with template<class T> struct > len and match by template specialization. Bingo, you got the exact same > function turned into a meta-function. I object! The len function computes the length of a *runtime* list. Obviously with template specializations we're no longer dealing with runtime data structures. I don't see how to the two relate. > So writing ML first help us test the meta-function (usually the large, > complex meta-function we use in the semantic) with a proper level of > error detection. Afterward, the transformation is rather simple and we > know by transitivity of corretcness that the template is now working for > every case. I've planned to get students working on such ML2C++ > converter of meta-functions but never found a proper student able to > take on this task Good luck! > [Aside discussion] > That's a temporary solution though. What we may need is to have a formal > description of C++ template in HOARE logic and proven with Coq or > ISABELLE so we know when we write a template metafunction that is does > what it does in all situation. But that's one of a longer time frame > research project. And on the quesiton why do we want this ? Well, if we > prove that the C++ code generator is "correct" under some assumptions, > that this C++ generator is based upon a simpler language we can verify > and that we take for granted the C++ compiler is OK, then we have a > complete DSL -> C++ -> executable chain which is certifiable and > formally proven. In some use cases (aeronautics and such) this > provability is a requirements. > [/Aside discussion] In theory it should be possible to add a theorem prover to proto to validate semantic actions, right? Not that C++ TMP is necessarily the best tool for this. -- Eric Niebler BoostPro Computing http://www.boostpro.com _______________________________________________ proto mailing list proto@lists.boost.org http://lists.boost.org/mailman/listinfo.cgi/proto