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.

Documentation

module Data.Parameterized.Context.Unsafe

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

Context extension and embedding utilities

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

Context embedding.

Constructors

CtxEmbedding

Fields

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

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

Minimal complete definition

extendContext

Methods

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

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

Minimal complete definition

extendContext'

Methods

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

Instances

ExtendContext' k' k' (Index k')

Methods

extendContext' :: Diff (Index k') ctx ctx' -> f ctx v -> f ctx' v

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

Minimal complete definition

applyEmbedding

Methods

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

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

Minimal complete definition

applyEmbedding'

Methods

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

Instances

ApplyEmbedding' k' k' (Index k')

Methods

applyEmbedding' :: CtxEmbedding (Index k') ctx ctx' -> f ctx v -> f 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)

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.

getCtx :: forall n ctx f r. Idx n ctx r => Assignment f ctx -> f r

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

setCtx :: forall n ctx f r. Idx n ctx r => f r -> Assignment f ctx -> Assignment f ctx

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.

Minimal complete definition

curryAssignment, uncurryAssignment

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 k (EmptyCtx k)

Methods

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

uncurryAssignment :: CurryAssignment (EmptyCtx k) ctx f x -> Assignment (EmptyCtx k) f ctx -> x

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

Methods

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

uncurryAssignment :: CurryAssignment ((k ::> ctx) a) ctx f x -> Assignment ((k ::> ctx) a) f ctx -> x