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

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.

Minimal complete definition

knownSize

Methods

knownSize :: Size ctx

Instances

KnownContext k (EmptyCtx k)

Methods

knownSize :: Size (EmptyCtx k) ctx

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

Methods

knownSize :: Size ((k ::> ctx) tp) ctx

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 (Ctx k) (Diff k)

Methods

id :: cat a a

(.) :: cat b c -> cat a b -> cat 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.

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

A difference that can be automatically inferred at compile time.

Minimal complete definition

knownDiff

Methods

knownDiff :: Diff l r

Instances

KnownDiff k l l

Methods

knownDiff :: Diff l l r

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

Methods

knownDiff :: Diff l ((k ::> r) tp) 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

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 k (Index k ctx)

Methods

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

HashableF k (Index k ctx)

Methods

hashWithSaltF :: Int -> f tp -> Int

hashF :: f tp -> Int

ShowF k (Index k ctx)

Methods

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

showF :: f tp -> String

showsF :: f tp -> String -> String

OrdF k (Index k ctx)

Methods

compareF :: ktp x -> ktp y -> OrderingF (Index k ctx) 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

Eq (Index k ctx tp)

Methods

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

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

Ord (Index k ctx tp)

Methods

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

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

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

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

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

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

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

Show (Index k ctx tp)

Methods

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

show :: Index k ctx tp -> String

showList :: [Index k ctx tp] -> ShowS

Hashable (Index k ctx tp)

Methods

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

hash :: Index k 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.

base :: Index (EmptyCtx ::> tp) tp

Index for first element in context.

skip :: 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, 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.

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 -> *) (ctx :: Ctx k)

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

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)

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

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

IxedF' k (Assignment k f ctx)

Methods

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

IxedF k (Assignment k f ctx)

Methods

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

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

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

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

TestEquality k f => Eq (Assignment k f ctx)

Methods

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

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

OrdF k f => Ord (Assignment k f ctx)

Methods

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

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

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

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

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

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

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

ShowF k f => Show (Assignment k f ctx)

Methods

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

show :: Assignment k f ctx -> String

showList :: [Assignment k f ctx] -> ShowS

NFData (Assignment k f ctx)

Methods

rnf :: Assignment k f ctx -> ()

HashableF k f => Hashable (Assignment k f ctx)

Methods

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

hash :: Assignment k f ctx -> Int

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

Methods

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

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

type IxValueF k (Assignment k f ctx)

type IxValueF k (Assignment k f ctx) = f

type IndexF k (Assignment k f ctx)

type IndexF k (Assignment k f ctx) = Index k 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 indexec vector.

null :: Assignment f ctx -> Bool

Return true if assignment is empty.

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

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

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

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

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

Return assignment with all but the last block.

data AssignView (f :: k -> *) (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)

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

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

(!) :: 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.

toList :: (forall tp. f tp -> a) -> Assignment f c -> [a]

Convert assignment to list.

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)