hobbits-1.3.1: A library for canonically representing terms with binding
Copyright(c) 2011 Edwin Westbrook Nicolas Frisby and Paul Brauner
LicenseBSD3
Maintaineremw4@rice.edu
Stabilityexperimental
PortabilityGHC
Safe HaskellNone
LanguageHaskell2010

Data.Binding.Hobbits

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

Values under multi-bindings

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

Closed terms

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

Pattern-matching multi-bindings and closed terms

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

Lifting values out of multi-bindings

Ancilliary modules

module Data.Proxy

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

NuMatchingAny1 f => NuMatching (RAssign f ctx) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

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

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