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.

Documentation

data RList a

Constructors

RNil

(RList a) :> a

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

Instances

type r :++: (RNil *)

type r :++: (RNil *) = r

type r1 :++: ((:>) * r2 a)

type r1 :++: ((:>) * r2 a) = (:>) * ((:++:) r1 r2) a

proxyCons :: Proxy r -> f a -> Proxy (r :> a)

data Member ctx a 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

Show (Member r a)

Methods

showsPrec :: Int -> Member r a -> ShowS

show :: Member r a -> String

showList :: [Member r a] -> ShowS

NuMatching (Member c a)

Methods

nuMatchingProof :: MbTypeRepr (Member c a)

Liftable (Member c a)

Methods

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

showsPrecMember :: Bool -> Member ctx a -> ShowS

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

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

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)

data MapRList f c where

A MapRList f r is a vector with exactly one element of type f a for each type a in the type RList r.

Constructors

MNil :: MapRList f RNil

(:>:) :: MapRList f c -> f a -> MapRList f (c :> a)

Instances

Show (MapRList Name c)

Methods

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

show :: MapRList Name c -> String

showList :: [MapRList Name c] -> ShowS

(NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList f ctx)

Methods

nuMatchingProof :: MbTypeRepr (MapRList f ctx)

empty :: MapRList f RNil

Create an empty MapRList vector.

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

Create a singleton MapRList vector.

mapRListLookup :: Member c a -> MapRList f c -> f a

Look up an element of a MapRList vector using a Member proof.

mapMapRList :: (forall x. f x -> g x) -> MapRList f c -> MapRList g c

Map a function on all elements of a MapRList vector.

mapMapRList2 :: (forall x. f x -> g x -> h x) -> MapRList f c -> MapRList g c -> MapRList h c

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

appendMapRList :: MapRList f c1 -> MapRList f c2 -> MapRList f (c1 :++: c2)

Append two MapRList vectors.

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

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

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

A version of mkAppend that takes in a Proxy argument.

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

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

splitMapRList :: c ~ (c1 :++: c2) => Proxy c1 -> MapRList any c2 -> MapRList f c -> (MapRList f c1, MapRList f c2)

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

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

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

mapRListToList :: MapRList (Constant a) c -> [a]

Convert an MapRList to a list

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

Minimal complete definition

typeCtxProxies

Methods

typeCtxProxies :: MapRList Proxy ctx

Instances

TypeCtx (RNil *)

Methods

typeCtxProxies :: MapRList (Proxy *) (RNil *)

TypeCtx ctx => TypeCtx ((:>) * ctx a)

Methods

typeCtxProxies :: MapRList (Proxy *) ((* :> ctx) a)