| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Circuit.Mat.Array
Description
Arrays as the monoidal array category [C; I] of Abbott & Zardini.
Overview
Abbott & Zardini define an array category [C; I] from any base symmetric
monoidal category C and any indexing category I. Objects are synthetic
arrays [X; P]; morphisms are generated by two families:
- Batch lift
[f; P]— apply a base morphismf : X -> Yat every index of shapeP. - Reindexing
[X; η]— precompose with an indexing morphismη : P -> Q.
This module gives a direct presheaf semantics: an array of shape s over
base category arr is a morphism Fins s -> X in arr. The two
generators are therefore exactly categorical composition in arr.
Instantiations
arr = (->): arrays are functions from indices to values.arr = Mat r: arrays are functional matrices between finite index sets.
The module also provides a conceptual renaming: backpermute in harpie
is reindex in [C; I].
Synopsis
- type IxMap (s' :: [Nat]) (s :: [Nat]) = Fins s' -> Fins s
- newtype ArrayC (arr :: Type -> Type -> Type) (s :: [Nat]) a = ArrayC {}
- class Category arr => LiftFun (arr :: Type -> Type -> Type) where
- liftFun :: (i -> j) -> arr i j
- class Category arr => Tabular (arr :: Type -> Type -> Type) where
- type TabulateOb (arr :: Type -> Type -> Type) i j
- tabulateArr :: TabulateOb arr i j => (i -> j) -> arr i j
- indexArr :: TabulateOb arr i j => arr i j -> i -> j
- reindex :: forall (arr :: Type -> Type -> Type) (s' :: [Nat]) (s :: [Nat]) a. LiftFun arr => IxMap s' s -> ArrayC arr s a -> ArrayC arr s' a
- batch :: forall arr a b (s :: [Nat]). Category arr => arr a b -> ArrayC arr s a -> ArrayC arr s b
- tabulateC :: forall (arr :: Type -> Type -> Type) (s :: [Nat]) a. (Tabular arr, TabulateOb arr (Fins s) a) => (Fins s -> a) -> ArrayC arr s a
- indexC :: forall (arr :: Type -> Type -> Type) (s :: [Nat]) a. (Tabular arr, TabulateOb arr (Fins s) a) => ArrayC arr s a -> Fins s -> a
- allFins :: forall (s :: [Nat]). KnownNats s => [Fins s]
Indexing category
type IxMap (s' :: [Nat]) (s :: [Nat]) = Fins s' -> Fins s Source #
A morphism in the indexing category I: a map between shape indices.
Array category carrier
newtype ArrayC (arr :: Type -> Type -> Type) (s :: [Nat]) a Source #
Arrays in the array category [C; I].
An array of shape s with values in object a is a morphism
Fins s -> a in the base category arr.
Instances
| Applicative (ArrayC (->) s) Source # | |
Defined in Circuit.Mat.Array Methods pure :: a -> ArrayC (->) s a # (<*>) :: ArrayC (->) s (a -> b) -> ArrayC (->) s a -> ArrayC (->) s b # liftA2 :: (a -> b -> c) -> ArrayC (->) s a -> ArrayC (->) s b -> ArrayC (->) s c # (*>) :: ArrayC (->) s a -> ArrayC (->) s b -> ArrayC (->) s b # (<*) :: ArrayC (->) s a -> ArrayC (->) s b -> ArrayC (->) s a # | |
| Functor (ArrayC (->) s) Source # | |
Base-category support
class Category arr => LiftFun (arr :: Type -> Type -> Type) where Source #
Lift a plain function to a morphism in the base category.
For functions this is the identity; for matrices it is the Fun
constructor.
class Category arr => Tabular (arr :: Type -> Type -> Type) where Source #
Categories that can represent a functional relation i -> j as a
morphism and recover it.
The Mat r instance builds a matrix with a single one in each row
and recovers the function by looking for that one. It therefore
requires the matrix to be functional.
Methods
tabulateArr :: TabulateOb arr i j => (i -> j) -> arr i j Source #
indexArr :: TabulateOb arr i j => arr i j -> i -> j Source #
Instances
| Tabular (Mat r) Source # | |||||
Defined in Circuit.Mat.Array Methods tabulateArr :: TabulateOb (Mat r) i j => (i -> j) -> Mat r i j Source # indexArr :: TabulateOb (Mat r) i j => Mat r i j -> i -> j Source # | |||||
| Tabular (->) Source # | |||||
Defined in Circuit.Mat.Array Associated Types
Methods tabulateArr :: TabulateOb (->) i j => (i -> j) -> i -> j Source # indexArr :: TabulateOb (->) i j => (i -> j) -> i -> j Source # | |||||
Array-category operations
reindex :: forall (arr :: Type -> Type -> Type) (s' :: [Nat]) (s :: [Nat]) a. LiftFun arr => IxMap s' s -> ArrayC arr s a -> ArrayC arr s' a Source #
Reindexing morphism [X; η].
Precompose with an indexing morphism. This is exactly harpie's
backpermute, renamed to match the paper.
batch :: forall arr a b (s :: [Nat]). Category arr => arr a b -> ArrayC arr s a -> ArrayC arr s b Source #
Batch lift [f; P].
Apply a base morphism at every index of the array.
tabulateC :: forall (arr :: Type -> Type -> Type) (s :: [Nat]) a. (Tabular arr, TabulateOb arr (Fins s) a) => (Fins s -> a) -> ArrayC arr s a Source #
Separator / tabulation: build an array from a function on indices.
This is the separator Sp of the paper, mapping the presheaf
representation back to an array object.
indexC :: forall (arr :: Type -> Type -> Type) (s :: [Nat]) a. (Tabular arr, TabulateOb arr (Fins s) a) => ArrayC arr s a -> Fins s -> a Source #
Join / lookup: recover the function on indices from an array.
This is the join Jn of the paper.
Finite support for shape indices
allFins :: forall (s :: [Nat]). KnownNats s => [Fins s] Source #
All indices of a statically-known shape.