hobbits-1.1: A library for canonically representing terms with binding

Safe HaskellNone




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

data Cl a Source

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

cl :: Q Exp -> Q ExpSource

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

1) bound globally or 2) bound within the quotation or 3) also of type Cl.

clApply :: Cl (a -> b) -> Cl a -> Cl bSource

Closed terms are closed (sorry) under application.

unCl :: Cl a -> aSource

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.


mkClosed :: Q Exp -> Q ExpSource

mkClosed = cl

type Closed = ClSource

Closed = Cl

unClosed :: Cl a -> aSource

unClosed = unCl