| 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 |
Data.Binding.Hobbits.Closed
Description
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