Portability | GHC |
---|---|
Stability | experimental |
Maintainer | emw4@rice.edu |
Safe Haskell | None |
This module uses Template Haskell to distinguish closed terms, so that the
library can trust such functions to not contain any Name
values in their
closure.
Abstract types
The type Cl a
represents a closed term of type a
,
i.e., an expression of type a
with no free (Haskell) variables.
Since this cannot be checked directly in the Haskell type system,
the Cl
data type is hidden, and the user can only create
closed terms using Template Haskell, through the mkClosed
operator.
Operators involving Cl
mbApplyCl :: Cl (a -> b) -> Mb ctx a -> Mb ctx bSource
mbApplyCl
f
b
applies a closed function f
to the body of
multi-binding b
. For example:
mbApplyCl $(cl [| f |]) (nu $ \n -> n) = nu f
mbLiftClosed :: Mb ctx (Cl a) -> Cl aSource
mbLiftClosed
is safe because closed terms don't contain names.
noClosedNames :: Cl (Name a) -> bSource
noClosedNames
encodes the hobbits guarantee that no name can escape its
multi-binding.