Data.Parameterized.Ctx

This module defines type-level lists used for representing the type of variables in a context.

Documentation

data Ctx k

Kind Ctx k comprises lists of types of kind k.

Constructors

EmptyCtx

(Ctx k) ::> k

Instances

TraversableFC k (Ctx k) (Assignment k)

Methods

traverseFC :: Applicative m => (forall (s :: Assignment k). e s -> m (f s)) -> t e c -> m (t f c)

TraversableFC k (Ctx k) (Assignment k)

Methods

traverseFC :: Applicative m => (forall (s :: Assignment k). e s -> m (f s)) -> t e c -> m (t f c)

FoldableFC k (Ctx k) (Assignment k)

Methods

foldMapFC :: Monoid m => (forall (s :: Assignment k). e s -> m) -> t e c -> m

foldrFC :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b

foldlFC :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b

foldrFC' :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b

foldlFC' :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b

toListFC :: (forall (tp :: Assignment k). f tp -> a) -> t f c -> [a]

FoldableFC k (Ctx k) (Assignment k)

Methods

foldMapFC :: Monoid m => (forall (s :: Assignment k). e s -> m) -> t e c -> m

foldrFC :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b

foldlFC :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b

foldrFC' :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b

foldlFC' :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b

toListFC :: (forall (tp :: Assignment k). f tp -> a) -> t f c -> [a]

OrdFC k (Ctx k) (Assignment k)

Methods

compareFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> OrderingF (Assignment k) x y) -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF l x y

OrdFC k (Ctx k) (Assignment k)

Methods

compareFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> OrderingF (Assignment k) x y) -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF l x y

TestEqualityFC k (Ctx k) (Assignment k)

Methods

testEqualityFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> Maybe ((Assignment k :~: x) y)) -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe ((l :~: x) y)

TestEqualityFC k (Ctx k) (Assignment k)

Methods

testEqualityFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> Maybe ((Assignment k :~: x) y)) -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe ((l :~: x) y)

FunctorFC k (Ctx k) (Assignment k)

Methods

fmapFC :: (forall (x :: Assignment k). f x -> g x) -> forall (x :: k). m f x -> m g x

FunctorFC k (Ctx k) (Assignment k)

Methods

fmapFC :: (forall (x :: Assignment k). f x -> g x) -> forall (x :: k). m f x -> m g x

Category (Ctx k) (Diff k)

Methods

id :: cat a a

(.) :: cat b c -> cat a b -> cat a c

Category (Ctx k) (Diff k)

Methods

id :: cat a a

(.) :: cat b c -> cat a b -> cat a c

TestEquality k f => TestEquality (Ctx k) (Assignment k f)

Methods

testEquality :: f a -> f b -> Maybe ((Assignment k f :~: a) b)

TestEquality k f => TestEquality (Ctx k) (Assignment k f)

Methods

testEquality :: f a -> f b -> Maybe ((Assignment k f :~: a) b)

HashableF k f => HashableF (Ctx k) (Assignment k f)

Methods

hashWithSaltF :: Int -> f tp -> Int

hashF :: f tp -> Int

HashableF k f => HashableF (Ctx k) (Assignment k f)

Methods

hashWithSaltF :: Int -> f tp -> Int

hashF :: f tp -> Int

ShowF k f => ShowF (Ctx k) (Assignment k f)

Methods

withShow :: p f -> q tp -> (Show (f tp) -> a) -> a

showF :: f tp -> String

showsF :: f tp -> String -> String

ShowF k f => ShowF (Ctx k) (Assignment k f)

Methods

withShow :: p f -> q tp -> (Show (f tp) -> a) -> a

showF :: f tp -> String

showsF :: f tp -> String -> String

OrdF k f => OrdF (Ctx k) (Assignment k f)

Methods

compareF :: ktp x -> ktp y -> OrderingF (Assignment k f) x y

leqF :: ktp x -> ktp y -> Bool

ltF :: ktp x -> ktp y -> Bool

geqF :: ktp x -> ktp y -> Bool

gtF :: ktp x -> ktp y -> Bool

OrdF k f => OrdF (Ctx k) (Assignment k f)

Methods

compareF :: ktp x -> ktp y -> OrderingF (Assignment k f) x y

leqF :: ktp x -> ktp y -> Bool

ltF :: ktp x -> ktp y -> Bool

geqF :: ktp x -> ktp y -> Bool

gtF :: ktp x -> ktp y -> Bool

KnownRepr (Ctx k) (Assignment k f) (EmptyCtx k)

Methods

knownRepr :: EmptyCtx k ctx

KnownRepr (Ctx k) (Assignment k f) (EmptyCtx k)

Methods

knownRepr :: EmptyCtx k ctx

(KnownRepr (Ctx k) (Assignment k f) ctx, KnownRepr k f bt) => KnownRepr (Ctx k) (Assignment k f) ((::>) k ctx bt)

Methods

knownRepr :: (k ::> ctx) bt ctx

(KnownRepr (Ctx k) (Assignment k f) ctx, KnownRepr k f bt) => KnownRepr (Ctx k) (Assignment k f) ((::>) k ctx bt)

Methods

knownRepr :: (k ::> ctx) bt ctx

type EmptyCtx = EmptyCtx

type SingleCtx x = EmptyCtx ::> x

type (::>) (c :: Ctx k) (a :: k) = c ::> a

type family (x :: Ctx k) <+> (y :: Ctx k) :: Ctx k where ...

Append two type-level contexts.

Equations

x <+> EmptyCtx = x

x <+> (y ::> e) = (x <+> y) ::> e

Type context manipulation

type family CtxSize (a :: Ctx k) :: Nat where ...

This type family computes the number of elements in a Ctx

Equations

CtxSize EmptyCtx = 0

CtxSize (xs ::> x) = 1 + CtxSize xs

type CtxLookup (n :: Nat) (ctx :: Ctx k) = CtxLookupRight (FromLeft ctx n) ctx

Lookup the value in a context by number, from the left. Produce a type error if the index is out of range.

type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) = CtxUpdateRight (FromLeft ctx n) x ctx

Update the value in a context by number, from the left. If the index is out of range, the context is unchanged.

type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where ...

Lookup the value in a context by number, from the right

Equations

CtxLookupRight 0 (ctx ::> r) = r

CtxLookupRight n (ctx ::> r) = CtxLookupRight (n - 1) ctx

type family CtxUpdateRight (n :: Nat) (x :: k) (ctx :: Ctx k) :: Ctx k where ...

Update the value in a context by number, from the right. If the index is out of range, the context is unchanged.

Equations

CtxUpdateRight n x EmptyCtx = EmptyCtx

CtxUpdateRight 0 x (ctx ::> old) = ctx ::> x

CtxUpdateRight n x (ctx ::> y) = CtxUpdateRight (n - 1) x ctx ::> y

type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint where ...

Helper type family used to generate descriptive error messages when an index is larger than the length of the Ctx being indexed.

Equations

CheckIx ctx n True = ()

CheckIx ctx n False = TypeError (((Text "Index " :<>: ShowType n) :<>: Text " out of range in ") :<>: ShowType ctx)

type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n ((n + 1) <=? CtxSize ctx)

A constraint that checks that the nat n is a valid index into the context ctx, and raises a type error if not.

type FromLeft ctx n = (CtxSize ctx - 1) - n

Ctx is a snoc-list. In order to use the more intuitive left-to-right ordering of elements the desired index is subtracted from the total number of elements.