Data.Binding.Hobbits

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

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

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

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

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

NuMatchingAny1 f => NuMatching (RAssign f ctx)

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingProof :: MbTypeRepr (RAssign f ctx)

ClosableAny1 f => Closable (RAssign f ctx)

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: RAssign f ctx -> Closed (RAssign f ctx)

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

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

TestEquality (Member ctx :: k -> Type)

Defined in Data.Type.RList

Methods

testEquality :: Member ctx a -> Member ctx b -> Maybe (a :~: b)

Eq (Member ctx a)

Defined in Data.Type.RList

Methods

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

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

Show (Member r a)

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)

Defined in Data.Binding.Hobbits.NuMatchingInstances

Methods

nuMatchingProof :: MbTypeRepr (Member ctx a)

Closable (Member ctx a)

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: Member ctx a -> Closed (Member ctx a)

Liftable (Member c a)

Defined in Data.Binding.Hobbits.Liftable

Methods

mbLift :: Mb ctx (Member c a) -> Member c a

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

Append two RLists at the type level

Instances

type (r :: RList k) :++: (RNil :: RList k)

Defined in Data.Type.RList

type (r :: RList k) :++: (RNil :: RList k) = r

type (r1 :: RList a1) :++: (r2 :> a2 :: RList a1)

Defined in Data.Type.RList

type (r1 :: RList a1) :++: (r2 :> a2 :: RList a1) = (r1 :++: r2) :> a2

data Append ctx1 ctx2 ctx where

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