| Copyright | (c) 2014 Edwin Westbrook Nicolas Frisby and Paul Brauner |
|---|---|
| License | BSD3 |
| Maintainer | emw4@rice.edu |
| Stability | experimental |
| Portability | GHC |
| Safe Haskell | None |
| Language | Haskell2010 |
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.
Synopsis
- 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
- unsafeClose :: a -> Closed a
- 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.
Instances
| NuMatching (Closed a) Source # | |
Defined in Data.Binding.Hobbits.NuMatching Methods nuMatchingProof :: MbTypeRepr (Closed a) Source # | |
| Closable (Closed a) Source # | |
| Liftable (Closed a) Source # | |
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
unsafeClose :: a -> Closed a Source #
Mark an object as closed without actually traversing it. This is unsafe if the object does in fact contain any names.
Typeclass for inherently closed types
class Closable a where Source #
Typeclass for inherently closed types
Instances
| Closable Bool Source # | |
| Closable Char Source # | |
| Closable Int Source # | |
| Closable Integer Source # | |
| Closable a => Closable [a] Source # | |
Defined in Data.Binding.Hobbits.Closed | |
| Closable (Closed a) Source # | |
| Closable (Proxy a) Source # | |
| ClosableAny1 f => Closable (RAssign f ctx) Source # | |
| Closable (Member ctx a) Source # | |