Vectors and Matrices type parameterised over their length.

algebra.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
import Prelude hiding (tail, head)
import qualified Data.List as L
import Data.Coerce
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.Zip

class Peano t where
    measure :: Integral a => t -> a
    fromList :: [a] -> SafeList t a

data Zero
data Succ p

type P1 = Succ Zero
type P2 = Succ P1
type P3 = Succ P2
type P4 = Succ P3
type P5 = Succ P4
type P6 = Succ P5
type P7 = Succ P6


take1 :: [a] -> SafeList P1 a
take1 = fromList
take2 :: [a] -> SafeList P2 a
take2 = fromList
take3 :: [a] -> SafeList P3 a
take3 = fromList
take4 :: [a] -> SafeList P4 a
take4 = fromList
take5 :: [a] -> SafeList P5 a
take5 = fromList
take6 :: [a] -> SafeList P6 a
take6 = fromList
take7 :: [a] -> SafeList P7 a
take7 = fromList


peal :: Succ a -> a
peal = undefined

instance Peano Zero where
    measure _ = 0
    fromList _ = empty

instance Peano p => Peano (Succ p) where
    measure x = 1 + (measure.peal) x
    fromList (x:xs) = x `cons` fromList xs

pzero :: Zero
pzero = undefined

psucc :: Peano a => a -> Succ a
psucc = undefined

newtype SafeList p a = List [a]
    deriving (Show, Read, Eq, Ord, Functor, Foldable)

empty :: SafeList Zero a
empty = List []

cons :: a -> SafeList p a -> SafeList (Succ p) a
cons x (List xs) = coerce (x:xs)

uncons :: SafeList (Succ p) a -> (a,SafeList p a)
uncons (toList -> (x:xs)) = coerce (x, xs)

head :: SafeList (Succ p) a -> a
head = fst.uncons

tail :: SafeList (Succ p) a -> SafeList p a
tail (List (_:xs)) = coerce xs

transpose :: Matr m n a -> Matr n m a
transpose = coerce.L.transpose. (coerce :: Matr m n a -> [[a]])

toList :: SafeList m a -> [a]
toList = coerce

toList2 :: Matr m n a -> [[a]]
toList2 = coerce

fromList2 :: (Peano n, Peano m) => [[a]] -> Matr m n a
fromList2 = fromList . map fromList

identity :: (Peano n, Num a) => Matr n n a
identity = fromList . map fromList $ iterate (0:) (1:repeat 0)

class Det t a where
    det :: Num a => t -> a

instance {-# OVERLAPS #-} Det (SafeList P2 (SafeList P2 a)) a where
    det (coerce -> [[a,b],[c,d]]) = a*d - b*c

instance Det (SafeList n (SafeList n a)) a => Det (SafeList (Succ n) (SafeList (Succ n) a)) a where
    det lsts = sum $ do
        (x,m) <- zip (zipWith (*) (cycle [1,-1]) (toList $ fmap head lsts)) (toList . reduceS . fmap tail $ lsts)
        return (x * det m)

reduceS :: SafeList (Succ m) a -> SafeList (Succ m) (SafeList m a)
reduceS = coerce.reduce.toList

reduce :: [a] -> [[a]]
reduce [] = []
reduce (x:xs) = xs : do
    lst <- reduce xs
    return (x:lst)

bajs = bajs

instance {-# OVERLAPS #-} Applicative (SafeList P1) where
    pure x = List [x]
    liftA2 f (head -> a) (head -> b) = pure $ f a b

instance Applicative (SafeList n) => Applicative (SafeList (Succ n)) where
    pure x = cons x $ pure x
    liftA2 f (List as) (List bs) = List $ zipWith f as bs

instance {-# OVERLAPS #-} Monad (SafeList P1) where
    (head -> x) >>= f = f x

instance Monad (SafeList n) => Monad (SafeList (Succ n)) where
    (uncons -> (x,xs)) >>= f = head (f x) `cons` (xs >>= (tail . f))

instance Monad (SafeList n) => MonadZip (SafeList n) where
    mzipWith = liftA2

type Matr m n a = SafeList m (SafeList n a)

mul :: (Num a, Monad (SafeList m), Monad (SafeList r), Monad (SafeList n)) 
    => Matr m r a -> Matr r n a -> Matr m n a
mul xs ys = do
    x <- xs
    return $ do
        y <- transpose ys
        return $ sum $ liftA2 (*) x y

jonas :: (Monad (SafeList a), Monad (SafeList b), Monad (SafeList c)) 
    => Matr b a Int -> Matr c b Int -> SafeList a (SafeList b (SafeList c Int))
jonas xs ys = do
    x <- transpose xs
    return $ do
        y <- ys
        let xx = _ $ pure1 x
        let yy = _ $ pure1 y
        return $ mul (xx :: Matr P3 P1) (yy :: Matr P1 P3)
    --return $ (mul :: Matr P3 P1 Int -> Matr P1 P3 Int -> Matr P3 P3 Int) (fmap pure x) (pure y)

pure1 :: w -> SafeList P1 w
pure1 = pure

j :: Matr P3 P3 Int
j = List [List [1,1,1],List [2,2,2],List [3,3,3]]

j1 :: Matr P3 P3 Int
j1 = List [List [1,2,3],List [4,5,6],List [7,8,9]]

j2 :: Matr P3 P3 Int
j2 = List [List [3,1,3],List [4,1,3],List [5,1,9]]

a :: Matr P2 P3 Int
a = List . map List $ [1,2,4]:[2,6,0]:[]
b :: Matr P3 P4 Int
b = List . map List $ [4,1,4,3]:[0,-1,3,1]:[2,7,5,2]:[]

add :: (Num a, Monad (SafeList m), Monad (SafeList n))
    => Matr m n a -> Matr m n a -> Matr m n a
add xs ys = liftA2 (liftA2 (+)) xs ys

data Nat t where
    Z :: Nat t
    S :: Nat t -> Nat (Succ t)

instance Bounded (Nat Zero) where
    minBound = Z
    maxBound = Z

instance Bounded (Nat t) => Bounded (Nat (Succ t)) where
    minBound = Z
    maxBound = S minBound

instance Enum (Nat Zero) where
    toEnum 0 = Z
    fromEnum Z = 0

instance Enum (Nat t) => Enum (Nat (Succ t)) where
    toEnum 0 = Z
    toEnum n | n > 0 = S (toEnum (n-1))
    fromEnum Z = 0
    fromEnum (S p) = succ (fromEnum p)
    succ Z = S Z
    succ (S p) = S $ succ p
    pred (S Z) = Z
    pred (S p) = S $ pred p

--newtype Elementary n a = E (SafeList n (SafeList n a))
--    deriving (Show, Read, Eq)
--
--mulrow :: (Num a, Monad (SafeList n)) => Nat n -> a -> SafeList n (SafeList n a)
--mulrow (S p) x = (1 `cons` pure 0) `cons` mulrow p x
--
--deriving instance Show (Nat t)