Copyright	(c) 2011 Edwin Westbrook Nicolas Frisby and Paul Brauner
License	BSD3
Maintainer	emw4@rice.edu
Stability	experimental
Portability	GHC
Safe Haskell	None
Language	Haskell2010

Data.Binding.Hobbits

Contents

Values under multi-bindings
Closed terms
Pattern-matching multi-bindings and closed terms
Lifting values out of multi-bindings
Ancilliary modules

Description

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

Synopsis

module Data.Binding.Hobbits.Mb
module Data.Binding.Hobbits.Closed
module Data.Binding.Hobbits.QQ
module Data.Binding.Hobbits.Liftable
module Data.Proxy
module Data.Type.Equality
data RList a
- = RNil
- | (RList a) :> a
data RAssign (f :: k -> *) (c :: RList k) where
- MNil :: RAssign f RNil
- (:>:) :: RAssign f c -> f a -> RAssign f (c :> a)
data Member (ctx :: RList k1) (a :: k2) where
- Member_Base :: Member (ctx :> a) a
- Member_Step :: Member ctx a -> Member (ctx :> b) a
type family (r1 :: RList k) :++: (r2 :: RList k) :: RList k
data Append ctx1 ctx2 ctx where
- Append_Base :: Append ctx RNil ctx
- Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
module Data.Binding.Hobbits.NuMatching

Values under multi-bindings

module Data.Binding.Hobbits.Mb

The Mb type modeling multi-bindings is the central abstract type of the library

Closed terms

module Data.Binding.Hobbits.Closed

The Cl type models super-combinators, which are safe functions to apply under Mb.

Pattern-matching multi-bindings and closed terms

module Data.Binding.Hobbits.QQ

The nuP quasiquoter allows safe pattern matching on Mb values. superCombP is similar.

Lifting values out of multi-bindings

module Data.Binding.Hobbits.Liftable

Ancilliary modules

module Data.Proxy

module Data.Type.Equality

Type lists track the types of bound variables.

data RList a Source #

A form of lists where elements are added to the right instead of the left

Constructors

RNil
(RList a) :> a

data RAssign (f :: k -> *) (c :: RList k) where Source #

An RAssign f r an assignment of an f a for each a in the RList r

Constructors

MNil :: RAssign f RNil
(:>:) :: RAssign f c -> f a -> RAssign f (c :> a)

Instances

Instances details

Show (RAssign (Name :: k -> Type) c) Source #
Instance details Defined in Data.Binding.Hobbits.Internal.Name Methods showsPrec :: Int -> RAssign Name c -> ShowS # show :: RAssign Name c -> String # showList :: [RAssign Name c] -> ShowS #
NuMatchingAny1 f => NuMatching (RAssign f ctx) Source #
Instance details Defined in Data.Binding.Hobbits.NuMatching Methods nuMatchingProof :: MbTypeRepr (RAssign f ctx) 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 #

data Member (ctx :: RList k1) (a :: k2) where Source #

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.

Constructors

Member_Base :: Member (ctx :> a) a
Member_Step :: Member ctx a -> Member (ctx :> b) a

Instances

Instances details

TestEquality (Member ctx :: k -> Type) Source #
Instance details Defined in Data.Type.RList Methods testEquality :: forall (a :: k0) (b :: k0). Member ctx a -> Member ctx b -> Maybe (a :~: b) #
Eq (Member ctx a) Source #
Instance details Defined in Data.Type.RList Methods (==) :: Member ctx a -> Member ctx a -> Bool # (/=) :: Member ctx a -> Member ctx a -> Bool #
Show (Member r a) Source #
Instance details Defined in Data.Type.RList Methods showsPrec :: Int -> Member r a -> ShowS # show :: Member r a -> String # showList :: [Member r a] -> ShowS #
NuMatching (Member ctx a) Source #
Instance details Defined in Data.Binding.Hobbits.NuMatchingInstances Methods nuMatchingProof :: MbTypeRepr (Member ctx a) Source #
Closable (Member ctx a) Source #
Instance details Defined in Data.Binding.Hobbits.Closed Methods toClosed :: Member ctx a -> Closed (Member ctx a) Source #
Liftable (Member c a) Source #
Instance details Defined in Data.Binding.Hobbits.Liftable Methods mbLift :: forall k (ctx :: RList k). Mb ctx (Member c a) -> Member c a Source #

type family (r1 :: RList k) :++: (r2 :: RList k) :: RList k infixr 5 Source #

Append two RLists at the type level

Instances

Instances details

type (r :: RList k) :++: ('RNil :: RList k) Source #
Instance details Defined in Data.Type.RList type (r :: RList k) :++: ('RNil :: RList k) = r
type (r1 :: RList a1) :++: (r2 :> a2 :: RList a1) Source #
Instance details Defined in Data.Type.RList type (r1 :: RList a1) :++: (r2 :> a2 :: RList a1) = (r1 :++: r2) :> a2

data Append ctx1 ctx2 ctx where Source #

An Append ctx1 ctx2 ctx is a "proof" that ctx = ctx1 :++: ctx2.

Constructors

Append_Base :: Append ctx RNil ctx
Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)

The Data.Binding.Hobbits.NuMatching module exposes the NuMatching class, which allows pattern-matching on (G)ADTs in the bodies of multi-bindings

module Data.Binding.Hobbits.NuMatching