Data.Parameterized.Context

This module reexports either Data.Parameterized.Context.Safe or Data.Parameterized.Context.Unsafe depending on the the unsafe-operations compile-time flag.

It also defines some utility typeclasses for transforming between curried and uncurried versions of functions over contexts.

The Assignment type is isomorphic to the List type, except Assignments construct lists from the right-hand side, and instead of using type-level '[]-style lists, an Assignment is indexed by a type-level Ctx. The implementation of Assignments is also more efficent than List for lists of many elements, as it uses a balanced binary tree representation rather than a linear-time list. For a motivating example, see List.

Documentation

module Data.Parameterized.Ctx

class KnownContext (ctx :: Ctx k) where

A context that can be determined statically at compiler time.

Methods

knownSize :: Size ctx

Instances

KnownContext ('EmptyCtx :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownSize :: Size 'EmptyCtx

KnownContext ctx => KnownContext (ctx ::> tp :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownSize :: Size (ctx ::> tp)

Size

data Size (ctx :: Ctx k)

Represents the size of a context.

Instances

ShowF (Size :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p Size -> q tp -> (Show (Size tp) => a) -> a

showF :: forall (tp :: k0). Size tp -> String

showsPrecF :: forall (tp :: k0). Int -> Size tp -> String -> String

Show (Size ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> Size ctx -> ShowS

show :: Size ctx -> String

showList :: [Size ctx] -> ShowS

sizeInt :: Size ctx -> Int

Convert a context size to an Int.

zeroSize :: Size 'EmptyCtx

The size of an empty context.

incSize :: Size ctx -> Size (ctx ::> tp)

Increment the size to the next value.

decSize :: Size (ctx ::> tp) -> Size ctx

extSize :: Size l -> Diff l r -> Size r

Extend the size by a given difference.

addSize :: Size x -> Size y -> Size (x <+> y)

The total size of two concatenated contexts.

data SizeView (ctx :: Ctx k) where

Allows interpreting a size.

Constructors

ZeroSize :: SizeView 'EmptyCtx

IncSize :: !(Size ctx) -> SizeView (ctx ::> tp)

viewSize :: Size ctx -> SizeView ctx

Project a size

Diff

data Diff (l :: Ctx k) (r :: Ctx k)

Difference in number of elements between two contexts. The first context must be a sub-context of the other.

Instances

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

Implemented with noDiff and addDiff

Defined in Data.Parameterized.Context.Unsafe

Methods

id :: forall (a :: k0). Diff a a

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

noDiff :: Diff l l

The identity difference. Identity element of Category instance.

addDiff :: Diff a b -> Diff b c -> Diff a c

The addition of differences. Flipped binary operation of Category instance.

extendRight :: Diff l r -> Diff l (r ::> tp)

Extend the difference to a sub-context of the right side.

appendDiff :: Size r -> Diff l (l <+> r)

data DiffView a b where

Constructors

NoDiff :: DiffView a a

ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)

viewDiff :: Diff a b -> DiffView a b

class KnownDiff (l :: Ctx k) (r :: Ctx k) where

A difference that can be automatically inferred at compile time.

Methods

knownDiff :: Diff l r

Instances

KnownDiff (l :: Ctx k) (l :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownDiff :: Diff l l

KnownDiff l r => KnownDiff (l :: Ctx k) (r ::> tp :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownDiff :: Diff l (r ::> tp)

data IsAppend l r where

Proof that r = l + app for some app

Constructors

IsAppend :: Size app -> IsAppend l (l <+> app)

diffIsAppend :: Diff l r -> IsAppend l r

If l is a sub-context of r then extract out their "contextual difference", i.e., the app such that r = l + app

Indexing

data Index (ctx :: Ctx k) (tp :: k)

An index is a reference to a position with a particular type in a context.

Instances

ExtendContext' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'0). Diff ctx ctx' -> Index ctx v -> Index ctx' v

ApplyEmbedding' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'0). CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v

TestEquality (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: forall (a :: k0) (b :: k0). Index ctx a -> Index ctx b -> Maybe (a :~: b)

HashableF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: forall (tp :: k0). Int -> Index ctx tp -> Int

hashF :: forall (tp :: k0). Index ctx tp -> Int

ShowF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p (Index ctx) -> q tp -> (Show (Index ctx tp) => a) -> a

showF :: forall (tp :: k0). Index ctx tp -> String

showsPrecF :: forall (tp :: k0). Int -> Index ctx tp -> String -> String

OrdF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> OrderingF x y

leqF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool

ltF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool

geqF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool

gtF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool

Eq (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

(==) :: Index ctx tp -> Index ctx tp -> Bool

(/=) :: Index ctx tp -> Index ctx tp -> Bool

Ord (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

compare :: Index ctx tp -> Index ctx tp -> Ordering

(<) :: Index ctx tp -> Index ctx tp -> Bool

(<=) :: Index ctx tp -> Index ctx tp -> Bool

(>) :: Index ctx tp -> Index ctx tp -> Bool

(>=) :: Index ctx tp -> Index ctx tp -> Bool

max :: Index ctx tp -> Index ctx tp -> Index ctx tp

min :: Index ctx tp -> Index ctx tp -> Index ctx tp

Show (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> Index ctx tp -> ShowS

show :: Index ctx tp -> String

showList :: [Index ctx tp] -> ShowS

Hashable (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSalt :: Int -> Index ctx tp -> Int

hash :: Index ctx tp -> Int

indexVal :: Index ctx tp -> Int

baseIndex :: Index ('EmptyCtx ::> tp) tp

Index for first element in context.

skipIndex :: Index ctx x -> Index (ctx ::> y) x

Increase context while staying at same index.

lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp

Return the last index of a element.

nextIndex :: Size ctx -> Index (ctx ::> tp) tp

Return the index of a element one past the size.

leftIndex :: Size r -> Index l tp -> Index (l <+> r) tp

Adapts an index in the left hand context of an append operation.

rightIndex :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp

Adapts an index in the right hand context of an append operation.

extendIndex :: KnownDiff l r => Index l tp -> Index r tp

extendIndex' :: Diff l r -> Index l tp -> Index r tp

Compute an Index into a context r from an Index into a sub-context l of r.

extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp

Compute an Index into an appended context from an Index into its suffix.

forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r

Given a size n, an initial value v0, and a function f, the expression forIndex n v0 f is equivalent to v0 when n is zero, and f (forIndex (n-1) v0) n otherwise. Unlike the safe version, which starts from Index 0 and increments Index values, this version starts at Index (n-1) and decrements Index values to Index 0.

forIndexRange :: forall ctx r. Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r

Given an index i, size n, a function f, value v, and a function f, the expression forIndex i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n v) otherwise.

intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))

Return index at given integer or nothing if integer is out of bounds.

data IndexView ctx tp where

View of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range.

Constructors

IndexViewLast :: !(Size ctx) -> IndexView (ctx ::> t) t

IndexViewInit :: !(Index ctx t) -> IndexView (ctx ::> u) t

Instances

ShowF (IndexView ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p (IndexView ctx) -> q tp -> (Show (IndexView ctx tp) => a) -> a

showF :: forall (tp :: k0). IndexView ctx tp -> String

showsPrecF :: forall (tp :: k0). Int -> IndexView ctx tp -> String -> String

Show (IndexView ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> IndexView ctx tp -> ShowS

show :: IndexView ctx tp -> String

showList :: [IndexView ctx tp] -> ShowS

viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp

Project an index

IndexRange

data IndexRange (ctx :: Ctx k) (sub :: Ctx k)

This represents a contiguous range of indices.

allRange :: Size ctx -> IndexRange ctx ctx

Return a range containing all indices in the context.

indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e

indexOfRange returns the only index in a range.

dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y

dropHeadRange r n drops the first n elements in r.

dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x

dropTailRange r n drops the last n elements in r.

Assignments

data Assignment (f :: k -> Type) (ctx :: Ctx k)

An assignment is a sequence that maps each index with type tp to a value of type f tp.

This assignment implementation uses a binomial tree implementation that offers lookups and updates in time and space logarithmic with respect to the number of elements in the context.

Instances

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

Defined in Data.Parameterized.Context.Unsafe

Methods

traverseFC :: forall f g m. 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 :: forall f m. 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 f b. (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 f b. (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

IxedF' k (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

ixF' :: forall (x :: k). IndexF (Assignment f ctx) x -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x)

IxedF k (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

ixF :: forall (x :: k). IndexF (Assignment f ctx) x -> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x)

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

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: forall (a :: k0) (b :: k0). 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 :: forall (tp :: k0). Int -> Assignment f tp -> Int

hashF :: forall (tp :: k0). Assignment f tp -> Int

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

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a

showF :: forall (tp :: k0). Assignment f tp -> String

showsPrecF :: forall (tp :: k0). Int -> Assignment f tp -> String -> String

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

Defined in Data.Parameterized.Context.Unsafe

Methods

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

leqF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

ltF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

geqF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

gtF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool

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

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k0) r. 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)

TestEquality f => Eq (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

(==) :: Assignment f ctx -> Assignment f ctx -> Bool

(/=) :: Assignment f ctx -> Assignment f ctx -> Bool

OrdF f => Ord (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

compare :: Assignment f ctx -> Assignment f ctx -> Ordering

(<) :: Assignment f ctx -> Assignment f ctx -> Bool

(<=) :: Assignment f ctx -> Assignment f ctx -> Bool

(>) :: Assignment f ctx -> Assignment f ctx -> Bool

(>=) :: Assignment f ctx -> Assignment f ctx -> Bool

max :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx

min :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx

ShowF f => Show (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> Assignment f ctx -> ShowS

show :: Assignment f ctx -> String

showList :: [Assignment f ctx] -> ShowS

NFData (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

rnf :: Assignment f ctx -> ()

HashableF f => Hashable (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSalt :: Int -> Assignment f ctx -> Int

hash :: Assignment f ctx -> Int

type IxValueF (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

type IxValueF (Assignment f ctx) = f

type IndexF (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

type IndexF (Assignment f ctx) = Index ctx

size :: Assignment f ctx -> Size ctx

Return number of elements in assignment.

replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx

replicate n make a context with different copies of the same polymorphic value.

generate :: Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx

Generate an assignment

generateM :: Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx)

Generate an assignment in an Applicative context

empty :: Assignment f EmptyCtx

Return empty assignment

extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)

adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx

Deprecated: Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead.

update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx

Deprecated: Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead.

adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)

Modify the value of an assignment at a particular index.

data AssignView f ctx where

Represent an assignment as either empty or an assignment with one appended.

Constructors

AssignEmpty :: AssignView f EmptyCtx

AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)

viewAssign :: forall f ctx. Assignment f ctx -> AssignView f ctx

View an assignment as either empty or an assignment with one appended.

(!) :: Assignment f ctx -> Index ctx tp -> f tp

Return value of assignment.

(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp

Return value of assignment, where the index is into an initial sequence of the assignment.

zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a

zipWithM :: Applicative m => (forall x. f x -> g x -> m (h x)) -> Assignment f a -> Assignment g a -> m (Assignment h a)

(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)

traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)

singleton :: f tp -> Assignment f (EmptyCtx ::> tp)

Create a single element context.

toVector :: Assignment f tps -> (forall tp. f tp -> e) -> Vector e

Convert the assignment to a vector.

pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx' infixl 9

Pattern synonym for extending an assignment on the right

pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx

Pattern synonym for the empty assignment

decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)

null :: Assignment f ctx -> Bool

Return true if assignment is empty.

init :: Assignment f (ctx ::> tp) -> Assignment f ctx

Return assignment with all but the last block.

last :: Assignment f (ctx ::> tp) -> f tp

Return the last element in the assignment.

view :: forall f ctx. Assignment f ctx -> AssignView f ctx

Deprecated: Use viewAssign or the Empty and :> patterns instead.

View an assignment as either empty or an assignment with one appended.

take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx

Return the prefix of an appended Assignment

drop :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'

Return the suffix of an appended Assignment

forIndexM :: forall ctx m. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m ()) -> m ()

'forIndexM sz f' calls f on indices '[0..sz-1]'.

generateSome :: forall f. Int -> (Int -> Some f) -> Some (Assignment f)

Generate an assignment with some context type that is not known.

generateSomeM :: forall m f. Applicative m => Int -> (Int -> m (Some f)) -> m (Some (Assignment f))

Generate an assignment with some context type that is not known.

fromList :: [Some f] -> Some (Assignment f)

Create an assignment from a list of values.

traverseAndCollect :: (Monoid w, Applicative m) => (forall tp. Index ctx tp -> f tp -> m w) -> Assignment f ctx -> m w

Visit each of the elements in an Assignment in order from left to right and collect the results using the provided Monoid.

traverseWithIndex_ :: Applicative m => (forall tp. Index ctx tp -> f tp -> m ()) -> Assignment f ctx -> m ()

Visit each of the elements in an Assignment in order from left to right, executing an action with each.

dropPrefix

Arguments

:: forall f xs prefix a. TestEquality f

=> Assignment f xs

Assignment to split

-> Assignment f prefix

Expected prefix

-> a

error continuation

-> (forall addl. xs ~ (prefix <+> addl) => Assignment f addl -> a)

success continuation

-> a

Utility function for testing if xs is an assignment with prefix as a prefix, and computing the tail of xs not in the prefix, if so.

Context extension and embedding utilities

data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k)

This datastructure contains a proof that the first context is embeddable in the second. This is useful if we want to add extend an existing term under a larger context.

Constructors

CtxEmbedding

Fields

• _ctxeSize :: Size ctx'
• _ctxeAssignment :: Assignment (Index ctx') ctx

class ExtendContext (f :: Ctx k -> *) where

Methods

extendContext :: Diff ctx ctx' -> f ctx -> f ctx'

class ExtendContext' (f :: Ctx k -> k' -> *) where

Methods

extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v

Instances

ExtendContext' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'0). Diff ctx ctx' -> Index ctx v -> Index ctx' v

class ApplyEmbedding (f :: Ctx k -> *) where

Methods

applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx'

class ApplyEmbedding' (f :: Ctx k -> k' -> *) where

Methods

applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v

Instances

ApplyEmbedding' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'0). CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v

identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx

extendEmbeddingRightDiff :: forall ctx ctx' ctx''. Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''

extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)

extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)

appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')

Prove that the prefix of an appended context is embeddable in it

appendEmbeddingLeft :: Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')

Prove that the suffix of an appended context is embeddable in it

ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')

ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx') (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)

Static indexing and lenses for assignments

type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)

Constraint synonym used for getting an Index into a Ctx. n is the zero-based, left-counted index into the list of types ctx which has the type r.

field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r)

Get a lens for an position in an Assignment by zero-based, left-to-right position. The position must be specified using TypeApplications for the n parameter.

natIndex :: forall n ctx r. Idx n ctx r => Index ctx r

Compute an Index value for a particular position in a Ctx. The TypeApplications extension will be needed to disambiguate the choice of the type n.

natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r

This version of natIndex is suitable for use without the TypeApplications extension.

Currying and uncurrying for assignments

type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: * where ...

This type family is used to define currying/uncurrying operations on assignments. It is best understood by seeing its evaluation on several examples:

CurryAssignment EmptyCtx f x = x
CurryAssignment (EmptyCtx ::> a) f x = f a -> x
CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x
CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x

Equations

CurryAssignment EmptyCtx f x = x

CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> x)

class CurryAssignmentClass (ctx :: Ctx k) where

This class implements two methods that witness the isomorphism between curried and uncurried functions.

Methods

curryAssignment :: (Assignment f ctx -> x) -> CurryAssignment ctx f x

Transform a function that accepts an assignment into one with a separate variable for each element of the assignment.

uncurryAssignment :: CurryAssignment ctx f x -> Assignment f ctx -> x

Transform a curried function into one that accepts an assignment value.

Instances

CurryAssignmentClass (EmptyCtx :: Ctx k)

Defined in Data.Parameterized.Context

Methods

curryAssignment :: forall (f :: k0 -> Type) x. (Assignment f EmptyCtx -> x) -> CurryAssignment EmptyCtx f x

uncurryAssignment :: forall (f :: k0 -> Type) x. CurryAssignment EmptyCtx f x -> Assignment f EmptyCtx -> x

CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a :: Ctx k)

Defined in Data.Parameterized.Context

Methods

curryAssignment :: forall (f :: k0 -> Type) x. (Assignment f (ctx ::> a) -> x) -> CurryAssignment (ctx ::> a) f x

uncurryAssignment :: forall (f :: k0 -> Type) x. CurryAssignment (ctx ::> a) f x -> Assignment f (ctx ::> a) -> x

Size and Index values

size1 :: Size (EmptyCtx ::> a)

size2 :: Size ((EmptyCtx ::> a) ::> b)

size3 :: Size (((EmptyCtx ::> a) ::> b) ::> c)

size4 :: Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)

size5 :: Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)

size6 :: Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)

i1of2 :: Index ((EmptyCtx ::> a) ::> b) a

i2of2 :: Index ((EmptyCtx ::> a) ::> b) b

i1of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) a

i2of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) b

i3of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) c

i1of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a

i2of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b

i3of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c

i4of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d

i1of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a

i2of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b

i3of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c

i4of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d

i5of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e

i1of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a

i2of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b

i3of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c

i4of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d

i5of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e

i6of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f