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.
If you "forgot" a case that make the function not working, ML will
complain and in some case give you the missing case.
Which means when your function is typed by ML, it has no more obvious
error and should work ;)
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.
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
[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]
_______________________________________________
proto mailing list
proto@lists.boost.org
http://lists.boost.org/mailman/listinfo.cgi/proto
