|
|
| Line 1: |
Line 1: |
| {{DISPLAYTITLE:<span style="position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);">{{FULLPAGENAME}}</span>}}
| | #REDIRECT [[pseudo-function]] |
| <font size="+3" face="Times New Roman">Unsafe perforatives</font>
| |
| | |
| <blockquote>
| |
| [Using the FFI] you can import any C function with a pure type, | |
| which also allows you to wreak arbitrary havoc. We enable
| |
| the user to disguise arbitrary machine code as a Haskell
| |
| function of essentially arbitrary type. In comparison,
| |
| <code>unsafePerformIO</code> seems angelic.
| |
| | |
| :<small>[[QuotesPage|Manuel Chakravarty]]</small>
| |
| </blockquote>
| |
| | |
| == 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>
| |
| | |
| == A rogues' gallery ==
| |
| | |
| These are just some of the various unsafe perforatives lurking in libraries:
| |
| | |
| * <hask>unsafeLocalState :: IO a -> a</hask>
| |
| * <hask>unsafePerformIO :: IO a -> a</hask>
| |
| * <hask>inlinePerformIO :: IO a -> a</hask>
| |
| * <hask>unsafeInterleaveIO :: IO a -> IO a</hask>
| |
| * <hask>unsafeInterleaveST :: ST s a -> ST s a</hask>
| |
| * <hask>unsafeIOToST :: IO a -> ST s a</hask>
| |
| * <hask>unsafeIOToSTM :: IO a -> STM a</hask>
| |
| * <hask>unsafeFreeze</hask>, <hask>unsafeThaw</hask>
| |
| * <hask>unsafeCoerce# :: a -> b</hask>
| |
| | |
| Unsafe perforatives can:
| |
| | |
| * break type safety (<code>unsafeCoerce#</code>, <code>unsafeLocalState</code>, <code>unsafePerformIO</code>),
| |
| | |
| * or break [https://okmij.org/ftp/Haskell/index.html#lazyIO-not-True equational reasoning] (<code>unsafeInterleaveIO</code>).
| |
| | |
| Their use would require some kind of assurance on the part of the programmer that what they're doing is safe, particularly in multithreaded programs - if they are misused in vain attempts to hide externally-visible effects the resulting code simply will not be [[pure]], whatever type it is given.
| |
| | |
| | |
| ----
| |
| <code>unsafe</code> is also a keyword which can be used in a [http://haskell.org/haskellwiki/Performance/FFI foreign import declaration].
| |
| | |
| | |
| {{stub}}
| |
| | |
| [[Category:Idioms]]
| |