matrix.hs

{-# 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)