module Dim3 where
default (Double)
infixl 7 ***
infixl 6 +++

data Zero = Zero
data Succ x = Succ x

class Peano a where
  value :: a -> Int
  element :: a
instance Peano Zero where
  value Zero = 0 ; element = Zero
instance (Peano a) => Peano (Succ a) where
  value (Succ x) = value x + 1 ; element = Succ element

class (Peano a, Peano b, Peano c) => PeanoAdd a b c | a b -> c
instance (Peano a) => PeanoAdd Zero a a
instance (PeanoAdd a b c) => PeanoAdd (Succ a) b (Succ c)

data (Peano a) => Dim a b = Dim a b deriving (Eq)

class Mul a b c | a b -> c where (***) :: a -> b -> c
instance Mul Double Double Double where (***) = (*)
instance (Mul a b c, PeanoAdd d e f) => Mul (Dim d a) (Dim e b) (Dim f c) where
  (Dim _ a) *** (Dim _ b) = Dim element (a *** b)
instance (Show a, Peano b) => Show (Dim b a) where
  show (Dim b a) = show a ++ " d^" ++ show (value b)

class Additive a where
  (+++) :: a -> a -> a
  zero :: a
instance Additive Double where
  (+++) = (+) ; zero = 0
instance (Peano a, Additive b) => Additive (Dim a b) where
  Dim a b +++ Dim c d = Dim a (b+++d)
  zero = Dim element zero

scalar :: Double -> Dim Zero Double
scalar x = Dim Zero x
unit = scalar 1.0
d = Dim (Succ Zero) 1.0

f (x,y,z) = x***x +++ y***y***y +++ z***z***z***z***z