| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Circuit.FinRel
Description
Finite-dimensional linear relations over GF(2).
This is a reference semantics for boolean signal-flow graphs: objects are
natural numbers (encoded as FinObj), morphisms are GF(2)-linear relations
presented as the row space of a matrix with (n+m) columns.
Values are Bool, addition is xor, multiplication is &&. The category
carries the cartesian monoidal structure (,), is traced, and supports the
copydiscardplus/zero generators that Net uses for wiring.
This module is intentionally small and self-contained: it is the minimal reference category needed to decide equality on wiring diagrams over a two- element field.
Synopsis
- data FinObj (n :: Nat) = FinObj
- class KnownDim (a :: k) where
- data FinRel n m = FinRel {}
- finId :: KnownDim a => FinRel a a
- compFinRel :: forall a b c. FinRel b c -> FinRel a b -> FinRel a c
- parFinRel :: FinRel a b -> FinRel c d -> FinRel (a, c) (b, d)
- unitlFinRel :: KnownDim a => FinRel ((), a) a
- unitl'FinRel :: KnownDim a => FinRel a ((), a)
- unitrFinRel :: KnownDim a => FinRel (a, ()) a
- unitr'FinRel :: KnownDim a => FinRel a (a, ())
- swapFinRel :: (KnownDim a, KnownDim b) => FinRel (a, b) (b, a)
- assocFinRel :: (KnownDim a, KnownDim b, KnownDim c) => FinRel ((a, b), c) (a, (b, c))
- assoc'FinRel :: (KnownDim a, KnownDim b, KnownDim c) => FinRel (a, (b, c)) ((a, b), c)
- slideFinRel :: (KnownDim a, KnownDim b, KnownDim c) => FinRel (a, (b, c)) (b, (a, c))
- strengthFinRel :: KnownDim a => FinRel b c -> FinRel (a, b) (a, c)
- traceFinRel :: (KnownDim a, KnownDim b, KnownDim c) => FinRel (a, b) (a, c) -> FinRel b c
- finCopy :: forall (n :: Nat). KnownNat n => FinRel (FinObj n) (FinObj n, FinObj n)
- finDiscard :: forall (n :: Nat). KnownNat n => FinRel (FinObj n) ()
- finPlus :: forall (n :: Nat). KnownNat n => FinRel (FinObj n, FinObj n) (FinObj n)
- finZero :: forall (n :: Nat). KnownNat n => FinRel () (FinObj n)
- finScalar :: forall (n :: Nat). KnownNat n => Bool -> FinRel (FinObj n) (FinObj n)
- wiring :: (KnownDim a, KnownDim b) => (Int -> Int) -> FinRel a b
Objects
data FinObj (n :: Nat) Source #
Object token for a finite-dimensional space of dimension n.
Constructors
| FinObj |
Instances
| KnownNat n => Discard FinRel (FinObj n :: Type) Source # | |
| KnownNat n => Zero FinRel (FinObj n :: Type) Source # | |
| KnownNat n => Copy FinRel (FinObj n) Source # | |
| KnownNat n => Merge FinRel (FinObj n) Source # | |
| KnownNat n => KnownDim (FinObj n :: Type) Source # | |
| Eq (FinObj n) Source # | |
| Ord (FinObj n) Source # | |
Defined in Circuit.FinRel | |
| Show (FinObj n) Source # | |
class KnownDim (a :: k) where Source #
Dimension evidence for objects closed under the (,) tensor.
() has dimension 0, 'FinObj n' has dimension n, and pairs add.
Morphisms
A GF(2)-linear relation n -> m.
Internally a matrix whose rows span the relation:
{ (take n v, drop n v) | v in row space }
The stored dimensions are trusted; the matrix is kept in reduced row echelon form for canonical equality.
Instances
| Copy FinRel () Source # | |
Defined in Circuit.FinRel | |
| Merge FinRel () Source # | |
Defined in Circuit.FinRel | |
| Discard FinRel () Source # | |
Defined in Circuit.FinRel | |
| Zero FinRel () Source # | |
Defined in Circuit.FinRel | |
| KnownNat n => Discard FinRel (FinObj n :: Type) Source # | |
| KnownNat n => Zero FinRel (FinObj n :: Type) Source # | |
| KnownNat n => Copy FinRel (FinObj n) Source # | |
| KnownNat n => Merge FinRel (FinObj n) Source # | |
| Eq (FinRel n m) Source # | |
| Show (FinRel n m) Source # | |
Smart constructors
unitlFinRel :: KnownDim a => FinRel ((), a) a Source #
unitl'FinRel :: KnownDim a => FinRel a ((), a) Source #
unitrFinRel :: KnownDim a => FinRel (a, ()) a Source #
unitr'FinRel :: KnownDim a => FinRel a (a, ()) Source #