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.