{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Prelude hiding (sum,head,tail,map,zipWith,foldr,foldl)


data a :. b = !a :. !b
  deriving (Eq,Ord,Read,Show)

infixr :.

class Det' a m | m -> a where
  det' :: m -> a

--base case for 2x2
instance Num a => Det' a ((a:.a:.()):.(a:.a:.()):.()) where
  det' ( (a:.b:.()) :. (c:.d:.()) :. () ) = a*d-b*c



------------------------
-- Overlapping instance (works in 6.8 & 6.10)
{-
instance
    (Num a
    ,Fold a v
    ,Num v
    ,Head m v
    ,Vec n a v
    ,Map m__ a vm v
    ,Transpose vmt vm
    ,DropConsec v vv
    ,Map v vv m_ vmt
    ,Tail m m_
    ,Alternating n a v
    ,Det' a m__
    )
    => Det' a m
  where
    det' m =
      sum ((alternating undefined 1) * (head m) *
           (map det' (transpose(map(dropConsec)(tail m)))))
-}

---------------------
-- Non-overlapping instance (works in 6.8)

instance
    (Num a
    ,Num (a:.a:.a:.v)
    ,Fold a (a:.a:.a:.v)
    ,Alternating (Succ (Succ (Succ n))) a (a:.a:.a:.v)
    ,DropConsec (a:.a:.a:.v) vv
    ,Map (a:.a:.a:.v) vv ((a:.a:.a:.v):.(a:.a:.a:.v):.m) vmt
    ,Transpose vmt vm
    ,Map ((a:.a:.v):.(a:.a:.v):.m_) a vm (a:.a:.a:.v)
    ,Det' a ((a:.a:.v):.(a:.a:.v):.m_)
    ,Vec (Succ (Succ (Succ n))) a (a:.a:.a:.v)
    ,Vec (Succ (Succ (Succ n))) (a:.a:.a:.v) ((a:.a:.a:.v):.(a:.a:.a:.v):.(a:.a:.a:.v):.m)
    )
     => 
    Det' a ((a:.a:.a:.v):.(a:.a:.a:.v):.(a:.a:.a:.v):.m)
  where
    det' (mh:.mt) =
      sum ((alternating undefined 1) * mh *
          (map det' (transpose (map dropConsec mt :: vmt))))












det :: forall n a r m. (Vec n a r, Vec n r m, Det' a m) => m -> a
det = det'



-- Vector type. Matrices are vectors of vectors.


data N0
data Succ a

class Pred x y | x -> y, y -> x
instance Pred (Succ N0) N0
instance Pred (Succ n) p => Pred (Succ (Succ n)) (Succ p)

type N1  = Succ N0
type N2  = Succ N1
type N3  = Succ N2
type N4  = Succ N3
type N5  = Succ N4



class Vec n a v | n a -> v, v -> n a where
  mkVec :: n -> a -> v

instance Vec N1 a ( a :. () ) where
  mkVec _ a = a :. ()

instance Vec (Succ n) a (a':.v) => Vec (Succ (Succ n)) a (a:.a':.v) where
  mkVec _ a = a :. (mkVec undefined a)



  
class Head v a | v -> a  where 
  head :: v -> a
instance Head (a :. as) a where 
  head (a :. _) = a


class Tail v v_ | v -> v_ where 
  tail :: v -> v_
instance Tail (a :. as) as where 
  tail (_ :. as) = as




class Map a b u v | u -> a, v -> b, b u -> v, a v -> u where
  map :: (a -> b) -> u -> v
instance Map a b (a :. ()) (b :. ()) where
  map f (x :. ()) = (f x) :. ()
instance Map a b (a':.u) (b':.v) => Map a b (a:.a':.u) (b:.b':.v) where
  map f (x:.v) = (f x):.(map f v)




class ZipWith a b c u v w | u->a, v->b, w->c, u v c -> w where
  zipWith :: (a -> b -> c) -> u -> v -> w
instance ZipWith a b c (a:.()) (b:.()) (c:.()) where
  zipWith f (x:._) (y:._) = f x y :.()
instance ZipWith a b c (a:.()) (b:.b:.bs) (c:.()) where
  zipWith f (x:._) (y:._) = f x y :.()
instance ZipWith a b c (a:.a:.as) (b:.()) (c:.()) where
  zipWith f (x:._) (y:._) = f x y :.()
instance 
  ZipWith a b c (a':.u) (b':.v) (c':.w) 
  => ZipWith a b c (a:.a':.u) (b:.b':.v) (c:.c':.w) 
    where
      zipWith f (x:.u) (y:.v) = f x y :. zipWith f u v



class Fold a v | v -> a where
  fold  :: (a -> a -> a) -> v -> a
instance Fold a (a:.()) where
  fold  f   (a:._) = a 
instance Fold a (a':.u) => Fold a (a:.a':.u) where
  fold  f   (a:.v) = (f a) (fold f v)

sum ::  (Fold a v, Num a) => v -> a
sum x = fold (+) x






class Transpose a b | a -> b, b -> a where 
  transpose :: a -> b

instance Transpose () () where
  transpose = id

instance 
    (Vec (Succ n) s (s:.ra)  --(s:ra) is an n-vector of s'es (row of a)
    ,Vec (Succ m) (s:.ra) ((s:.ra):.a)  --a is an m-vector of ra's
    ,Vec (Succ m) s (s:.rb)  --rb is an m-vector of s'es (row of b)
    ,Vec (Succ n) (s:.rb) ((s:.rb):.b)  --b is an n-vector of rb's
    ,Transpose' ((s:.ra):.a) ((s:.rb):.b)
    )
    => Transpose ((s:.ra):.a) ((s:.rb):.b)
  where
    transpose = transpose'






class Transpose' a b | a->b
  where transpose' :: a -> b

instance Transpose' () () where 
  transpose' = id

instance 
    (Transpose' vs vs') => Transpose' ( () :. vs ) vs'
  where
    transpose' (():.vs) = transpose' vs

instance Transpose' ((x:.()):.()) ((x:.()):.()) where
  transpose' = id

instance 
    (Head xss_h xss_hh
    ,Map xss_h xss_hh (xss_h:.xss_t) xs'
    ,Tail xss_h xss_ht
    ,Map xss_h xss_ht (xss_h:.xss_t) xss_
    ,Transpose' (xs :. xss_) xss'
    )
    => Transpose' ((x:.xs):.(xss_h:.xss_t)) ((x:.xs'):.xss') 
  where
    transpose' ((x:.xs):.xss) =
      (x :. (map head xss)) :. (transpose' (xs :. (map tail xss) :: (xs:.xss_)))






class DropConsec v vv | v -> vv where
  dropConsec :: v -> vv

instance 
  (Vec n a v
  ,Pred n n_
  ,Vec n_ a v_
  ,Vec n v_ vv
  ,DropConsec' () v vv
  ) => DropConsec v vv
  where
    dropConsec v = dropConsec' () v 

class DropConsec' p v vv  where
  dropConsec' :: p -> v -> vv
    
instance DropConsec' p (a:.()) (p:.()) where
  dropConsec' p (a:.()) = (p:.())

instance 
    (Append p (a:.v) x
    ,Append p (a:.()) y
    ,DropConsec' y (a:.v) z
    ) 
    => DropConsec' p (a:.a:.v) (x:.z)
  where
    dropConsec' p (a:.v) = 
      (append p v) :. (dropConsec' (append p (a:.())) v)





class Alternating n a v | v -> n a where
  alternating :: n -> a -> v

instance Alternating N1 a (a:.()) where
  alternating _ a = a:.()

instance (Num a, Alternating n a (a:.v)) => Alternating (Succ n) a (a:.a:.v) where
  alternating _ a = a:.(alternating (undefined::n) (negate a))






class Append v1 v2 v3 | v1 v2 -> v3, v1 v3 -> v2 where 
  append :: v1 -> v2 -> v3

instance Append () v v where
  append _ = id

instance Append (a:.()) v (a:.v) where
  append (a:.()) v = a:.v

instance (Append (a':.v1) v2 v3) => Append (a:.a':.v1) v2 (a:.v3) where
  append (a:.u) v  =  a:.(append u v)





instance
    (Eq (a:.u)
    ,Show (a:.u)
    ,Num a
    ,Map a a (a:.u) (a:.u) 
    ,ZipWith a a a (a:.u) (a:.u) (a:.u)
    ,Vec (Succ l) a (a:.u)
    )
    => Num (a:.u) 
  where
    (+) u v = zipWith (+) u v 
    (-) u v = zipWith (-) u v
    (*) u v = zipWith (*) u v
    abs u = map abs u
    signum u = map signum u
    fromInteger i = mkVec undefined (fromInteger i)