From 0b7d9faf4dfa9539a4b862a99ea8a1acd20a2c95 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 8 Jul 2026 16:53:51 -0700
Subject: Add functional matrices

---
 Data/Matrix/Functional.agda | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 Data/Matrix/Functional.agda

(limited to 'Data/Matrix/Functional.agda')

diff --git a/Data/Matrix/Functional.agda b/Data/Matrix/Functional.agda
new file mode 100644
index 0000000..2f9a85d
--- /dev/null
+++ b/Data/Matrix/Functional.agda
@@ -0,0 +1,41 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+open import Algebra using (Semiring)
+
+module Data.Matrix.Functional {c ℓ : Level} (R : Semiring c ℓ) where
+
+open import Data.Bool using (if_then_else_)
+open import Data.Fin using (Fin; _≟_)
+open import Data.Nat using (ℕ)
+open import Data.Vec.Functional using (Vector; head; tail)
+open import Function using (flip)
+open import Relation.Nullary.Decidable using (⌊_⌋)
+
+open Semiring R
+open ℕ
+
+Matrix : ℕ → ℕ → Set c
+Matrix n m = Vector (Vector Carrier m) n
+
+sum : {n : ℕ} → Vector Carrier n → Carrier
+sum {zero} _ = 0#
+sum {suc n} v = head v + sum (tail v)
+
+_⟨*⟩_ : {n : ℕ} → Vector Carrier n → Vector Carrier n → Vector Carrier n
+_⟨*⟩_ v w i = v i * w i
+
+_⟨+⟩_ : {n : ℕ} → Vector Carrier n → Vector Carrier n → Vector Carrier n
+_⟨+⟩_ v w i = v i + w i
+
+_[+]_ : {n m : ℕ} → Matrix n m → Matrix n m → Matrix n m
+_[+]_ v w i = v i ⟨+⟩ w i
+
+_∙_ : {n : ℕ} → Vector Carrier n → Vector Carrier n → Carrier
+_∙_ v w = sum (v ⟨*⟩ w)
+
+_·_ : {n m o : ℕ} → Matrix m o → Matrix n m → Matrix n o
+_·_ A B i j = flip A j ∙ B i
+
+identity : {n : ℕ} → Matrix n n
+identity {n} i j = if ⌊ i ≟ j ⌋ then 1# else 0#
-- 
cgit v1.2.3