Data.Type.RList

A right list, or RList, is a list where cons adds to the end, or the right-hand side, of a list. This is useful conceptually for contexts of name-bindings, where the most recent name-binding is intuitively at the end of the context.

Right-lists as a datatype

data RList a

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

Constructors

RNil

(RList a) :> 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

Proofs of membership in a type-level list

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

weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a

Weaken a Member proof by prepending another context to the context it proves membership in

Proofs that one list equals the append of two others

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)

mkAppend :: RAssign f c2 -> Append c1 c2 (c1 :++: c2)

Make an Append proof from any RAssign vector for the second argument of the append.

mkMonoAppend :: Proxy c1 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2)

A version of mkAppend that takes in a Proxy argument.

proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2

The inverse of mkAppend, that builds an RAssign from an Append

Contexts

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)

empty :: RAssign f RNil

Create an empty RAssign vector.

singleton :: f a -> RAssign f (RNil :> a)

Create a singleton RAssign vector.

get :: Member c a -> RAssign f c -> f a

Look up an element of an RAssign vector using a Member proof

data HApply (f :: k1 -> Type) (a :: k2) where

Heterogeneous type application, including a proof that the input kind of the function equals the kind of the type argument

Constructors

HApply :: forall (f :: k -> Type) (a :: k). f a -> HApply f a

hget :: forall (f :: k1 -> Type) (c :: RList k1) (a :: k2). Member c a -> RAssign f c -> HApply f a

Look up an element of an RAssign vector using a Member proof at what GHC thinks might be a different kind, i.e., heterogeneously

modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c

Modify an element of an RAssign vector using a Member proof.

set :: Member c a -> f a -> RAssign f c -> RAssign f c

Set an element of an RAssign vector using a Member proof.

memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a)

Test if an object is in an RAssign, returning a Member proof if it is

map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c

Map a function on all elements of an RAssign vector.

mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c

An alternate name for map that does not clash with the prelude

map2 :: (forall x. f x -> g x -> h x) -> RAssign f c -> RAssign g c -> RAssign h c

Map a binary function on all pairs of elements of two RAssign vectors.

tail :: RAssign f (ctx :> a) -> RAssign f ctx

Take the tail of an RAssign

toList :: RAssign (Constant a) c -> [a]

Convert a monomorphic RAssign to a list

mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b]

Map a function with monomorphic output type across an RAssign to create a standard list:

mapToList f = toList . map (Constant . f)

append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)

Append two RAssign vectors.

foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r

Perform a right fold across an RAssign

split :: c ~ (c1 :++: c2) => prx c1 -> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)

Split an RAssign vector into two pieces. The first argument is a phantom argument that gives the form of the first list piece.

members :: RAssign f c -> RAssign (Member c) c

Create a vector of proofs that each type in c is a Member of c.

class TypeCtx ctx where

A type-class which ensures that ctx is a valid context, i.e., has | the form (RNil :> t1 :> ... :> tn) for some types t1 through tn

Methods

typeCtxProxies :: RAssign Proxy ctx

Instances

TypeCtx (RNil :: RList k)

Defined in Data.Type.RList

Methods

typeCtxProxies :: RAssign Proxy RNil

TypeCtx ctx => TypeCtx (ctx :> a :: RList k)

Defined in Data.Type.RList

Methods

typeCtxProxies :: RAssign Proxy (ctx :> a)