Skip to content

Instantly share code, notes, and snippets.

@oisdk oisdk/matrix.hs
Created Dec 27, 2019

Embed
What would you like to do?
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, NoStarIsType #-}
{-# OPTIONS_GHC -Wall -fno-warn-unticked-promoted-constructors #-}
import Data.Monoid (Sum(..))
import Data.Kind (Type)
data Nat = Z | S Nat
data Fin (n :: Nat) where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
type (|*|) (n :: Nat) (m :: Nat) (a :: Type) = Fin n -> Fin m -> a
ident :: Num a => (n |*| m) a
ident FZ FZ = 1
ident FZ (FS _) = 0
ident (FS _) FZ = 0
ident (FS n) (FS m) = ident n m
class Finite n where
summarise :: Monoid a => (Fin n -> a) -> a
instance Finite Z where
summarise _ = mempty
instance Finite n => Finite (S n) where
summarise f = f FZ <> summarise (f . FS)
sigma :: (Finite n, Num a) => (Fin n -> a) -> a
sigma f = getSum (summarise (Sum . f))
mult :: (Finite n, Num a) => (m |*| n) a -> (n |*| p) a -> (m |*| p) a
mult a b i j = sigma (\k -> a i k * b k j)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.