hobbits-1.3.1: A library for canonically representing terms with binding
Copyright(c) 2014 Edwin Westbrook Nicolas Frisby and Paul Brauner
LicenseBSD3
Maintaineremw4@rice.edu
Stabilityexperimental
PortabilityGHC
Safe HaskellNone
LanguageHaskell2010

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

Abstract types

data Closed a Source #

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

Instances details
NuMatching (Closed a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

Closable (Closed a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: Closed a -> Closed (Closed a) Source #

Liftable (Closed a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Liftable

Methods

mbLift :: forall k (ctx :: RList k). Mb ctx (Closed a) -> Closed a Source #

Operators involving Closed

unClosed :: Closed a -> a Source #

Extract the value of a Closed object

mkClosed :: Q Exp -> Q Exp Source #

mkClosed is used with Template Haskell quotations to create closed terms of type Closed. A quoted expression is closed if all of the names occuring in it are either:

1) bound globally or 2) bound within the quotation or 3) also of type 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

Methods

toClosed :: a -> Closed a Source #

Instances

Instances details
Closable Bool Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Closable Char Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Closable Int Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: Int -> Closed Int Source #

Closable Integer Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Closable a => Closable [a] Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: [a] -> Closed [a] Source #

Closable (Closed a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: Closed a -> Closed (Closed a) Source #

Closable (Proxy a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: Proxy a -> Closed (Proxy a) Source #

ClosableAny1 f => Closable (RAssign f ctx) Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: RAssign f ctx -> Closed (RAssign f ctx) Source #

Closable (Member ctx a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: Member ctx a -> Closed (Member ctx a) Source #