-- 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.0
-- | A simple parser for Haskell patterns. Currently does not handle:
--
--
-- - Record patterns Pt { pointx = x }
-- - Signature patterns p :: t
-- - View patterns e -> p
--
module Data.Binding.Hobbits.PatternParser
parsePattern :: [Char] -> Pat
parseVar :: [Char] -> String
-- | 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 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
-- | 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
-- | 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 :: [Int] -> b -> Mb ctx b
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.
combineMb :: 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.
separateMb :: 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]
instance [overlap ok] (Liftable2 f, Liftable a) => Liftable1 (f a)
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 (Name a)
-- | This module uses Template Haskell to distinguish super-combinators, so
-- that the library can trust such functions to not contain any
-- Name values in their closure.
module Data.Binding.Hobbits.SuperComb
-- | The type SuperComb a represents a super-combinator 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 SuperComb data type is hidden, and
-- the user can only create super-combinators using Template Haskell,
-- through the superComb operator.
data SuperComb a
-- | superComb is used with Template Haskell to create
-- super-combinators; see documentation for mbToplevel to see how
-- it is used.
superComb :: Q Exp -> Q Exp
-- | mbToplevel f b applies super-combinator
-- f to the body of multi-binding b. For example:
--
--
-- mbToplevel $(superComb [| f |]) (nu $ \n -> n) = nu f
--
mbToplevel :: SuperComb (a -> b) -> Mb ctx a -> Mb ctx b
-- | Defines a quasi-quoter for writing patterns that match the bodies of
-- Mb multi-bindings. Uses the
-- Data.Binding.Hobbits.PatternParser module, and thus only
-- supports the pattern forms listed there. If P is a
-- (supported) Haskell pattern, then [nuQQ| P ] defines a
-- pattern that will match an multi-binding whose body matches
-- P. Any variables matched by P will remain inside the
-- binding; thus, for example, in the pattern [nuQQ| x |],
-- x matches the entire multi-binding.
--
-- Examples:
--
--
-- case (nu Left) of [nuQQ| Left x |] -> x == nu id
--
module Data.Binding.Hobbits.QQ
nuQQ :: 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
-- | 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')
--
nuWithElimMulti :: NuElimList args => MapC f ctx -> MapC (Mb ctx) args -> (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b
-- | Similar to nuWithElimMulti but binds only one name.
nuWithElim :: NuElimList args => MapC (Mb (Nil :> a)) args -> (Name a -> MapC Identity args -> b) -> Binding a b
-- | Similar to nuWithElimMulti but takes only one argument that
-- binds a single name.
nuWithElim1 :: NuElim arg => 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 NuElimProof args
data NuElimProof a
instance (NuElimList args, NuElim a) => NuElimList (args :> a)
instance NuElimList Nil
instance (NuElim a, NuElim b) => NuElim (Either a b)
instance (NuElim a, NuElim b) => NuElim (a, b)
instance NuElim a => NuElim [a]
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 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)