{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

{-
Dimensional.hs

Gregory Price (price mit.edu)
2003-11-12
lightly edited 2007-11-19 for a SIPB cluedump

Sadly, this seems to trigger a bug in GHC 6.8.1.  Try 6.6.
-}

module Dimensional where

import qualified List

-- Our type-level integers.
import Peano(UnPeano, unPeano, PNum(PNum), Zero, One, MOne)
import qualified Peano as N

infixl 7 <*>, </>
infixl 6 <+>, <->

{- The data types of dimensionalities and dimensional quantities, a
function to turn a dimensionality into a tuple of integers, and a
convenience function for operating on the underlying numbers in the
quantities.  -}

data Dimension pMass pLength pTime = Dm
data DimlQty num d = DQ d num
--data DimlZero = DZ

class UnDimension d where
    unDimension :: d -> (Int,Int,Int)
instance (UnPeano m, UnPeano l, UnPeano t) => UnDimension (Dimension m l t) where
    unDimension Dm = (unPeano (PNum::PNum m),
                      unPeano (PNum::PNum l),
                      unPeano (PNum::PNum t))

-- Dangerous!
lift2 :: (a -> b -> c) -> (DimlQty a d1 -> DimlQty b d2 -> DimlQty c (Dimension m l t))
lift2 f = \ (DQ _ a) (DQ _ b) ->
          DQ Dm $ f a b



{-
  The computational meat of the module -- multiplication and division.
  Looks simple because Peano.Add and Peano.Sub are doing all the work.                                       
-}

(<*>) :: (Num        n, N.Add m1 m2 m3, N.Add l1 l2 l3, N.Add t1 t2 t3) => 
         DimlQty n (Dimension m1 l1 t1) -> DimlQty n (Dimension m2 l2 t2) -> DimlQty n (Dimension m3 l3 t3)
(</>) :: (Fractional n, N.Sub m1 m2 m3, N.Sub l1 l2 l3, N.Sub t1 t2 t3) => 
         DimlQty n (Dimension m1 l1 t1) -> DimlQty n (Dimension m2 l2 t2) -> DimlQty n (Dimension m3 l3 t3)
(<*>) = lift2 (*)
(</>) = lift2 (/)


{-
  Trivial operations -- addition and subtraction, and instances of Eq and Ord.
-}


(<+>) :: Num n => DimlQty n (Dimension m l t) -> DimlQty n (Dimension m l t) -> DimlQty n (Dimension m l t)
(<->) :: Num n => DimlQty n (Dimension m l t) -> DimlQty n (Dimension m l t) -> DimlQty n (Dimension m l t)
(<+>) = lift2 (+)
(<->) = lift2 (-)


instance Eq  n => Eq  (DimlQty n (Dimension m l t)) where
    (DQ _ a) == (DQ _ b) = a == b
instance Ord n => Ord (DimlQty n (Dimension m l t)) where
    (DQ _ a) <= (DQ _ b) = a <= b



{-
  Constants: zero, one, units, and a few physical constants.
  Also a function `dm' to make a dimensionless number from a plain number.
-}

dm :: n -> DimlQty n (Dimension Zero Zero Zero)
dm = DQ Dm

zero :: Num n => DimlQty n (Dimension m l t)
one  :: Num n => DimlQty n (Dimension Zero Zero Zero)
kg   :: Num n => DimlQty n (Dimension  One Zero Zero)
m    :: Num n => DimlQty n (Dimension Zero  One Zero)
s    :: Num n => DimlQty n (Dimension Zero Zero  One)
zero = DQ Dm 0
one  = DQ Dm 1
kg   = DQ Dm 1 
m    = DQ Dm 1
s    = DQ Dm 1


{- The type signatures here are because of a bizarre dark corner of
Haskell -- when it let-binds the values, it monomorphizes the numeric
type unless a type signature on the outside says otherwise.  The
problem has nothing to do with this code -- try

  > :t 1
  1 :: forall t. (Num t) => t

  > let l = 1
  > :t l
  l :: Integer

  > let l :: (forall n. (Num n) => n) = 1
  > :t l
  l :: Integer

  > let l :: (forall n. (Num n) => n); l = 1
  > :t l
  l :: forall n. (Num n) => n

in your interactive toplevel.

The ugliness in the definition of Einstein's constant is needed only
because I choose to keep the type constraint at Num rather than
Fractional, which means eschewing (/) and hence (</>).  So I need an
explicit s^-1 value, which doesn't seem worth the namespace cost of
putting at top level.  This is really an issue with (/), and one that
doesn't seem likely to be a problem very often outside of this
context.  -}

gGravity   :: Fractional n => DimlQty n (Dimension Zero One (N.P (N.P N.Z)))
cEinstein  ::        Num n => DimlQty n (Dimension Zero One MOne)
hbarPlanck :: Fractional n => DimlQty n (Dimension  One (N.S (N.S N.Z)) (N.P N.Z))
gGravity   = dm 9.8              <*> m       </> s </> s
cEinstein  = dm 299792458        <*> m       <*> DQ (Dm::Dimension Zero Zero (N.P N.Z)) 1
hbarPlanck = dm 1.05457e-34   <*> kg <*> m <*> m </> s




{-
  Instances of Show, with some helper functions.
-}


showsPower :: String -> Int -> String -> String
showsPower x n | n ==  0 = id
               | n ==  1 = (++"*"++x)
               | n >   1 = (++"*"++x++"^"++show n)
               | n == -1 = (++"/"++x)
               | n <  -1 = (++"/"++x++"^"++show (negate n))

showPower :: String -> Int -> String
showPower x n | n ==  0 = "1"
              | n ==  1 = x
              | True    = x++"^"++show n

showMonomial :: [(String, Int)] -> String
showMonomial [] = "1"
showMonomial m  = concat $ List.intersperse " * " $ 
                  map (\(x,n) -> showPower x n) $ 
                  filter (\ (_,n) -> n /= 0) $
                  m

instance UnDimension (Dimension m l t) => Show (Dimension m l t) where
    show d = showMonomial [("kg", m),
                           ("m",  l),
                           ("s",  t)]
        where (m, l, t) = unDimension d
                             
instance (Show n, Show d) => Show (DimlQty n d) where
    show (DQ d n) = show n ++ dimstr
      where dimstr = case show d of
                     "1" -> ""
                     s   -> " "++s






{-
  Demo.
-}

lambdaGreen = dm 550e-9 <*> m

main :: IO ()
main = do putStr $ "h-bar is " ++ show hbarPlanck ++ "\n"
          putStr $ "the speed of light is " ++ show cEinstein ++ "\n"
          putStr $ "green light has wavelength about "
                     ++ show lambdaGreen ++ "\n"
          putStr $ "so a green photon has energy about "
                     ++ show (hbarPlanck <*> cEinstein </> lambdaGreen) ++ "\n"