The Coq mailing list

[roconnor AT theorem.ca]

One of the nicest things about programing in Coq, is that you never need
to have your functions produce garbage output in cases that are either
impossible, or outside the domain of the function.  One can use False_rec
in these branches and prove the branch is impossible.

But such a programming style does not play well with Coq's compute, or
call-by-value evaluation order.  Whenever proof objects are mixed in with
data, call-by-value evaluation order slows to a crawl.  This is
presumably because call-by-value is trying to normalize the proof objects.
This process is slow, and the proof object are almost never used in the
evaluation.

I understand the new virtual machine will use call-by-value, and
presumably suffer from the same problems.  This will put pressure on
developers to separate proofs objects from functions, and result in
developers putting garbage values inside functions.

Couldn't we have the best of both call-by-value, and lazy evaluation?  How
about a reduction scheme that is strict on the part of the terms that live
in the Set world, and lazy on the part of the terms that live in the Prop
world?  So function parameters would be normalized only if they are inside
Set, otherwise they remain as an unevaluated thunk.  Some care would be
needed so that x : {A}+{B} is only evaluated until (left [thunk]) or
(right [thunk]) is reached, and the thunk remains unevaluated.

What do people think?  Can this sort of thing be done?  Is it a good idea?

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''