1. Thijs Alkemade
  2. haskell-unittyped

Commits

Thijs Alkemade  committed 5f696eb

Simplified some dimension definitions, added tests.

Added (~.) for `coerce`.

  • Participants
  • Parent commits 93b7062
  • Branches default

Comments (0)

Files changed (6)

File src/UnitTyped.hs

View file
 
 data Number = Zero | Neg Nat | Pos Nat
 
-type Two = Pos (Suc One)
-type Three = Pos (Suc (Suc One))
+type POne = Pos One
+type PTwo = Pos (Suc One)
+type PThree = Pos (Suc (Suc One))
+type PFour = Pos (Suc (Suc (Suc One)))
+
+type NOne = Neg One
+type NTwo = Neg (Suc One)
+type NThree = Neg (Suc (Suc One))
+type MFour = Neg (Suc (Suc (Suc One)))
 
 -- These two are useful for Add
 
 coerce :: (Convertable a b, Convertable c d, Fractional f, UnitEq a c True) => Value f a b -> Value f c d -> Value f c d
 coerce u _ = let result = mkVal (factor u * val u / factor result) in result
 
+infixl 5 ~.
+
+(~.) :: (Convertable a b, Convertable c d, Fractional f, UnitEq a c True) => Value f a b -> Value f c d -> Value f c d
+(~.) = coerce
+
 data Mul b d
 
 data Div b d

File src/UnitTyped/SI/Constants.hs

View file
 c = mkVal 299792458
 
 -- planck constant
-h :: (Fractional f) => Value f (UnitCons Time (Neg One) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) UnitNil))) (Mul Joule Second)
+h :: (Fractional f) => Value f (UnitCons Time NOne (UnitCons Length PTwo (UnitCons Mass POne UnitNil))) (Mul Joule Second)
 h = mkVal 6.6260695729e-34
 
 -- atomic unit of action
-hbar :: (Fractional f, Floating f) => Value f (UnitCons Time (Neg One) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) UnitNil))) (Mul Joule Second)
+hbar :: (Fractional f, Floating f) => Value f (UnitCons Time NOne (UnitCons Length PTwo (UnitCons Mass POne UnitNil))) (Mul Joule Second)
 hbar = coerce (h ./. (2 .$. UnitTyped.SI.Constants.pi)) (joule .*. second)
 
 -- atomic unit of charge (elementary charge)
 e_h :: (Fractional f) => Value f Energy Joule
 e_h = mkVal 4.3597441775e-18
 
-r :: (Fractional f) => Value f (UnitCons Temperature (Neg One) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) (UnitCons Time (Neg (Suc One)) UnitNil)))) (Div Joule (Mul Kelvin Mole))
+r :: (Fractional f) => Value f (UnitCons Temperature NOne (UnitCons Length PTwo (UnitCons Mass POne (UnitCons Time (Neg (Suc One)) UnitNil)))) (Div Joule (Mul Kelvin Mole))
 r = mkVal 8.314462175

File src/UnitTyped/SI/Derived.hs

View file
 
 import Data.Ratio
 
-type Speed = UnitCons Time (Neg One) (UnitCons Length (Pos One) UnitNil)
-type Acceleration = UnitCons Time (Neg (Suc One)) (UnitCons Length (Pos One) UnitNil)
+type Speed = UnitCons Time NOne (UnitCons Length POne UnitNil)
+type Acceleration = UnitCons Time NTwo (UnitCons Length POne UnitNil)
 
 
 data Knot
 
 --
 
-type Force = UnitCons Time (Neg (Suc One)) (UnitCons Mass (Pos One) (UnitCons Length (Pos One) UnitNil))
+type Force = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length POne UnitNil))
 data Newton
 
 instance Convertable Force Newton where
 
 --
 
-type Energy = UnitCons Time (Neg (Suc One)) (UnitCons Mass (Pos One) (UnitCons Length (Pos (Suc One)) UnitNil))
+type Energy = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length PTwo UnitNil))
 
 data Joule
 
 
 --
 
-type Power = UnitCons Time (Neg (Suc (Suc One))) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) UnitNil))
+type Power = UnitCons Time NThree (UnitCons Length PTwo (UnitCons Mass POne UnitNil))
 
 data Watt
 
 
 --
 
-type Pressure = UnitCons Time (Neg (Suc One)) (UnitCons Mass (Pos One) (UnitCons Length (Neg One) UnitNil))
+type Pressure = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length NOne UnitNil))
 
 data Pascal
 
 
 --
 
-type Charge = (UnitCons Time (Pos One) (UnitCons Current (Pos One) UnitNil))
+type Charge = (UnitCons Time POne (UnitCons Current POne UnitNil))
 
 data Coulomb
 
 
 --
 
-type Potential = (UnitCons Current (Neg One) (UnitCons Mass (Pos One) (UnitCons Length (Pos (Suc One)) (UnitCons Time (Neg (Suc (Suc One))) UnitNil))))
+type Potential = (UnitCons Current NOne (UnitCons Mass POne (UnitCons Length PTwo (UnitCons Time NThree UnitNil))))
 
 data Volt
 
 
 --
 
-type Capacitance = (UnitCons Current (Pos (Suc One)) (UnitCons Mass (Neg One) (UnitCons Length (Neg (Suc One)) (UnitCons Time (Pos (Suc (Suc (Suc One)))) UnitNil))))
+type Capacitance = (UnitCons Current PTwo (UnitCons Mass NOne (UnitCons Length NTwo (UnitCons Time PFour UnitNil))))
 
 data Farad
 
 
 --
 
-type Resistance = (UnitCons Current (Neg (Suc One)) (UnitCons Time (Neg (Suc (Suc One))) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) UnitNil))))
+type Resistance = (UnitCons Current NTwo (UnitCons Time NThree (UnitCons Length PTwo (UnitCons Mass POne UnitNil))))
 
 data Ohm
 
 
 --
 
-type Conductance = (UnitCons Current (Pos (Suc One)) (UnitCons Mass (Neg One) (UnitCons Length (Neg (Suc One)) (UnitCons Time (Pos (Suc (Suc One))) UnitNil))))
+type Conductance = (UnitCons Current PTwo (UnitCons Mass NOne (UnitCons Length NTwo (UnitCons Time PThree UnitNil))))
 
 data Siemens
 
 
 --
 
-type Flux = (UnitCons Current (Neg One) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) (UnitCons Time (Neg (Suc One)) UnitNil))))
+type Flux = (UnitCons Current NOne (UnitCons Length PTwo (UnitCons Mass POne (UnitCons Time NTwo UnitNil))))
 
 data Weber
 
 
 --
 
-type FluxDensity = (UnitCons Length (Neg One) (UnitCons Time (Neg (Suc One)) (UnitCons Mass (Pos One) (UnitCons Current (Neg One) UnitNil))))
+type FluxDensity = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Current NOne UnitNil))
 
 data Tesla
 
 
 --
 
-type Inductance = (UnitCons Current (Neg (Suc One)) (UnitCons Time (Neg (Suc One)) (UnitCons Mass (Pos One) (UnitCons Length (Pos (Suc One)) UnitNil))))
+type Inductance = (UnitCons Current NTwo (UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length PTwo UnitNil))))
 
 data Henry
 

File src/UnitTyped/SI/Derived/Time.hs

View file
 	showunit _ _ = "a"
 
 
-data Herz
+data Hertz
 
-instance Convertable (UnitCons Time (Neg One) UnitNil) Herz where
+instance Convertable (UnitCons Time (Neg One) UnitNil) Hertz where
 	factor _ = 1
 	showunit _ _ = "Hz"
 
 month :: (Fractional f) => Value f TimeUnit Month
 month = one
 
-herz :: (Fractional f) => Value f (UnitCons Time (Neg One) UnitNil) Herz
-herz = one
+hertz :: (Fractional f) => Value f (UnitCons Time (Neg One) UnitNil) Hertz
+hertz = one

File tests/TestSI.hs

View file
+{-# LANGUAGE KindSignatures, DataKinds, MultiParamTypeClasses, FunctionalDependencies, ExistentialQuantification, TypeFamilies #-}
+module Main where
+
+import UnitTyped
+import UnitTyped.SI
+import UnitTyped.SI.Derived
+import UnitTyped.SI.Derived.Length
+import UnitTyped.SI.Derived.Mass
+import UnitTyped.SI.Derived.Count
+import UnitTyped.SI.Derived.Time
+import UnitTyped.SI.Meta
+import UnitTyped.Bytes
+import UnitTyped.Currency
+import UnitTyped.NoPrelude
+
+import qualified Prelude
+import Control.Monad (foldM, unless)
+import Prelude (zip, show, (++), IO, Bool(..), Integer, return, error, putStrLn)
+import System.Exit (exitFailure)
+
+t1 = hertz == (count / second)
+t2 = rad == (meter / meter)
+t3 = newton == kilo gram * meter / square second
+t4 = pascal == newton / square meter
+t5 = joule == newton * meter
+t6 = watt == joule / second
+t7 = coulomb == second * ampere
+t8 = volt == watt / ampere
+t9 = farad == coulomb / volt
+t10 = ohm == volt / ampere
+t11 = siemens == count / ohm
+t12 = weber == joule / ampere
+t13 = tesla == volt * second / square meter
+t14 = henry == volt * second / ampere
+
+t15 = 3.6 kilo meter / hour == 1 meter / second
+t16 = 3.6 mega joule == 1 kilo watt * hour
+
+runTest :: Bool -> (Bool, Integer) -> IO Bool
+runTest b (True, _) = return b
+runTest b (False, i) = do { putStrLn ("Test " ++ show i ++ " failed.")
+		   				  ; return False
+						  }
+
+main = do { b <- foldM runTest True (zip [t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16] [1..])
+		  ; unless b exitFailure
+		  }

File unittyped.cabal

View file
 version:        0.1
 author:         Thijs Alkemade
 license:        GPL
-Cabal-Version:  >= 1.2
+Cabal-Version:  >= 1.8
 build-type:     Simple
 synopsis:       A type-safe open-world library for computations including units.
 
                    ScopedTypeVariables,
                    FlexibleContexts,
                    OverlappingInstances,
-                   GADTs
+                   GADTs,
+                   EmptyDataDecls
   exposed-modules: UnitTyped,
                    UnitTyped.NoPrelude,
                    UnitTyped.SI,
                    UnitTyped.SI.Derived.Time,
                    UnitTyped.SI.Derived.Mass
   hs-source-dirs:  src
+
+Test-Suite test-si
+    type:          exitcode-stdio-1.0
+    main-is:       tests/TestSI.hs
+    build-depends: base == 4.6.0.0, unittyped