-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A library for canonically representing terms with binding
--
-- A library for canonically representing terms with binding via a
-- constructor for introducing fresh names and a restricted API that
-- avoids the need for alpha-equivalence.
@package hobbits
@version 1.1
-- | Using the haskell-src-meta package to parse Haskell patterns.
module Data.Binding.Hobbits.PatternParser
parsePattern :: String -> String -> Either String Pat
-- | The type-level constructors of type lists.
module Data.Type.List.List
data Nil
data (:>) r a
proxyCons :: Proxy r -> f a -> Proxy (r :> a)
instance Typeable Nil
instance Typeable2 :>
-- | Proofs regarding a type list as an append of two others.
module Data.Type.List.Proof.Append
-- | An Append ctx1 ctx2 ctx is a "proof" that ctx = ctx1
-- :++: ctx2.
data Append ctx1 ctx2 ctx
Append_Base :: Append ctx Nil ctx
Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
-- | Appends two Append proofs.
trans :: Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx
-- | Returns a proof that ctx :=: ctx1 :++: ctx2
appendPf :: Append ctx1 ctx2 ctx -> (ctx :=: (ctx1 :++: ctx2))
-- | Returns the length of an Append proof.
length :: Append ctx1 ctx2 ctx3 -> Int
-- | Proofs regarding membership of a type in a type list.
module Data.Type.List.Proof.Member
-- | A Member ctx a is a "proof" that the type a is in
-- the type list ctx, meaning that ctx equals
--
--
-- t0 ':>' a ':>' t1 ':>' ... ':>' tn
--
--
-- for some types t0,t1,...,tn.
data Member ctx a
Member_Base :: Member (ctx :> a) a
Member_Step :: Member ctx a -> Member (ctx :> b) a
toEq :: Member (Nil :> a) b -> b :=: a
weakenL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
same :: Member r a -> Member r b -> Maybe (a :=: b)
weakenR :: Member r1 a -> Append r1 r2 r -> Member r a
split :: Append r1 r2 r -> Member r a -> Either (Member r1 a) (Member r2 a)
instance Typeable2 Member
instance Show (Member r a)
-- | Vectors indexed by a type list
module Data.Type.List.Map
-- | A MapC f c is a vector with exactly one element of type f
-- a for each type a in the type list c.
data MapC f c
Nil :: MapC f Nil
(:>) :: MapC f c -> f a -> MapC f (c :> a)
-- | Create an empty MapC vector.
empty :: MapC f Nil
-- | Create a singleton MapC vector.
singleton :: f a -> MapC f (Nil :> a)
-- | Look up an element of a MapC vector using a Member
-- proof.
lookup :: Member c a -> MapC f c -> f a
-- | Map a function to all elements of a MapC vector.
mapC :: (forall x. f x -> g x) -> MapC f c -> MapC g c
-- | Map a binary function to all pairs of elements of two MapC
-- vectors.
mapC2 :: (forall x. f x -> g x -> h x) -> MapC f c -> MapC g c -> MapC h c
-- | Append two MapC vectors.
append :: MapC f c1 -> MapC f c2 -> MapC f (c1 :++: c2)
-- | Make an Append proof from any MapC vector for the second
-- argument of the append.
mkAppend :: MapC f c2 -> Append c1 c2 (c1 :++: c2)
-- | A version of mkAppend that takes in a Proxy argument.
mkMonoAppend :: Proxy c1 -> MapC f c2 -> Append c1 c2 (c1 :++: c2)
-- | Split a MapC vector into two pieces.
split :: Append c1 c2 c -> MapC f c -> (MapC f c1, MapC f c2)
-- | Create a Proxy object for the type list of a MapC
-- vector.
proxy :: MapC f c -> Proxy c
-- | Create a vector of proofs that each type in c is a
-- Member of c.
members :: MapC f c -> MapC (Member c) c
-- | Replace a single element of a MapC vector.
replace :: MapC f c -> Member c a -> f a -> MapC f c
-- | A type list contains types as elements. We use GADT proofs
-- terms to establish membership and append relations. A
-- Data.Type.List.Map.MapC f is a vector indexed by a
-- type list, where f :: * -> * is applied to each type
-- element.
module Data.Type.List
-- | This module is internal to the Hobbits library, and should not be used
-- directly.
module Data.Binding.Hobbits.Internal
-- | A Name a is a bound name that is associated with type
-- a.
newtype Name a
MkName :: Int -> Name a
-- | An Mb ctx b is a multi-binding that binds exactly one name
-- for each type in ctx, where ctx has the form
-- Nil :> t1 :> ... :> tn.
data Mb ctx b
MkMb :: (MapC Name ctx) -> b -> Mb ctx b
-- | 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.
newtype Cl a
Cl :: a -> Cl a
unCl :: Cl a -> a
data ExMember
ExMember :: Member c a -> ExMember
memberFromLen :: Int -> ExMember
unsafeLookupC :: Int -> Member c a
data ExProxy
ExProxy :: MapC Proxy ctx -> ExProxy
proxyFromLen :: Int -> ExProxy
unsafeProxyFromLen :: Int -> MapC Proxy ctx
unsafeNamesFromInts :: [Int] -> MapC Name ctx
counter :: IORef Int
fresh_name :: a -> Int
instance Typeable1 Name
instance Typeable2 Mb
instance Eq (Name a)
-- | This module defines multi-bindings as the type Mb, as well as a
-- number of operations on multi-bindings. See the paper E. Westbrook, N.
-- Frisby, P. Brauner, "Hobbits for Haskell: A Library for Higher-Order
-- Encodings in Functional Programming Languages" for more information.
module Data.Binding.Hobbits.Mb
-- | A Name a is a bound name that is associated with type
-- a.
data Name a
-- | A Binding is simply a multi-binding that binds one name
type Binding a = Mb (Nil :> a)
-- | An Mb ctx b is a multi-binding that binds exactly one name
-- for each type in ctx, where ctx has the form
-- Nil :> t1 :> ... :> tn.
data Mb ctx b
-- | nu f creates a binding which binds a fresh name n
-- and whose body is the result of f n.
nu :: (Name a -> b) -> Binding a b
-- | Creates an empty binding that binds 0 names.
emptyMb :: a -> Mb Nil a
-- | The expression nuMulti p f creates a multi-binding of zero or
-- more names, one for each element of the vector p. The bound
-- names are passed the names to f, which returns the body of
-- the multi-binding. The argument p, of type Mb f
-- ctx, acts as a "phantom" argument, used to reify the list of
-- types ctx at the term level; thus it is unimportant what the
-- type function f is.
nuMulti :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b
-- | Eliminates an empty binding, returning its body. Note that
-- elimEmptyMb is the inverse of emptyMb.
elimEmptyMb :: Mb Nil a -> a
-- | Combines a binding inside another binding into a single binding.
mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
-- | Separates a binding into two nested bindings. The first argument, of
-- type Append c1 c2 c, is a "phantom" argument to
-- indicate how the context c should be split.
mbSeparate :: Append c1 c2 c -> Mb c a -> Mb c1 (Mb c2 a)
-- | Returns a proxy object that enumerates all the types in ctx.
mbToProxy :: Mb ctx a -> MapC Proxy ctx
-- | cmpName n m compares names n and m of types
-- Name a and Name b, respectively. When they are
-- equal, Some e is returned for e a proof of type
-- a :=: b that their types are equal. Otherwise, None
-- is returned.
--
-- For example:
--
--
-- nu $ \n -> nu $ \m -> cmpName n n == nu $ \n -> nu $ \m -> Some Refl
-- nu $ \n -> nu $ \m -> cmpName n m == nu $ \n -> nu $ \m -> None
--
cmpName :: Name a -> Name b -> Maybe (a :=: b)
-- | Compares two names inside bindings, taking alpha-equivalence into
-- account; i.e., if both are the ith name, or both are the same
-- name not bound in their respective multi-bindings, then they compare
-- as equal. The return values are the same as for cmpName, so
-- that Some Refl is returned when the names are equal and
-- Nothing is returned when they are not.
mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :=: b)
-- | Checks if a name is bound in a multi-binding, returning Left
-- mem when the name is bound, where mem is a proof that
-- the type of the name is in the type list for the multi-binding, and
-- returning Right n when the name is not bound, where
-- n is the name.
--
-- For example:
--
--
-- nu $ \n -> mbNameBoundP (nu $ \m -> m) == nu $ \n -> Left Member_Base
-- nu $ \n -> mbNameBoundP (nu $ \m -> n) == nu $ \n -> Right n
--
mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
-- | The class Liftable a gives a "lifting function" for a, which
-- can take any data of type a out of a multi-binding of type
-- Mb ctx a.
class Liftable a
mbLift :: Liftable a => Mb ctx a -> a
-- | The class Liftable1 f gives a lifting function for each type
-- f a when a itself is Liftable.
class Liftable1 f
mbLift1 :: (Liftable1 f, Liftable a) => Mb ctx (f a) -> f a
-- | The class Liftable2 f gives a lifting function for each type
-- f a b when a and b are Liftable.
class Liftable2 f
mbLift2 :: (Liftable2 f, Liftable a, Liftable b) => Mb ctx (f a b) -> f a b
-- | Lift a list (but not its elements) out of a multi-binding
mbList :: Mb c [a] -> [Mb c a]
-- |
-- nus = nuMulti
--
nus :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b
instance [overlap ok] (Liftable2 f, Liftable a) => Liftable1 (f a)
instance [overlap ok] Liftable1 []
instance [overlap ok] (Liftable1 f, Liftable a) => Liftable (f a)
instance [overlap ok] Liftable (Member c a)
instance [overlap ok] Liftable Char
instance [overlap ok] Liftable Int
instance [overlap ok] Show a => Show (Mb c a)
instance [overlap ok] Show (MapC Name c)
instance [overlap ok] Show (Name a)
-- | Defines a quasi-quoter for writing patterns that match the bodies of
-- Mb multi-bindings. Uses the haskell-src-exts parser. [nuP|
-- P ] defines a pattern that will match a multi-binding whose body
-- matches P. Any variables matched by P will remain
-- inside the binding; thus, for example, in the pattern [nuP| x
-- |], x matches the entire multi-binding.
--
-- Examples:
--
--
-- case (nu Left) of [nuP| Left x |] -> x == nu id
--
--
--
-- - clP| P | does the same for the Cl type, and [clNuP| P |]
-- works for both simultaneously: Cl (Mb ctx a).
--
module Data.Binding.Hobbits.QQ
nuP :: QuasiQuoter
clP :: QuasiQuoter
clNuP :: QuasiQuoter
-- | This module defines the NuElim typeclass, which allows eliminations of
-- (multi-) bindings. The high-level idea is that, when a fresh name is
-- created with nu, the fresh name can also be substituted for the
-- bound name in a binding. See the documentation for nuWithElim1
-- and nuWithElimMulti for details.
module Data.Binding.Hobbits.NuElim
-- | Applies a function in a multi-binding to an argument in a
-- multi-binding that binds the same number and types of names.
mbApply :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbMapAndSwap :: NuElim a => (Mb ctx1 a -> b) -> Mb ctx1 (Mb ctx2 a) -> Mb ctx2 b
-- | Take a multi-binding inside another multi-binding and move the outer
-- binding inside the inner one.
mbRearrange :: NuElim a => Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
-- | The expression nuWithElimMulti args f takes a sequence
-- args of zero or more multi-bindings, each of type Mb ctx
-- ai for the same type context ctx of bound names, and a
-- function f and does the following:
--
--
-- - Creates a multi-binding that binds names n1,...,nn, one
-- name for each type in ctx;
-- - Substitutes the names n1,...,nn for the names bound by
-- each argument in the args sequence, yielding the bodies of
-- the args (using the new name n); and then
-- - Passes the sequence n1,...,nn along with the result of
-- substituting into args to the function f, which then
-- returns the value for the newly created binding.
--
--
-- Note that the types in args must each have a NuElim
-- instance; this is represented with the NuElimList type class.
--
-- Here are some examples:
--
--
-- commuteFun :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
-- commuteFun f a =
-- nuWithElimMulti ('mbToProxy' f) ('Nil' :> f :> a)
-- (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')
--
nuMultiWithElim :: (NuElimList args, NuElim b) => MapC f ctx -> MapC (Mb ctx) args -> (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b
-- | Similar to nuMultiWithElim but binds only one name.
nuWithElim :: (NuElimList args, NuElim b) => MapC (Mb (Nil :> a)) args -> (Name a -> MapC Identity args -> b) -> Binding a b
-- | Similar to nuMultiWithElim but takes only one argument
nuMultiWithElim1 :: (NuElim arg, NuElim b) => MapC f ctx -> Mb ctx arg -> (MapC Name ctx -> arg -> b) -> Mb ctx b
-- | Similar to nuMultiWithElim but takes only one argument that
-- binds a single name.
nuWithElim1 :: (NuElim arg, NuElim b) => Binding a arg -> (Name a -> arg -> b) -> Binding a b
-- | Instances of the NuElim a class allow the type a to
-- be used with nuWithElimMulti and nuWithElim1. The
-- structure of this class is mostly hidden from the user; see
-- mkNuElimData to see how to create instances of the
-- NuElim class.
class NuElim a
nuElimProof :: NuElim a => NuElimProof a
-- | Template Haskell function for creating NuElim instances for (G)ADTs.
-- Typical usage is to include the following line in the source file for
-- (G)ADT T (here assumed to have two type arguments):
--
--
-- $(mkNuElimData [t| forall a b . T a b |])
--
--
-- The mkNuElimData call here will create an instance declaration
-- for NuElim (T a b). It is also possible to include a
-- context in the forall type; for example, if we define the ID
-- data type as follows:
--
--
-- data ID a = ID a
--
--
-- then we can create a NuElim instance for it like this:
--
--
-- $( mkNuElimData [t| NuElim a => ID a |])
--
--
-- Note that, when a context is included, the Haskell parser will add the
-- forall a for you.
mkNuElimData :: Q Type -> Q [Dec]
class NuElimList args
nuElimListProof :: NuElimList args => MapC NuElimObj args
class NuElim1 f
nuElimProof1 :: (NuElim1 f, NuElim a) => NuElimObj (f a)
data NuElimProof a
instance (NuElim1 f, NuElimList ctx) => NuElim (MapC f ctx)
instance (NuElimList args, NuElim a) => NuElimList (args :> a)
instance NuElimList Nil
instance NuElim a => NuElim [a]
instance (NuElim a, NuElim b) => NuElim (Either a b)
instance (NuElim a, NuElim b, NuElim c, NuElim d) => NuElim (a, b, c, d)
instance (NuElim a, NuElim b, NuElim c) => NuElim (a, b, c)
instance (NuElim a, NuElim b) => NuElim (a, b)
instance NuElim Char
instance NuElim Int
instance NuElim a => NuElim (Mb ctx a)
instance (NuElim a, NuElim b) => NuElim (a -> b)
instance NuElim (Name a)
-- | 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.
module Data.Binding.Hobbits.Closed
-- | 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.
data Cl a
-- | 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.
cl :: Q Exp -> Q Exp
-- | Closed terms are closed (sorry) under application.
clApply :: Cl (a -> b) -> Cl a -> Cl b
unCl :: Cl a -> a
-- | 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
--
mbApplyCl :: Cl (a -> b) -> Mb ctx a -> Mb ctx b
-- | mbLiftClosed is safe because closed terms don't contain
-- names.
mbLiftClosed :: Mb ctx (Cl a) -> Cl a
-- | noClosedNames encodes the hobbits guarantee that no name can
-- escape its multi-binding.
noClosedNames :: Cl (Name a) -> b
-- |
-- mkClosed = cl
--
mkClosed :: Q Exp -> Q Exp
-- |
-- Closed = Cl
--
type Closed = Cl
-- |
-- unClosed = unCl
--
unClosed :: Cl a -> a
-- | This library implements multi-bindings as described in the paper E.
-- Westbrook, N. Frisby, P. Brauner, "Hobbits for Haskell: A Library for
-- Higher-Order Encodings in Functional Programming Languages".
module Data.Binding.Hobbits
module Data.Binding.Hobbits.Examples.LambdaLifting.Terms
data L a
data D a
data Term :: * -> *
Var :: Name (L a) -> Term a
Lam :: Binding (L b) (Term a) -> Term (b -> a)
App :: Term (b -> a) -> Term b -> Term a
lam :: (Term a -> Term b) -> Term (a -> b)
data DTerm :: * -> *
TVar :: Name (L a) -> DTerm a
TDVar :: Name (D a) -> DTerm a
TApp :: DTerm (a -> b) -> DTerm a -> DTerm b
data Decl :: * -> *
Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)
Decl_Cons :: Binding (L a) (Decl b) -> Decl (a -> b)
data Decls :: * -> *
Decls_Base :: DTerm a -> Decls a
Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a
instance Show (Decls a)
instance Show (DTerm a)
instance Show (Term a)
module Data.Binding.Hobbits.Examples.LambdaLifting.Examples
ex1 :: Term ((b1 -> b) -> b1 -> b)
ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)
ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)
ex4 :: Term (((b1 -> b) -> b2 -> b) -> (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1)
ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)
ex6 :: Binding (L ((b -> b) -> a)) (Term a)
ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))
exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)
-- | The lambda lifting example from the paper E. Westbrook, N. Frisby, P.
-- Brauner, "Hobbits for Haskell: A Library for Higher-Order Encodings in
-- Functional Programming Languages".
module Data.Binding.Hobbits.Examples.LambdaLifting
lambdaLift :: Term a -> Decls a
mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)