On Tue, Dec 19, 2006 at 08:57:33PM +0000, Neil Mitchell wrote:
I don't know if any actual language does this,
What, that is strict and would like to inline things for performance? There is a reason they can't do this.
I had intended for that to apply to my proposal - I know real strict languages have inlining issues.
but your inlining problem can be solved by letting _|_ = arbitrary behaivor.
So would you allow folding? (inlining = unfolding) i.e. replacing defined behaviour with _|_?
And how many equational reasoning steps do you have to go, before your program is totally different?
In my idea, the rule: forall a. _|_ -> a only works forward - so you can turn a program that fails into a program that fails silently, but a working program must stay a working program. This was intended to make optimizing compilation easier, human equational reasoners would not be the intended beneficiaries. This proposal effectively allows a compiler to assume that a program will terminate successfully; a strictly weaker set of deduction rules would correspond to leaving evaluation order unspecified. I apologize for the unclearness. Stefan