{-# LANGUAGE Haskell2010 , KindSignatures , ScopedTypeVariables , DeriveFunctor #-} __ = __ data Z :: * data S :: * -> * type One = S Z ; one = __ :: One type Two = S One ; two = __ :: Two type Three = S Two ; three = __ :: Three type Four = S Three ; four = __ :: Four type Five = S Four ; five = __ :: Five newtype Matrix m n a = Matrix [[a]] deriving (Eq, Show, Read, Functor) generator :: (Int, Int) -> Double generator (i,j) = case (i,j) of (1,1) -> 9 (2,3) -> 5 _ -> 0 mkMatrix :: (Nat m, Nat n) => m -> n -> ((Int, Int) -> a) -> Matrix m n a mkMatrix m n g = Matrix [[(g (i, j)) | j <- [1..toInt n]] | i <- [1..toInt m]] class Nat a where toInt :: a -> Int instance Nat Z where toInt _ = 0 instance Nat n => Nat (S n) where toInt _ = 1 + toInt (__ :: n) matAt :: (Nat m, Nat n) => Matrix m n a -> (Int, Int) -> a matAt (Matrix cells) (m, n) = cells !! pred m !! pred n matMult :: forall m n o a. (Nat m, Nat n, Nat o, Num a) => Matrix m n a -> Matrix n o a -> Matrix m o a matMult m1 m2 = mkMatrix __ __ (\(i,j) -> sum [at1 i z * at2 z j | z <- [1..toInt (__ :: n)]]) where at1 i j = m1 `matAt` (i,j) at2 i j = m2 `matAt` (i,j) identity dim = mkMatrix dim dim (uncurry \$ \i j -> if i == j then 1 else 0) mconst m n val = mkMatrix m n (const val) dim :: forall m n a. (Nat m, Nat n) => Matrix m n a -> (Int, Int) dim _ = (toInt (__ :: m), toInt (__ :: n)) main = do let m = ((+3) `fmap` identity five) `matMult` mconst five three 8 print \$ dim m print m