Safe Haskell	None
Language	GHC2024

Circuit.Mat.Harpie

Contents

KnownNat wrapper
Coproduct isomorphism
Matrices indexed by F

Description

Harpie-backed finite indices for Circuit.Mat.

Harpie shapes are rectangular products of type-level naturals; there is no native shape constructor for coproducts. This module provides the minimal bridge: a KnownNat-indexed wrapper F n around Harpie.Shape.Fin n, with a Finite instance, so that matrices can use harpie-style type-level sizes while reusing the existing Mat machinery.

The central isomorphism is the standard disjoint-union-as-initial-segment:

Either (F i) (F j)  ≅  F (i + j)

realised by eitherToF and fToEither. This lets the biproduct parH embed block-diagonally into a single rectangular harpie dimension, and lets traceF reuse traceMat on a feedback channel whose size is known at the type level.

Synopsis

newtype F (n :: Nat) = F {
- unF :: Fin n
}
finF :: forall (n :: Nat). KnownNat n => Int -> F n
safeFinF :: forall (n :: Nat). KnownNat n => Int -> Maybe (F n)
fromF :: forall (n :: Nat). F n -> Fin n
toF :: forall (n :: Nat). Fin n -> F n
eitherToF :: forall (i :: Nat) (j :: Nat). (KnownNat i, KnownNat j) => Either (F i) (F j) -> F (i + j)
fToEither :: forall (i :: Nat) (j :: Nat). (KnownNat i, KnownNat j) => F (i + j) -> Either (F i) (F j)
matF :: forall (i :: Nat) (j :: Nat) s. (KnownNat i, KnownNat j) => (Fin i -> Fin j -> s) -> Mat s (F i) (F j)
runMatF :: forall s (i :: Nat) (j :: Nat). (Additive s, Multiplicative s) => Mat s (F i) (F j) -> Fin i -> Fin j -> s
parH :: forall (i :: Nat) (j :: Nat) (k :: Nat) (l :: Nat) s. (KnownNat i, KnownNat j, KnownNat k, KnownNat l, KnownNat (i + k), KnownNat (j + l), Additive s, Multiplicative s) => Mat s (F i) (F j) -> Mat s (F k) (F l) -> Mat s (F (i + k)) (F (j + l))
traceF :: forall (n :: Nat) s b c. (KnownNat n, StarSemiring s, Additive s, Multiplicative s, Finite b, Finite c) => Mat s (Either (F n) b) (Either (F n) c) -> Mat s b c

KnownNat wrapper

newtype F (n :: Nat) Source #

A KnownNat-backed finite index type.

F n is exactly Fin n, but carries a Finite instance derived from the type-level natural. This is the smallest wrapper that lets Mat treat harpie-style indices as enumerable objects.

Constructors

F
Fields unF :: Fin n

Instances

Instances details

KnownNat n => Finite (F n) Source #	Enumerate all `F n` values. `>>>` `universe :: [F 3]`[0,1,2]
Instance details Defined in Circuit.Mat.Harpie Methods universe :: [F n] Source #
Eq (F n) Source #
Instance details Defined in Circuit.Mat.Harpie Methods (==) :: F n -> F n -> Bool # (/=) :: F n -> F n -> Bool #
Ord (F n) Source #
Instance details Defined in Circuit.Mat.Harpie Methods compare :: F n -> F n -> Ordering # (<) :: F n -> F n -> Bool # (<=) :: F n -> F n -> Bool # (>) :: F n -> F n -> Bool # (>=) :: F n -> F n -> Bool # max :: F n -> F n -> F n # min :: F n -> F n -> F n #
Show (F n) Source #
Instance details Defined in Circuit.Mat.Harpie Methods showsPrec :: Int -> F n -> ShowS # show :: F n -> String # showList :: [F n] -> ShowS #

finF :: forall (n :: Nat). KnownNat n => Int -> F n Source #

Construct an F n from an Int. Errors if out of bounds.

>>> finF @3 2
2

safeFinF :: forall (n :: Nat). KnownNat n => Int -> Maybe (F n) Source #

Construct an F n from an Int safely.

>>> safeFinF @3 2
Just 2
>>> safeFinF @3 3
Nothing

fromF :: forall (n :: Nat). F n -> Fin n Source #

Coerce to the underlying Fin n.

toF :: forall (n :: Nat). Fin n -> F n Source #

Coerce from a Fin n.

Coproduct isomorphism

eitherToF :: forall (i :: Nat) (j :: Nat). (KnownNat i, KnownNat j) => Either (F i) (F j) -> F (i + j) Source #

Disjoint-union embedding into F (i + j).

Left summand occupies indices [0, i); right summand occupies [i, i+j).

>>> eitherToF @2 @3 (Left (finF 1))
1
>>> eitherToF @2 @3 (Right (finF 1))
3

fToEither :: forall (i :: Nat) (j :: Nat). (KnownNat i, KnownNat j) => F (i + j) -> Either (F i) (F j) Source #

Split an F (i + j) into the left or right summand.

>>> fToEither @2 @3 (finF @5 1)
Left 1
>>> fToEither @2 @3 (finF @5 3)
Right 1

Matrices indexed by F

matF :: forall (i :: Nat) (j :: Nat) s. (KnownNat i, KnownNat j) => (Fin i -> Fin j -> s) -> Mat s (F i) (F j) Source #

Build a matrix from a function on underlying Fin indices.

runMatF :: forall s (i :: Nat) (j :: Nat). (Additive s, Multiplicative s) => Mat s (F i) (F j) -> Fin i -> Fin j -> s Source #

Run a matrix at underlying Fin indices.

parH :: forall (i :: Nat) (j :: Nat) (k :: Nat) (l :: Nat) s. (KnownNat i, KnownNat j, KnownNat k, KnownNat l, KnownNat (i + k), KnownNat (j + l), Additive s, Multiplicative s) => Mat s (F i) (F j) -> Mat s (F k) (F l) -> Mat s (F (i + k)) (F (j + l)) Source #

Block-diagonal biproduct for harpie-backed indices.

The result lives on a single rectangular dimension F (i + k) × F (j + l), matching what a harpie Array [i + k, j + l] s@ expects.

>>> let m = matF @2 @2 (\i j -> if i == j then (1 :: Int) else 0)
>>> let n = matF @1 @1 (\_ _ -> (7 :: Int))
>>> runMat (parH m n) (eitherToF (Left (finF @2 1))) (eitherToF (Left (finF @2 1)))
1
>>> runMat (parH m n) (eitherToF (Right (finF @1 0))) (eitherToF (Right (finF @1 0)))
7
>>> runMat (parH m n) (eitherToF (Left (finF @2 0))) (eitherToF (Right (finF @1 0)))
0

traceF :: forall (n :: Nat) s b c. (KnownNat n, StarSemiring s, Additive s, Multiplicative s, Finite b, Finite c) => Mat s (Either (F n) b) (Either (F n) c) -> Mat s b c Source #

Trace over a feedback channel of known size.

This is just traceMat with the Finite dictionary supplied by the KnownNat n constraint on F n.

>>> let fFun (Left (F (UnsafeFin 0))) (Left (F (UnsafeFin 0))) = False; fFun (Left (F (UnsafeFin 0))) (Right (F (UnsafeFin 0))) = True; fFun (Right (F (UnsafeFin 0))) (Left (F (UnsafeFin 0))) = True; fFun _ _ = False
>>> let f = Mat fFun :: Mat Bool (Either (F 2) (F 1)) (Either (F 2) (F 1))
>>> runMat (traceF f) (finF @1 0) (finF @1 0)
True