Proto for Boost mailing list page: Re: [proto] talking proto

Subject: Re: [proto] talking proto
From: joel falcou (joel.falcou_at_[hidden])
Date: 2010-07-18 13:55:34

> 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?
>   
There is a funky algorithm to do this quite fast
>> 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?
>   
Nope. The typer "tries" to help you by giving you an example of missing 
stuff.
If it can't he just say "missing match cases dude"

> Cool. So you're using this to validate your semantic actions?
>   
to debug them in a friendly environment ;)
>> 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.
>   
Runtime values in ML <-> Compile-time value in C++ TMP
A function in ML operatirng on list of values becomes a meta-funtion in 
C++ operating on types list.
Both languages beign pure and functionnal helps the transition.

Just make a ML compound type like

type Type = f of Float | d of Double | i of Integer;

and let's have a polymorphic list of Type.

let l = len [ Float; Flaot; Double ];

see where we're going ?

> Good luck!
>   
The stuff is pretty much here. Need some sla... students to do the work ;)
> 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.
>   
I think it's better as an outside tools. However, a DSL for HOARE logic 
injection in C++ is another beast ;)