Editing Unsafe functions (section)

== Definitely '''not''' functions! ==

Regarding the perforative entity <code>val execute: α Beh ⟶ α</code> for PFL+:

<blockquote>
Unfortunately <code>execute</code> is not a safe extension to a functional language because it is not unfoldable—witness the expression

<pre>
(x ⟼ x-x)(execute(i?x. Ret x))
</pre>

which unfolds to

<pre>
execute(i?x. Ret x) - execute(i?x. Ret x)
</pre>

The first executes by reading one value from channel <code>i</code>, then returning <code>0</code>; while the second reads two values from <code>i</code>, and returns their difference. The first makes one suspension, the second two.

Nor is <code>execute</code> a function; the subexpression <code>execute(i?x. Ret x)</code> can take on two different values in the expression above.

:<small>[https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-160.pdf PFL+: A Kernel Scheme for Functional I/O] (pages 15-16 of 28).</small>
</blockquote>