On Fri, 26 Aug 2005, Christophe Raffalli <christophe.raffalli@univ-savoie.fr> wrote:
> 
> Remark: clearly, a good proof system should not show the monadic 
> translation and hide it behind the scene ...

Shouldn't a good proof system show the code to be correct regardless
of the evaluation order of function args, records,...?  After all,
different evaluation orders may be interesting on different platforms
and I think programs that rely on the evaluation order (say) of
functions arguments to be correct are fragile -- they have a great
potential to be broken at the first maintenance.

On Fri, 26 Aug 2005, Fernando Alegre <fernando@cc.gatech.edu> wrote:
> 
> Ignoring efficiency concerns, may I suggest that the correct way to
> build lists is by appending elements, not prepending them:
> 
> # append('d', append('c', append('b', append('a', []))));;
> - : char list = ['a'; 'b'; 'c'; 'd']

It is not.  You have to respect their recursive definition, from which
it is clear that "append" is not a primitive operation.  The data
structure that you contruct with "append" and deconstruct with "head"
is a FIFO queue.

I've been skimming through the discussion and basically I do not
understand you guys who want a given evaluation order for function
application, constructors,...  First there is a way of imposing
evaluation order of expressions if you need it and moreover, you are
using a functional language which emphasizes immutability for which
evaluation order does not matter...

My 2¢,
ChriS