{- |
We already have the dynamically checked physical units
provided by "Number.Physical"
and the statically checked ones of the @dimensional@ package of Buckwalter,
which require multi-parameter type classes with functional dependencies.

Here we provide a poor man's approach:
The units are presented by type terms.
There is no canonical form and thus the type checker
can not automatically check for equal units.
However, if two unit terms represent the same unit,
then you can tell the type checker to rewrite one into the other.

You can add more dimensions by introducing more types of class 'C'.

This approach is not entirely safe
because you can write your own flawed rewrite rules.
It is however more safe than with no units at all.
-}

module Algebra.DimensionTerm where

import Prelude hiding (recip)


{- Haddock does not like 'where' clauses before empty declarations -}
class Show a => C a -- where


noValue :: C a => a
noValue :: a
noValue =
   let x :: a
x = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"there is no value of type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
x)
   in  a
x

{- * Type constructors -}

data Scalar  = Scalar
data Mul a b = Mul
data Recip a = Recip
type Sqr   a = Mul a a

appPrec :: Int
appPrec :: Int
appPrec = Int
10

instance Show Scalar where
   show :: Scalar -> [Char]
show Scalar
_ = [Char]
"scalar"

instance (Show a, Show b) => Show (Mul a b) where
   showsPrec :: Int -> Mul a b -> [Char] -> [Char]
showsPrec Int
p Mul a b
x =
      let disect :: Mul a b -> (a,b)
          disect :: Mul a b -> (a, b)
disect Mul a b
_ = (a, b)
forall a. HasCallStack => a
undefined
          (a
y,b
z) = Mul a b -> (a, b)
forall a b. Mul a b -> (a, b)
disect Mul a b
x
      in  Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
appPrec)
            ([Char] -> [Char] -> [Char]
showString [Char]
"mul " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
appPrec a
y ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
             [Char] -> [Char] -> [Char]
showString [Char]
" " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> b -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
appPrec b
z)

instance (Show a) => Show (Recip a) where
   showsPrec :: Int -> Recip a -> [Char] -> [Char]
showsPrec Int
p Recip a
x =
      let disect :: Recip a -> a
          disect :: Recip a -> a
disect Recip a
_ = a
forall a. HasCallStack => a
undefined
      in  Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
appPrec)
            ([Char] -> [Char] -> [Char]
showString [Char]
"recip " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
appPrec (Recip a -> a
forall a. Recip a -> a
disect Recip a
x))


instance C Scalar -- where

instance (C a, C b) => C (Mul a b) -- where

instance (C a) => C (Recip a) -- where


scalar :: Scalar
scalar :: Scalar
scalar = Scalar
forall a. C a => a
noValue

mul :: (C a, C b) => a -> b -> Mul a b
mul :: a -> b -> Mul a b
mul a
_ b
_ = Mul a b
forall a. C a => a
noValue

recip :: (C a) => a -> Recip a
recip :: a -> Recip a
recip a
_ = Recip a
forall a. C a => a
noValue


infixl 7 %*%
infixl 7 %/%

(%*%) :: (C a, C b) => a -> b -> Mul a b
%*% :: a -> b -> Mul a b
(%*%) = a -> b -> Mul a b
forall a b. (C a, C b) => a -> b -> Mul a b
mul

(%/%) :: (C a, C b) => a -> b -> Mul a (Recip b)
%/% :: a -> b -> Mul a (Recip b)
(%/%) a
x b
y = a -> Recip b -> Mul a (Recip b)
forall a b. (C a, C b) => a -> b -> Mul a b
mul a
x (b -> Recip b
forall a. C a => a -> Recip a
recip b
y)


{- * Rewrites -}

applyLeftMul :: (C u0, C u1, C v) => (u0 -> u1) -> Mul u0 v -> Mul u1 v
applyLeftMul :: (u0 -> u1) -> Mul u0 v -> Mul u1 v
applyLeftMul u0 -> u1
_ Mul u0 v
_ = Mul u1 v
forall a. C a => a
noValue
applyRightMul :: (C u0, C u1, C v) => (u0 -> u1) -> Mul v u0 -> Mul v u1
applyRightMul :: (u0 -> u1) -> Mul v u0 -> Mul v u1
applyRightMul u0 -> u1
_ Mul v u0
_ = Mul v u1
forall a. C a => a
noValue
applyRecip :: (C u0, C u1) => (u0 -> u1) -> Recip u0 -> Recip u1
applyRecip :: (u0 -> u1) -> Recip u0 -> Recip u1
applyRecip u0 -> u1
_ Recip u0
_ = Recip u1
forall a. C a => a
noValue

commute :: (C u0, C u1) => Mul u0 u1 -> Mul u1 u0
commute :: Mul u0 u1 -> Mul u1 u0
commute Mul u0 u1
_ = Mul u1 u0
forall a. C a => a
noValue
associateLeft :: (C u0, C u1, C u2) => Mul u0 (Mul u1 u2) -> Mul (Mul u0 u1) u2
associateLeft :: Mul u0 (Mul u1 u2) -> Mul (Mul u0 u1) u2
associateLeft Mul u0 (Mul u1 u2)
_ = Mul (Mul u0 u1) u2
forall a. C a => a
noValue
associateRight :: (C u0, C u1, C u2) => Mul (Mul u0 u1) u2 -> Mul u0 (Mul u1 u2)
associateRight :: Mul (Mul u0 u1) u2 -> Mul u0 (Mul u1 u2)
associateRight Mul (Mul u0 u1) u2
_ = Mul u0 (Mul u1 u2)
forall a. C a => a
noValue
recipMul :: (C u0, C u1) => Recip (Mul u0 u1) -> Mul (Recip u0) (Recip u1)
recipMul :: Recip (Mul u0 u1) -> Mul (Recip u0) (Recip u1)
recipMul Recip (Mul u0 u1)
_ = Mul (Recip u0) (Recip u1)
forall a. C a => a
noValue
mulRecip :: (C u0, C u1) => Mul (Recip u0) (Recip u1) -> Recip (Mul u0 u1)
mulRecip :: Mul (Recip u0) (Recip u1) -> Recip (Mul u0 u1)
mulRecip Mul (Recip u0) (Recip u1)
_ = Recip (Mul u0 u1)
forall a. C a => a
noValue

identityLeft :: C u => Mul Scalar u -> u
identityLeft :: Mul Scalar u -> u
identityLeft Mul Scalar u
_ = u
forall a. C a => a
noValue
identityRight :: C u => Mul u Scalar -> u
identityRight :: Mul u Scalar -> u
identityRight Mul u Scalar
_ = u
forall a. C a => a
noValue
cancelLeft :: C u => Mul (Recip u) u -> Scalar
cancelLeft :: Mul (Recip u) u -> Scalar
cancelLeft Mul (Recip u) u
_ = Scalar
forall a. C a => a
noValue
cancelRight :: C u => Mul u (Recip u) -> Scalar
cancelRight :: Mul u (Recip u) -> Scalar
cancelRight Mul u (Recip u)
_ = Scalar
forall a. C a => a
noValue
invertRecip :: C u => Recip (Recip u) -> u
invertRecip :: Recip (Recip u) -> u
invertRecip Recip (Recip u)
_ = u
forall a. C a => a
noValue
doubleRecip :: C u => u -> Recip (Recip u)
doubleRecip :: u -> Recip (Recip u)
doubleRecip u
_ = Recip (Recip u)
forall a. C a => a
noValue
recipScalar :: Recip Scalar -> Scalar
recipScalar :: Recip Scalar -> Scalar
recipScalar Recip Scalar
_ = Scalar
forall a. C a => a
noValue


{- * Example dimensions -}

{- ** Scalar -}

{- |
This class allows defining instances that are exclusively for 'Scalar' dimension.
You won't want to define instances by yourself.
-}
class C dim => IsScalar dim where
   toScalar :: dim -> Scalar
   fromScalar :: Scalar -> dim

instance IsScalar Scalar where
   toScalar :: Scalar -> Scalar
toScalar = Scalar -> Scalar
forall a. a -> a
id
   fromScalar :: Scalar -> Scalar
fromScalar = Scalar -> Scalar
forall a. a -> a
id


{- ** Basis dimensions -}

data Length      = Length
data Time        = Time
data Mass        = Mass
data Charge      = Charge
data Angle       = Angle
data Temperature = Temperature
data Information = Information

length :: Length
length :: Length
length = Length
forall a. C a => a
noValue

time :: Time
time :: Time
time = Time
forall a. C a => a
noValue

mass :: Mass
mass :: Mass
mass = Mass
forall a. C a => a
noValue

charge :: Charge
charge :: Charge
charge = Charge
forall a. C a => a
noValue

angle :: Angle
angle :: Angle
angle = Angle
forall a. C a => a
noValue

temperature :: Temperature
temperature :: Temperature
temperature = Temperature
forall a. C a => a
noValue

information :: Information
information :: Information
information = Information
forall a. C a => a
noValue


instance Show Length      where show :: Length -> [Char]
show Length
_ = [Char]
"length"
instance Show Time        where show :: Time -> [Char]
show Time
_ = [Char]
"time"
instance Show Mass        where show :: Mass -> [Char]
show Mass
_ = [Char]
"mass"
instance Show Charge      where show :: Charge -> [Char]
show Charge
_ = [Char]
"charge"
instance Show Angle       where show :: Angle -> [Char]
show Angle
_ = [Char]
"angle"
instance Show Temperature where show :: Temperature -> [Char]
show Temperature
_ = [Char]
"temperature"
instance Show Information where show :: Information -> [Char]
show Information
_ = [Char]
"information"

instance C Length      -- where
instance C Time        -- where
instance C Mass        -- where
instance C Charge      -- where
instance C Angle       -- where
instance C Temperature -- where
instance C Information -- where

{- ** Derived dimensions -}

type Frequency = Recip Time

frequency :: Frequency
frequency :: Frequency
frequency = Frequency
forall a. C a => a
noValue


data Voltage = Voltage

type VoltageAnalytical =
        Mul (Mul (Sqr Length) Mass) (Recip (Mul (Sqr Time) Charge))

voltage :: Voltage
voltage :: Voltage
voltage = Voltage
forall a. C a => a
noValue

instance Show Voltage where show :: Voltage -> [Char]
show Voltage
_ = [Char]
"voltage"

instance C Voltage -- where

unpackVoltage :: Voltage -> VoltageAnalytical
unpackVoltage :: Voltage -> VoltageAnalytical
unpackVoltage Voltage
_ = VoltageAnalytical
forall a. C a => a
noValue

packVoltage :: VoltageAnalytical -> Voltage
packVoltage :: VoltageAnalytical -> Voltage
packVoltage VoltageAnalytical
_ = Voltage
forall a. C a => a
noValue