Copyright | (c) 2014 Edwin Westbrook Nicolas Frisby and Paul Brauner |
---|---|

License | BSD3 |

Maintainer | emw4@rice.edu |

Stability | experimental |

Portability | GHC |

Safe Haskell | None |

Language | Haskell98 |

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.

- data Closed a
- unClosed :: Closed a -> a
- mkClosed :: Q Exp -> Q Exp
- noClosedNames :: Closed (Name a) -> b
- clApply :: Closed (a -> b) -> Closed a -> Closed b
- clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) -> Closed (Mb ctx b)
- clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b
- class Closable a where

# Abstract types

The type `Closed 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 `Closed`

data type is hidden, and the
user can only create closed terms using Template Haskell, through the `mkClosed`

operator.

# Operators involving `Closed`

noClosedNames :: Closed (Name a) -> b Source #

`noClosedNames`

encodes the hobbits guarantee that no name can escape its
multi-binding.

clApply :: Closed (a -> b) -> Closed a -> Closed b Source #

Closed terms are closed (sorry) under application.

clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) -> Closed (Mb ctx b) Source #

Closed multi-bindings are also closed under application.

clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b Source #

When applying a closed function, the argument can be viewed as locally closed