Difference between revisions of "Unsafe functions"

From HaskellWiki
Jump to navigation Jump to search
m (Initial quote replaced)
(Some long-overdue clarification...)
Line 1: Line 1:
  +
{{DISPLAYTITLE:<span style="position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);">{{FULLPAGENAME}}</span>}}
  +
<font size="+3" face="Times New Roman">Unsafe definitions</font>
  +
 
<blockquote>
 
<blockquote>
 
[Using the FFI] you can import any C function with a pure type,
 
[Using the FFI] you can import any C function with a pure type,
Line 9: Line 12:
 
</blockquote>
 
</blockquote>
   
  +
== Definitions, '''not''' functions! ==
There are a number of '''unsafe functions''' in the libraries.
 
  +
  +
Regarding an extra primitive definition <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 definitions lurking in libraries:
   
 
* <hask>unsafeLocalState :: IO a -> a</hask>
 
* <hask>unsafeLocalState :: IO a -> a</hask>
Line 21: Line 50:
 
* <hask>unsafeCoerce# :: a -> b</hask>
 
* <hask>unsafeCoerce# :: a -> b</hask>
   
Unsafe functions can:
+
Unsafe definitions can:
   
 
* break type safety (<code>unsafeCoerce#</code>, <code>unsafeLocalState</code>, <code>unsafePerformIO</code>),
 
* break type safety (<code>unsafeCoerce#</code>, <code>unsafeLocalState</code>, <code>unsafePerformIO</code>),
Line 29: Line 58:
 
Their use would require some kind of assurance on the part of the programmer that what they're doing is safe.
 
Their use would require some kind of assurance on the part of the programmer that what they're doing is safe.
   
  +
  +
----
 
<code>unsafe</code> is also a keyword which can be used in a [http://haskell.org/haskellwiki/Performance/FFI foreign import declaration].
 
<code>unsafe</code> is also a keyword which can be used in a [http://haskell.org/haskellwiki/Performance/FFI foreign import declaration].
  +
   
 
{{stub}}
 
{{stub}}

Revision as of 22:54, 8 October 2024

Unsafe definitions

[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, unsafePerformIO seems angelic.

Manuel Chakravarty

Definitions, not functions!

Regarding an extra primitive definition val execute: α Beh ⟶ α for PFL+:

Unfortunately execute is not a safe extension to a functional language because it is not unfoldable—witness the expression

(x ⟼ x-x)(execute(i?x. Ret x))

which unfolds to

execute(i?x. Ret x) - execute(i?x. Ret x)

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

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

PFL+: A Kernel Scheme for Functional I/O (pages 15-16 of 28).

A rogues' gallery

These are just some of the various unsafe definitions lurking in libraries:

  • unsafeLocalState :: IO a -> a
  • unsafePerformIO :: IO a -> a
  • inlinePerformIO :: IO a -> a
  • unsafeInterleaveIO :: IO a -> IO a
  • unsafeInterleaveST :: ST s a -> ST s a
  • unsafeIOToST :: IO a -> ST s a
  • unsafeIOToSTM :: IO a -> STM a
  • unsafeFreeze, unsafeThaw
  • unsafeCoerce# :: a -> b

Unsafe definitions can:

  • break type safety (unsafeCoerce#, unsafeLocalState, unsafePerformIO),

Their use would require some kind of assurance on the part of the programmer that what they're doing is safe.



unsafe is also a keyword which can be used in a foreign import declaration.


This article is a stub. You can help by expanding it.