Data.Parameterized.Ctx

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

A Ctx is never intended to be manipulated at the value level; it is used purely as a type-level list, just like '[]. To see how it is used, see the module header for Data.Parameterized.Context.

Documentation

data Ctx k

Kind Ctx k comprises lists of types of kind k.

Constructors

EmptyCtx

(Ctx k) ::> k

Instances

TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

traverseFC :: Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). Assignment f x -> m (Assignment g x)

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

foldMapFC :: Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). Assignment f x -> m

foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b

foldlFC :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b

foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b

foldlFC' :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b

toListFC :: (forall (x :: k0). f x -> a) -> forall (x :: l). Assignment f x -> [a]

OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

TestEqualityFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). Assignment f x -> Assignment g x

Category (Diff :: Ctx k -> Ctx k -> Type)

Implemented with noDiff and addDiff

Defined in Data.Parameterized.Context.Unsafe

Methods

id :: Diff a a

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

ShowF (Size :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

showF :: Size tp -> String

showsPrecF :: Int -> Size tp -> String -> String

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

HashableF f => HashableF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: Int -> Assignment f tp -> Int

hashF :: Assignment f tp -> Int

ShowF f => ShowF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

showF :: Assignment f tp -> String

showsPrecF :: Int -> Assignment f tp -> String -> String

OrdF f => OrdF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareF :: Assignment f x -> Assignment f y -> OrderingF x y

leqF :: Assignment f x -> Assignment f y -> Bool

ltF :: Assignment f x -> Assignment f y -> Bool

geqF :: Assignment f x -> Assignment f y -> Bool

gtF :: Assignment f x -> Assignment f y -> Bool

IsRepr f => IsRepr (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: Assignment f a -> (KnownRepr (Assignment f) a -> r) -> r

KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f EmptyCtx

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

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f (ctx ::> bt)

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.