Data.Binding.Hobbits.Mb

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.

Abstract types

data Name (a :: k)

A Name a is a bound name that is associated with type a.

Instances

TestEquality (Name :: k -> Type)

Defined in Data.Binding.Hobbits.Internal.Name

Methods

testEquality :: Name a -> Name b -> Maybe (a :~: b)

NuMatchingAny1 (Name :: k -> Type)

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingAny1Proof :: MbTypeRepr (Name a)

Eq (Name a)

Defined in Data.Binding.Hobbits.Internal.Name

Methods

(==) :: Name a -> Name a -> Bool

(/=) :: Name a -> Name a -> Bool

Ord (Name a)

Defined in Data.Binding.Hobbits.Internal.Name

Methods

compare :: Name a -> Name a -> Ordering

(<) :: Name a -> Name a -> Bool

(<=) :: Name a -> Name a -> Bool

(>) :: Name a -> Name a -> Bool

(>=) :: Name a -> Name a -> Bool

max :: Name a -> Name a -> Name a

min :: Name a -> Name a -> Name a

Show (Name a)

Defined in Data.Binding.Hobbits.Internal.Name

Methods

showsPrec :: Int -> Name a -> ShowS

show :: Name a -> String

showList :: [Name a] -> ShowS

NuMatching (Name a)

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingProof :: MbTypeRepr (Name a)

Show (RAssign (Name :: k -> Type) c)

Defined in Data.Binding.Hobbits.Internal.Name

Methods

showsPrec :: Int -> RAssign Name c -> ShowS

show :: RAssign Name c -> String

showList :: [RAssign Name c] -> ShowS

type Binding (a :: k) = Mb (RNil :> a)

A Binding is simply a multi-binding that binds one name

data Mb (ctx :: RList k) b

An Mb ctx b is a multi-binding that binds one name for each type in ctx, where ctx has the form RNil :> t1 :> ... :> tn. Internally, multi-bindings are represented either as "fresh functions", which are functions that quantify over all fresh names that have not been used before and map them to the body of the binding, or as "fresh pairs", which are pairs of a list of names that are guaranteed to be fresh along with a body. Note that fresh pairs must come with an MbTypeRepr for the body type, to ensure that the names given in the pair can be relaced by fresher names.

Instances

Functor (Mb ctx)

Defined in Data.Binding.Hobbits.Mb

Methods

fmap :: (a -> b) -> Mb ctx a -> Mb ctx b

(<$) :: a -> Mb ctx b -> Mb ctx a

TypeCtx ctx => Applicative (Mb ctx)

Defined in Data.Binding.Hobbits.Mb

Methods

pure :: a -> Mb ctx a

(<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b

liftA2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c

(*>) :: Mb ctx a -> Mb ctx b -> Mb ctx b

(<*) :: Mb ctx a -> Mb ctx b -> Mb ctx a

Eq a => Eq (Mb ctx a)

Defined in Data.Binding.Hobbits.Liftable

Methods

(==) :: Mb ctx a -> Mb ctx a -> Bool

(/=) :: Mb ctx a -> Mb ctx a -> Bool

Show a => Show (Mb c a)

Defined in Data.Binding.Hobbits.Mb

Methods

showsPrec :: Int -> Mb c a -> ShowS

show :: Mb c a -> String

showList :: [Mb c a] -> ShowS

NuMatching a => NuMatching (Mb ctx a)

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingProof :: MbTypeRepr (Mb ctx a)

Multi-binding constructors

nu :: forall (a :: k1) (b :: *). (Name a -> b) -> Binding a b

nu f creates a binding which binds a fresh name n and whose body is the result of f n.

nuMulti :: RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b

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 RAssign 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.

nus :: RAssign f ctx -> (RAssign (Name :: k -> Type) ctx -> b) -> Mb ctx b

nus = nuMulti

emptyMb :: a -> Mb RNil a

Creates an empty binding that binds 0 names.

extMb :: Mb ctx a -> Mb (ctx :> tp) a

Extend the context of a name-binding by adding a single type

extMbMulti :: RAssign f ctx2 -> Mb ctx1 a -> Mb (ctx1 :++: ctx2) a

Extend the context of a name-binding with multiple types

Queries on names

cmpName :: Name a -> Name b -> Maybe (a :~: b)

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

hcmpName :: forall (a :: k1) (b :: k2). Name a -> Name b -> Maybe (a :~~: b)

Heterogeneous comparison of names, that could be at different kinds

mbNameBoundP :: forall (a :: k1) (ctx :: RList k2). Mb ctx (Name a) -> Either (Member ctx a) (Name a)

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

mbCmpName :: forall (a :: k1) (b :: k1) (c :: RList k2). Mb c (Name a) -> Mb c (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.

Operations on multi-bindings

elimEmptyMb :: Mb RNil a -> a

Eliminates an empty binding, returning its body. Note that elimEmptyMb is the inverse of emptyMb.

mbCombine :: forall (c1 :: RList k) (c2 :: RList k) a b. Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b

Combines a binding inside another binding into a single binding.

mbSeparate :: forall (ctx1 :: RList k) (ctx2 :: RList k) (any :: k -> *) a. RAssign any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a)

Separates a binding into two nested bindings. The first argument, of type RAssign any c2, is a "phantom" argument to indicate how the context c should be split.

mbToProxy :: forall (ctx :: RList k) (a :: *). Mb ctx a -> RAssign Proxy ctx

Returns a proxy object that enumerates all the types in ctx.

mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)

Take a multi-binding inside another multi-binding and move the outer binding inside the ineer one.

mbPure :: RAssign f ctx -> a -> Mb ctx a

Put a value inside a multi-binding

mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b

Applies a function in a multi-binding to an argument in a multi-binding that binds the same number and types of names.

mbMap2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c

Lift a binary function function to Mbs

Eliminators for multi-bindings

nuMultiWithElim :: (RAssign Name ctx -> RAssign Identity args -> b) -> RAssign (Mb ctx) args -> Mb ctx b

asdfasdf

The expression nuWithElimMulti args f takes a sequence args of one or more multi-bindings (it is a runtime error to pass an empty sequence of arguments), 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.

For example, here is an alternate way to implement mbApply:

mbApply' :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbApply' f a =
    nuWithElimMulti ('MNil' :>: f :>: a)
                    (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')

nuWithElim :: (Name a -> RAssign Identity args -> b) -> RAssign (Mb (RNil :> a)) args -> Binding a b

Similar to nuMultiWithElim but binds only one name. Note that the argument list here is allowed to be empty.

nuMultiWithElim1 :: (RAssign Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b

Similar to nuMultiWithElim but takes only one argument

nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b

Similar to nuMultiWithElim but takes only one argument that binds a single name.

Orphan instances

Functor (Mb ctx)

Methods

fmap :: (a -> b) -> Mb ctx a -> Mb ctx b

(<$) :: a -> Mb ctx b -> Mb ctx a

TypeCtx ctx => Applicative (Mb ctx)

Methods

pure :: a -> Mb ctx a

(<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b

liftA2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c

(*>) :: Mb ctx a -> Mb ctx b -> Mb ctx b

(<*) :: Mb ctx a -> Mb ctx b -> Mb ctx a

Show a => Show (Mb c a)

Methods

showsPrec :: Int -> Mb c a -> ShowS

show :: Mb c a -> String

showList :: [Mb c a] -> ShowS