Data.Parameterized.Context.Safe

This module defines type contexts as a data-kind that consists of a list of types. Indexes are defined with respect to these contexts. In addition, finite dependent products (Assignments) are defined over type contexts. The elements of an assignment can be accessed using appropriately-typed indexes.

This module is intended to export exactly the same API as module Data.Parameterized.Context.Unsafe, so that they can be used interchangeably.

This implementation is entirely typesafe, and provides a proof that the signature implemented by this module is consistent. Contexts, indexes, and assignments are represented naively by linear sequences.

Compared to the implementation in Data.Parameterized.Context.Unsafe, this one suffers from the fact that the operation of extending an the context of an index is not a no-op. We therefore cannot use coerce to understand indexes in a new context without actually breaking things.

Documentation

module Data.Parameterized.Ctx

Size

data Size (ctx :: Ctx k)

An indexed singleton type representing the size of a context.

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

View a size as either zero or a smaller size plus one.

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.Safe

Methods

knownSize :: Size EmptyCtx

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

Defined in Data.Parameterized.Context.Safe

Methods

knownSize :: Size (ctx ::> tp)

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)

Defined in Data.Parameterized.Context.Safe

Methods

id :: Diff a a

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

noDiff :: Diff l l

The identity difference.

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.Safe

Methods

knownDiff :: Diff l l

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

Defined in Data.Parameterized.Context.Safe

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

TestEquality (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Safe

Methods

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

HashableF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Safe

Methods

hashWithSaltF :: Int -> Index ctx tp -> Int

hashF :: Index ctx tp -> Int

ShowF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Safe

Methods

withShow :: p (Index ctx) -> q tp -> (Show (Index ctx tp) -> a) -> a

showF :: Index ctx tp -> String

showsPrecF :: Int -> Index ctx tp -> String -> String

OrdF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Safe

Methods

compareF :: Index ctx x -> Index ctx y -> OrderingF x y

leqF :: Index ctx x -> Index ctx y -> Bool

ltF :: Index ctx x -> Index ctx y -> Bool

geqF :: Index ctx x -> Index ctx y -> Bool

gtF :: Index ctx x -> Index ctx y -> Bool

Eq (Index ctx tp)

Defined in Data.Parameterized.Context.Safe

Methods

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

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

Ord (Index ctx tp)

Defined in Data.Parameterized.Context.Safe

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.Safe

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.Safe

Methods

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

hash :: Index ctx tp -> Int

indexVal :: Index ctx tp -> Int

Convert an index to an Int, where the index of the left-most type in the context is 0.

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 an element one past the size.

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

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

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 calls f on each index less than n starting from 0 and v0, with the value v obtained from the last call.

forIndexRange :: 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 forIndexRange 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.

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'.

Instances

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

Defined in Data.Parameterized.Context.Safe

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.Safe

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.Safe

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.Safe

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.Safe

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.Safe

Methods

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

IxedF k (Assignment f ctx)

Defined in Data.Parameterized.Context.Safe

Methods

ixF :: 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.Safe

Methods

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

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

Defined in Data.Parameterized.Context.Safe

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.Safe

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.Safe

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

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

Defined in Data.Parameterized.Context.Safe

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.Safe

Methods

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

TestEquality f => Eq (Assignment f ctx)

Defined in Data.Parameterized.Context.Safe

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.Safe

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.Safe

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.Safe

Methods

rnf :: Assignment f ctx -> ()

HashableF f => Hashable (Assignment f ctx)

Defined in Data.Parameterized.Context.Safe

Methods

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

hash :: Assignment f ctx -> Int

TestEquality f => PolyEq (Assignment f x) (Assignment f y)

Defined in Data.Parameterized.Context.Safe

Methods

polyEqF :: Assignment f x -> Assignment f y -> Maybe (Assignment f x :~: Assignment f y)

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

type IxValueF (Assignment f ctx)

Defined in Data.Parameterized.Context.Safe

type IxValueF (Assignment f ctx) = f

type IndexF (Assignment f ctx)

Defined in Data.Parameterized.Context.Safe

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 :: forall ctx f. Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx

Generate an assignment

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

Generate an assignment

empty :: Assignment f EmptyCtx

Create empty indexed vector.

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

adjust :: forall f ctx tp. (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 :: forall f ctx tp. 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 :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)

data AssignView (f :: k -> Type) (ctx :: Ctx k) where

View 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

(!) :: 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 tp. f tp -> g tp -> m (h tp)) -> Assignment f c -> Assignment g c -> m (Assignment h c)

(<++>) :: 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)