nominal-0.1.0.0: Binders and alpha-equivalence made easy

Safe HaskellNone
LanguageHaskell2010

Nominal.Unsafe

Description

This module provides three primitive functions that use unsafePerformIO. These functions are only safe if used correctly. How to use each function correctly is specified in its documentation.

Synopsis

Documentation

global_used :: IORef (Set String) Source #

A global variable holding a set of strings already used for free names.

The use of unsafePerformIO in this function is safe, because it is only called once and serves to create a global reference cell.

global_new_io :: NameGen -> IO String Source #

Create a globally new concrete name based on the given name suggestion. This ensures that fresh names have distinct names when they are not bound.

global_new :: NameGen -> String Source #

Create a globally new concrete name based on the given name suggestion. The use of unsafePerformIO in this function is safe if the user respects the correctness conditions associated with the function with_fresh and other analogous functions.

with_unique :: (Unique -> a) -> a Source #

Perform a subcomputation in the presence of a globally unique value. This is similar to newUnique, but uses a continuation monad instead of the IO monad. To ensure referential transparency, the unique value must not escape the function body.

The use of unsafePerformIO in this function is safe if the user respects the correctness conditions associated with the function with_fresh and other analogous functions.

unsafe_with :: IO a -> (a -> b) -> b Source #

Unsafely embed the IO monad in a continuation monad. This is in general unsafe, but can be safe for certain kinds of IO computation if the continuation satisfies a correctness condition.