BlockMatrix.hs

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators #-}
module BlockMatrix where

import GHC.TypeLits

data Block (n :: Nat) (m :: Nat) a where
  Number :: a -> Block 1 1 a
  Fourths :: Block n1 m1 a -> Block n1 m2 a -> Block n2 m1 a -> Block n2 m2 a -> Block (n1 + n2) (m1 + m2) a
  Vhalves :: Block n m1 a -> Block n m2 a -> Block n (m1 + m2) a
  Hhalves :: Block n1 m a -> Block n2 m a -> Block (n1 + n2) m a

i4 :: Block 2 2 Double
i4 = Hhalves col1 col2
  where
  col1 :: Block 1 2 Double
  col1 = Vhalves x11 x21
    where
    x11 :: Block 1 1 Double
    x11 = Number 1

    x21 :: Block 1 1 Double
    x21 = Number 0

  col2 :: Block 1 2 Double
  col2 = Vhalves x12 x22
    where
    x12 :: Block 1 1 Double
    x12 = Number 0

    x22 :: Block 1 1 Double
    x22 = Number 1