| Copyright | (c) 2016 Edwin Westbrook |
|---|---|
| License | BSD3 |
| Maintainer | westbrook@galois.com |
| Stability | experimental |
| Portability | GHC |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Type.RList
Description
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.
Synopsis
- data RList a
- type family (r1 :: RList k) :++: (r2 :: RList k) :: RList k
- data Member (ctx :: RList k1) (a :: k2) where
- Member_Base :: Member (ctx :> a) a
- Member_Step :: Member ctx a -> Member (ctx :> b) a
- weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
- data Append ctx1 ctx2 ctx where
- 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)
- mkMonoAppend :: Proxy c1 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2)
- proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2
- data RAssign (f :: k -> *) (c :: RList k) where
- empty :: RAssign f RNil
- singleton :: f a -> RAssign f (RNil :> a)
- get :: Member c a -> RAssign f c -> f a
- data HApply (f :: k1 -> Type) (a :: k2) where
- hget :: forall k1 k2 (f :: k1 -> Type) (c :: RList k1) (a :: k2). Member c a -> RAssign f c -> HApply f a
- modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c
- set :: Member c a -> f a -> RAssign f c -> RAssign f c
- memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a)
- map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c
- mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c
- map2 :: (forall x. f x -> g x -> h x) -> RAssign f c -> RAssign g c -> RAssign h c
- tail :: RAssign f (ctx :> a) -> RAssign f ctx
- toList :: RAssign (Constant a) c -> [a]
- mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b]
- append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
- foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r
- split :: c ~ (c1 :++: c2) => prx c1 -> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
- members :: RAssign f c -> RAssign (Member c) c
- class TypeCtx ctx where
- typeCtxProxies :: RAssign Proxy ctx
Right-lists as a datatype
A form of lists where elements are added to the right instead of the left
type family (r1 :: RList k) :++: (r2 :: RList k) :: RList k infixr 5 Source #
Append two RLists at the type level
Proofs of membership in a type-level list
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
| TestEquality (Member ctx :: k -> Type) Source # | |
Defined in Data.Type.RList | |
| Eq (Member ctx a) Source # | |
| Show (Member r a) Source # | |
| NuMatching (Member ctx a) Source # | |
Defined in Data.Binding.Hobbits.NuMatchingInstances Methods nuMatchingProof :: MbTypeRepr (Member ctx a) Source # | |
| Closable (Member ctx a) Source # | |
| Liftable (Member c a) Source # | |
weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a Source #
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 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) |
Contexts
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
Instances
| Show (RAssign (Name :: k -> Type) c) Source # | |
| NuMatchingAny1 f => NuMatching (RAssign f ctx) Source # | |
Defined in Data.Binding.Hobbits.NuMatching Methods nuMatchingProof :: MbTypeRepr (RAssign f ctx) Source # | |
| ClosableAny1 f => Closable (RAssign f ctx) Source # | |
data HApply (f :: k1 -> Type) (a :: k2) where Source #
Heterogeneous type application, including a proof that the input kind of the function equals the kind of the type argument
hget :: forall k1 k2 (f :: k1 -> Type) (c :: RList k1) (a :: k2). Member c a -> RAssign f c -> HApply f a Source #
memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a) Source #
map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c Source #
Map a function on all elements of an RAssign vector.
mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c Source #
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 Source #
Map a binary function on all pairs of elements of two RAssign vectors.
mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b] Source #
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) Source #
Append two RAssign vectors.
foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r Source #
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) Source #
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 Source #
Create a vector of proofs that each type in c is a Member of c.