Commits

Thijs Alkemade committed 2dbbf8e

Added a shorthand for singleton lists with value POne.
Made all proxies empty datatypes.
Implemented prettier notation for higher power units.

  • Participants
  • Parent commits fa87175

Comments (0)

Files changed (11)

File src/UnitTyped.hs

 {-# LANGUAGE DataKinds, ScopedTypeVariables, TypeFamilies #-}
 -- |Module defining values with dimensions and units, and mathematical operations on those.
 module UnitTyped (
-	Convertible(..), Convertible'(..),
+	Convertible(..), Convertible'(..), Unit(..),
 	Value(..), ValueProxy(..), proxy',
 
 	Count,
 
 -- |A value tagged with its dimension a and unit b.
 data Value f (a :: [(*, Number)]) (b :: [(*, Number)]) = Value f
-data ValueProxy (a :: [(*, Number)]) b = ValueProxy
-data ValueProxy' (a :: [(*, Number)]) (b :: [(*, Number)]) = ValueProxy'
-data NumberProxy (a :: Number) = NumberProxy
+data ValueProxy (a :: [(*, Number)]) b
+data ValueProxy' (a :: [(*, Number)]) (b :: [(*, Number)])
+data NumberProxy (a :: Number)
 
 proxy' :: (Convertible' a b) => Value f a b -> ValueProxy' a b
-proxy' _ = ValueProxy'
+proxy' _ = undefined
 
 class FromNumber (a :: Number) where
 	fromNumber :: NumberProxy a -> Integer
 	fromNumber _ = 1
 
 instance (FromNumber (Pos a)) => FromNumber (Pos (Suc a)) where
-	fromNumber _ = 1 + (fromNumber (NumberProxy :: NumberProxy (Pos a)))
+	fromNumber _ = 1 + (fromNumber (undefined :: NumberProxy (Pos a)))
 
 instance FromNumber (Neg One) where
 	fromNumber _ = -1
 
 instance (FromNumber (Neg a)) => FromNumber (Neg (Suc a)) where
-	fromNumber _ = -1 + (fromNumber (NumberProxy :: NumberProxy (Neg a)))
+	fromNumber _ = -1 + (fromNumber (undefined :: NumberProxy (Neg a)))
 
+-- |Convertible is a class that models the fact that the simple unit 'b' has dimension 'a'.
 class Convertible (a :: [(*, Number)]) b | b -> a where
 	factor :: (Fractional f) => ValueProxy a b -> f
-	showunit :: (Fractional f) => ValueProxy a b -> String
+	showunit :: ValueProxy a b -> String
 
--- |Convertible is a class that models the fact that the unit 'b' has dimension 'a' (of kind '[(*, Number)]').
+type Unit a = '[ '(a, POne) ]
+
+-- |Convertible' is a class that models the fact that the composed unit 'b' has dimension 'a'.
 class Convertible' (a :: [(*, Number)]) (b :: [(*, Number)]) where
 	-- |The multiplication factor to convert this unit between other units in the same dimension.
 	-- Only the ratio matters, which one is '1' is not important, as long as all are consistent.
 	factor' :: (Fractional f) => ValueProxy' a b -> f
 	-- |String representation of a unit. The boolean determines wether to use brackets (only important for the denomiator).
 	-- The value should not be important for the output, its only here because it needs to be a class method.
-	showunit' :: (Fractional f) => ValueProxy' a b -> String
+	showunit' :: ValueProxy' a b -> String
 
 --instance Convertible' '[] '[] where
 --	factor' _ = 1
 --	showunit' _ = ""
 
 instance (Convertible a b, MapEq a a' True) => Convertible' a' ('(b, POne) ': '[]) where
-	factor' _ = factor (ValueProxy :: ValueProxy a b)
-	showunit' _ = showunit (ValueProxy :: ValueProxy a b)
+	factor' _ = factor (undefined :: ValueProxy a b)
+	showunit' _ = showunit (undefined :: ValueProxy a b)
 
 instance (FromNumber value, Convertible' rec_dimension rest, MapNeg unit_dimension neg_unit_dimension,
 		  MapTimes value neg_unit_dimension times_neg_unit_dimension, MapMerge times_neg_unit_dimension dimension rec_dimension,
 		  Convertible unit_dimension unit) => Convertible' dimension ('(unit, value) ': rest) where
 	factor' _ = let
-					rec = factor' (ValueProxy' :: ValueProxy' rec_dimension rest)
-				in rec * ((factor (ValueProxy :: ValueProxy unit_dimension unit)) ^^ (fromNumber (NumberProxy :: NumberProxy value)))
+					rec = factor' (undefined :: ValueProxy' rec_dimension rest)
+				in rec * ((factor (undefined :: ValueProxy unit_dimension unit)) ^^ (fromNumber (undefined :: NumberProxy value)))
 	showunit' _ = let
-					rec = showunit' (ValueProxy' :: ValueProxy' rec_dimension rest)
-					power = fromNumber (NumberProxy :: NumberProxy value)
-				  in (if null rec then "" else rec) ++ (if (not $ null rec) && (power /= 0) then "⋅" else "") ++ (if power /= 0 then (showunit (ValueProxy :: ValueProxy a'' unit)) ++ (if power /= 1 then "^" ++ show power else "") else "")
+					rec = showunit' (undefined :: ValueProxy' rec_dimension rest)
+					power = fromNumber (undefined :: NumberProxy value)
+				  in (if null rec then "" else rec) ++ (if (not $ null rec) && (power /= 0) then "⋅" else "") ++ (if power /= 0 then (showunit (undefined :: ValueProxy a'' unit)) ++ if power /= 1 then show_power power else "" else "")
 
+show_power 1 = "¹"
+show_power 2 = "²"
+show_power 3 = "³"
+show_power 4 = "⁴"
+show_power 5 = "⁵"
+show_power 6 = "⁶"
+show_power 7 = "⁷"
+show_power 8 = "⁸"
+show_power 9 = "⁹"
+show_power n
+	| n < 0 = "⁻" ++ (show_power (-n))
+	| otherwise = (show_power (n `div` 10)) ++ (show_power (n `mod` 10))
 
 instance (Fractional f, Show f, Convertible' a b) => Show (Value f a b) where
 	show u = show (val u) ++ " " ++ showunit' (proxy' u)
 
 -- |Calculate @x^(-3)@.
 pown3 :: (Fractional f, Convertible' a b, Pow a b NThree c d) => Value f a b -> Value f c d
-pown3 = pow (NumberProxy :: NumberProxy NThree)
+pown3 = pow (undefined :: NumberProxy NThree)
 
 -- |Calculate @x^(-2)@.
 pown2 :: (Fractional f, Convertible' a b, Pow a b NTwo c d) => Value f a b -> Value f c d
-pown2 = pow (NumberProxy :: NumberProxy NTwo)
+pown2 = pow (undefined :: NumberProxy NTwo)
 
 -- |Calculate @x^(-1)@.
 pown1 :: (Fractional f, Convertible' a b, Pow a b NOne c d) => Value f a b -> Value f c d
-pown1 = pow (NumberProxy :: NumberProxy NOne)
+pown1 = pow (undefined :: NumberProxy NOne)
 
 -- |Calculate @x^0@. Yes, this is always @one :: Value f ('[] Count@.
 pow0 :: (Fractional f, Convertible' a b, Pow a b Zero c d) => Value f a b -> Value f c d
-pow0 = pow (NumberProxy :: NumberProxy Zero)
+pow0 = pow (undefined :: NumberProxy Zero)
 
 -- |Calculate @x^1@.
 pow1 :: (Fractional f, Convertible' a b, Pow a b POne c d) => Value f a b -> Value f c d
-pow1 = pow (NumberProxy :: NumberProxy POne)
+pow1 = pow (undefined :: NumberProxy POne)
 
 -- |Calculate @x^2@.
 pow2 :: (Fractional f, Convertible' a b, Pow a b PTwo c d) => Value f a b -> Value f c d
-pow2 = pow (NumberProxy :: NumberProxy PTwo)
+pow2 = pow (undefined :: NumberProxy PTwo)
 
 -- |Calculate @x^3@.
 pow3 :: (Fractional f, Convertible' a b, Pow a b PThree c d) => Value f a b -> Value f c d
-pow3 = pow (NumberProxy :: NumberProxy PThree)
+pow3 = pow (undefined :: NumberProxy PThree)
 
 -- |Calculate @x^4@.
 pow4 :: (Fractional f, Convertible' a b, Pow a b PFour c d) => Value f a b -> Value f c d
-pow4 = pow (NumberProxy :: NumberProxy PFour)
+pow4 = pow (undefined :: NumberProxy PFour)
 
 -- |Calculate @x^5@.
 pow5 :: (Fractional f, Convertible' a b, Pow a b PFive c d) => Value f a b -> Value f c d
-pow5 = pow (NumberProxy :: NumberProxy PFive)
+pow5 = pow (undefined :: NumberProxy PFive)
 
 -- |Calculate @x^6@.
 pow6 :: (Fractional f, Convertible' a b, Pow a b PSix c d) => Value f a b -> Value f c d
-pow6 = pow (NumberProxy :: NumberProxy PSix)
+pow6 = pow (undefined :: NumberProxy PSix)
 
 wrapB :: (Convertible' a b, Convertible' c d, MapEq c a True) => (Rational -> Rational -> Bool) -> Value Rational a b -> Value Rational c d -> Bool
 wrapB op a b = op (val a) (val $ coerce b a)

File src/UnitTyped/Bytes.hs

 -- |An of amount of data.
 data Data
 -- |The dimension representing @Data^1@.
-type DataUnit = '[ '(Data, POne) ]
+type DataDimension = '[ '(Data, POne) ]
 
 -- |A byte of data.
 data Byte
 
-instance Convertible DataUnit Byte where
+instance Convertible DataDimension Byte where
 	factor _ = 1
 	showunit _ = "B"
 
 -- |A bit of data.
 data Bit
 
-instance Convertible DataUnit Bit where
+instance Convertible DataDimension Bit where
 	factor _ = 0.125
 	showunit _ = "b"
 
 --
 
 -- |One byte.
-byte :: (Fractional f) => Value f DataUnit '[ '(Byte, POne) ]
+byte :: (Fractional f) => Value f DataDimension (Unit Byte)
 byte = one
 
 -- |One bit.
-bit :: (Fractional f) => Value f DataUnit '[ '(Bit, POne) ]
+bit :: (Fractional f) => Value f DataDimension (Unit Bit)
 bit = one

File src/UnitTyped/NoPrelude.hs

 -- |Calculate the tangens of a value. Works on 'Degree' and 'Radian'.
 tan = wrap1 Prelude.tan
 
-wrap2 :: (Floating f) => (f -> f) -> Value f '[] '[] -> Value f '[] '[ '(Radian, POne) ]
+wrap2 :: (Floating f) => (f -> f) -> Value f '[] '[] -> Value f '[] (Unit Radian)
 wrap2 op v = op (val v) ~> one
 
-asin, acos, atan :: (Floating f) => Value f '[] '[] -> Value f '[] '[ '(Radian, POne) ]
+asin, acos, atan :: (Floating f) => Value f '[] '[] -> Value f '[] (Unit Radian)
 -- |Calculate the arcsinus of a value. Always computes 'Radian's.
 asin = wrap2 Prelude.asin
 -- |Calculate the arccosinus of a value. Always computes 'Radian's.

File src/UnitTyped/SI.hs

 --
 
 -- |One meter (m).
-meter :: (Fractional f) => Value f LengthDimension '[ '(Meter, POne) ]
+meter :: (Fractional f) => Value f LengthDimension (Unit Meter)
 meter = one
 
 --
 
 -- |One second (s).
-second :: (Fractional f) => Value f TimeDimension '[ '(Second, POne) ]
+second :: (Fractional f) => Value f TimeDimension (Unit Second)
 second = one
 
 --
 
 -- |One gram (g).
-gram :: (Fractional f) => Value f MassDimension '[ '(Gram, POne) ]
+gram :: (Fractional f) => Value f MassDimension (Unit Gram)
 gram = one
 
 --
 
 -- |One Kelvin (K).
-kelvin :: (Fractional f) => Value f TemperatureDimension '[ '(Kelvin, POne) ]
+kelvin :: (Fractional f) => Value f TemperatureDimension (Unit Kelvin)
 kelvin = one
 
 --
 
 -- |One ampere (A).
-ampere :: (Fractional f) => Value f CurrentDimension '[ '(Ampere, POne) ]
+ampere :: (Fractional f) => Value f CurrentDimension (Unit Ampere)
 ampere = one
 
 --
 
 -- |One candela (cd).
-candela :: (Fractional f) => Value f LuminousDimension '[ '(Candela, POne) ]
+candela :: (Fractional f) => Value f LuminousDimension (Unit Candela)
 candela = one

File src/UnitTyped/SI/Constants.hs

 hbar = coerce (h ./. (2 ~> UnitTyped.SI.Constants.pi)) (joule .*. second)
 
 -- |Atomic unit of charge (elementary charge)
-e :: (Fractional f) => Value f Charge '[ '(Coulomb, POne) ]
+e :: (Fractional f) => Value f Charge (Unit Coulomb)
 e = mkVal 1.6021765314e-19
 
 -- |Atomic unit of mass (electron mass)
-m_e :: (Fractional f) => Value f MassDimension '[ '((Kilo Gram), POne) ]
+m_e :: (Fractional f) => Value f MassDimension (Unit (Kilo Gram))
 m_e = mkVal 9.109382616e-31
 
 -- |Atomic unit of length
-a_0 :: (Fractional f) => Value f LengthDimension '[ '(Meter, POne) ]
+a_0 :: (Fractional f) => Value f LengthDimension (Unit Meter)
 a_0 = mkVal 0.529177210818e-10
 
 -- |Atomic unit of energy
-e_h :: (Fractional f) => Value f Energy '[ '(Joule, POne) ]
+e_h :: (Fractional f) => Value f Energy (Unit Joule)
 e_h = mkVal 4.3597441775e-18
 
 -- |Gas constant.
 g = mkVal 6.6738480e-11
 
 ---- |Planck mass
---m_P :: (Fractional f, Floating f) => Value f MassDimension '[ '((Kilo Gram), POne) ]
+--m_P :: (Fractional f, Floating f) => Value f MassDimension (Unit (Kilo Gram))
 --m_P = mkVal (sqrt (val $ hbar .*. c ./. g))
 
 ---- |Reduced Planck mass
---m_P' :: (Fractional f, Floating f) => Value f MassDimension '[ '((Kilo Gram), POne) ]
+--m_P' :: (Fractional f, Floating f) => Value f MassDimension (Unit (Kilo Gram))
 --m_P' = mkVal (sqrt (val $ hbar .*. c ./. ((Prelude.pi * 8) ~> g)))

File src/UnitTyped/SI/Derived.hs

 --
 
 -- |One knot.
-knot :: (Fractional f) => Value f Speed '[ '(Knot, POne) ]
+knot :: (Fractional f) => Value f Speed (Unit Knot)
 knot = one
 
 -- |One newton.
-newton :: (Fractional f) => Value f '[ '(Time, NTwo), '(Mass, POne), '(Length, POne)] '[ '(Newton, POne) ]
+newton :: (Fractional f) => Value f '[ '(Time, NTwo), '(Mass, POne), '(Length, POne)] (Unit Newton)
 newton = one
 
 -- |One joule.
-joule :: (Fractional f) => Value f Energy '[ '(Joule, POne) ]
+joule :: (Fractional f) => Value f Energy (Unit Joule)
 joule = one
 
 -- |One eV.
-eV :: (Fractional f) => Value f Energy '[ '(Ev, POne) ]
+eV :: (Fractional f) => Value f Energy (Unit Ev)
 eV = one
 
 -- |One kwh.
 kwh = one
 
 -- |One watt.
-watt :: (Fractional f) => Value f Power '[ '(Watt, POne) ]
+watt :: (Fractional f) => Value f Power (Unit Watt)
 watt = one
 
 -- |One pascal.
-pascal :: (Fractional f) => Value f Pressure '[ '(Pascal, POne) ]
+pascal :: (Fractional f) => Value f Pressure (Unit Pascal)
 pascal = one
 
 -- |One bar.
-bar :: (Fractional f) => Value f Pressure '[ '(Bar, POne) ]
+bar :: (Fractional f) => Value f Pressure (Unit Bar)
 bar = one
 
 -- |One mmHg.
-mmHg :: (Fractional f) => Value f Pressure '[ '(MmHg, POne) ]
+mmHg :: (Fractional f) => Value f Pressure (Unit MmHg)
 mmHg = one
 
 -- |One coulomb.
-coulomb :: (Fractional f) => Value f Charge '[ '(Coulomb, POne) ]
+coulomb :: (Fractional f) => Value f Charge (Unit Coulomb)
 coulomb = one
 
 -- |One volt.
-volt :: (Fractional f) => Value f Potential '[ '(Volt, POne) ]
+volt :: (Fractional f) => Value f Potential (Unit Volt)
 volt = one
 
 -- |One farad.
-farad :: (Fractional f) => Value f Capacitance '[ '(Farad, POne) ]
+farad :: (Fractional f) => Value f Capacitance (Unit Farad)
 farad = one
 
 -- |One ohm.
-ohm :: (Fractional f) => Value f Resistance '[ '(Ohm, POne) ]
+ohm :: (Fractional f) => Value f Resistance (Unit Ohm)
 ohm = one
 
 -- |One siemens.
-siemens :: (Fractional f) => Value f Conductance '[ '(Siemens, POne) ]
+siemens :: (Fractional f) => Value f Conductance (Unit Siemens)
 siemens = one
 
 -- |One weber.
-weber :: (Fractional f) => Value f Flux '[ '(Weber, POne) ]
+weber :: (Fractional f) => Value f Flux (Unit Weber)
 weber = one
 
 -- |One tesla.
-tesla :: (Fractional f) => Value f FluxDensity '[ '(Tesla, POne) ]
+tesla :: (Fractional f) => Value f FluxDensity (Unit Tesla)
 tesla = one
 
 -- |One henry.
-henry :: (Fractional f) => Value f Inductance '[ '(Henry, POne) ]
+henry :: (Fractional f) => Value f Inductance (Unit Henry)
 henry = one

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

 --
 
 -- |One percent (%).
-percent :: (Fractional f) => Value f '[] '[ '(Percentage, POne) ]
+percent :: (Fractional f) => Value f '[] (Unit Percentage)
 percent = one
 
 -- |One per mille (‰).
-permil :: (Fractional f) => Value f '[] '[ '(Permil, POne) ]
+permil :: (Fractional f) => Value f '[] (Unit Permil)
 permil = one
 
 -- |One part per million (ppm).
-ppm :: (Fractional f) => Value f '[] '[ '(Ppm, POne) ]
+ppm :: (Fractional f) => Value f '[] (Unit Ppm)
 ppm = one
 
 -- |One part per billion (ppb).
-ppb :: (Fractional f) => Value f '[] '[ '(Ppb, POne) ]
+ppb :: (Fractional f) => Value f '[] (Unit Ppb)
 ppb = one
 
 -- |One part per trillion (ppt).
-ppt :: (Fractional f) => Value f '[] '[ '(Ppt, POne) ]
+ppt :: (Fractional f) => Value f '[] (Unit Ppt)
 ppt = one
 
 -- |One rad (rad).
-rad :: (Fractional f) => Value f '[] '[ '(Radian, POne) ]
+rad :: (Fractional f) => Value f '[] (Unit Radian)
 rad = one
 
 -- |One degree (˚).
-deg :: (Fractional f) => Value f '[] '[ '(Degree, POne) ]
+deg :: (Fractional f) => Value f '[] (Unit Degree)
 deg = one

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

 --
 
 -- |One mile (mile).
-mile :: (Fractional f) => Value f LengthDimension '[ '(Mile, POne) ]
+mile :: (Fractional f) => Value f LengthDimension (Unit Mile)
 mile = one
 
 -- |One inch (in).
-inch :: (Fractional f) => Value f LengthDimension '[ '(Inch, POne) ]
+inch :: (Fractional f) => Value f LengthDimension (Unit Inch)
 inch = one
 
 -- |One yard (yd).
-yard :: (Fractional f) => Value f LengthDimension '[ '(Yard, POne) ]
+yard :: (Fractional f) => Value f LengthDimension (Unit Yard)
 yard = one
 
 -- |One foot (ft).
-foot :: (Fractional f) => Value f LengthDimension '[ '(Foot, POne) ]
+foot :: (Fractional f) => Value f LengthDimension (Unit Foot)
 foot = one
 
-ångström, angstrom :: (Fractional f) => Value f LengthDimension '[ '(Ångström, POne) ]
+ångström, angstrom :: (Fractional f) => Value f LengthDimension (Unit Ångström)
 -- |One ångström (Å).
 ångström = one
 -- |One ångström, for those with bad UTF-8 support (Å).
 angstrom = one
 
 -- |One nautical mile (M).
-nautical_mile :: (Fractional f) => Value f LengthDimension '[ '(NauticalMile, POne) ]
+nautical_mile :: (Fractional f) => Value f LengthDimension (Unit NauticalMile)
 nautical_mile = one
 
 --
 
 -- |One barn (b).
-barn :: (Fractional f) => Value f AreaUnit '[ '(Barn, POne) ]
+barn :: (Fractional f) => Value f AreaUnit (Unit Barn)
 barn = one
 
 --
 
 -- |One liter (L).
-liter :: (Fractional f) => Value f VolumeUnit '[ '(Liter, POne) ]
+liter :: (Fractional f) => Value f VolumeUnit (Unit Liter)
 liter = one
 
 -- |One gallon (gallon).
-gallon :: (Fractional f) => Value f VolumeUnit '[ '(Gallon, POne) ]
+gallon :: (Fractional f) => Value f VolumeUnit (Unit Gallon)
 gallon = one
 
 -- |One fluid ounce (fl oz).
-fluid_ounce :: (Fractional f) => Value f VolumeUnit '[ '(FluidOunce, POne) ]
+fluid_ounce :: (Fractional f) => Value f VolumeUnit (Unit FluidOunce)
 fluid_ounce = one

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

 --
 
 -- |One pound (lb).
-pound :: (Fractional f) => Value f MassDimension '[ '(Pound, POne) ]
+pound :: (Fractional f) => Value f MassDimension (Unit Pound)
 pound = one

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

 --
 
 -- |One minute (min.).
-minute :: (Fractional f) => Value f TimeDimension '[ '(Minute, POne) ]
+minute :: (Fractional f) => Value f TimeDimension (Unit Minute)
 minute = one
 
 -- |One hour (h).
-hour :: (Fractional f) => Value f TimeDimension '[ '(Hour, POne) ]
+hour :: (Fractional f) => Value f TimeDimension (Unit Hour)
 hour = one
 
 -- |One day (day).
-day :: (Fractional f) => Value f TimeDimension '[ '(Day, POne) ]
+day :: (Fractional f) => Value f TimeDimension (Unit Day)
 day = one
 
 -- |One year (yr).
-year :: (Fractional f) => Value f TimeDimension '[ '(Year, POne) ]
+year :: (Fractional f) => Value f TimeDimension (Unit Year)
 year = one
 
 -- |One Julian year (a).
-julian_year :: (Fractional f) => Value f TimeDimension '[ '(JulianYear, POne) ]
+julian_year :: (Fractional f) => Value f TimeDimension (Unit JulianYear)
 julian_year = one
 
 -- |One month (month).
-month :: (Fractional f) => Value f TimeDimension '[ '(Month, POne) ]
+month :: (Fractional f) => Value f TimeDimension (Unit Month)
 month = one
 
 -- |One herz (Hz).
-hertz :: (Fractional f) => Value f '[ '(Time, NOne) ] '[ '(Hertz, POne) ]
+hertz :: (Fractional f) => Value f '[ '(Time, NOne) ] (Unit Hertz)
 hertz = one
 
 --
 -- Interaction with Data.Time
 
 -- |Convert a 'DT.DiffTime' into a value in seconds.
-fromDiffTime :: (Fractional f) => DT.DiffTime -> Value f TimeDimension '[ '(Second, POne) ]
+fromDiffTime :: (Fractional f) => DT.DiffTime -> Value f TimeDimension (Unit Second)
 fromDiffTime = mkVal . fromRational . toRational
 
 -- |Convert a 'DTC.NominalDiffTime' into a value in seconds.
-fromNominalDiffTime :: (Fractional f) => DTC.NominalDiffTime -> Value f TimeDimension '[ '(Second, POne) ]
+fromNominalDiffTime :: (Fractional f) => DTC.NominalDiffTime -> Value f TimeDimension (Unit Second)
 fromNominalDiffTime = mkVal . fromRational . toRational
 
 -- |Convert the number of seconds since a given 'DTC.UTCTime' into a value in seconds.
-since :: (Fractional f) => DTC.UTCTime -> IO (Value f TimeDimension '[ '(Second, POne) ])
+since :: (Fractional f) => DTC.UTCTime -> IO (Value f TimeDimension (Unit Second))
 since time = do { t <- DTC.getCurrentTime
 		        ; return (fromNominalDiffTime (DTC.diffUTCTime t time) `as` second)
 		        }
 
 -- |Calculate the number of seconds since a given date and\/or time, parsed according to the first argument.
-since_str :: (Fractional f) => String -> String -> IO (Value f TimeDimension '[ '(Second, POne) ])
+since_str :: (Fractional f) => String -> String -> IO (Value f TimeDimension (Unit Second))
 since_str fmt str = since (DTF.readTime SL.defaultTimeLocale fmt str)

File src/UnitTyped/SI/Meta.hs

 -- Meta-units
 ----
 
-data MetaProxy m a b = MetaProxy
+data MetaProxy m a b
 
 class (Convertible a b) => MetaUnit (m :: * -> *) a b where
 	metafactor :: (Fractional f) => MetaProxy m a b -> f
 	metashow :: (Fractional f) => MetaProxy m a b -> String
 
 instance (MetaUnit m a b, Convertible a b) => Convertible a (m b) where
-	factor _ = metafactor (MetaProxy :: MetaProxy m a b) * factor (ValueProxy :: ValueProxy a b)
-	showunit v = metashow (MetaProxy :: MetaProxy m a b) ++ showunit (ValueProxy :: ValueProxy a b)
+	factor _ = metafactor (undefined :: MetaProxy m a b) * factor (undefined :: ValueProxy a b)
+	showunit v = metashow (undefined :: MetaProxy m a b) ++ showunit (undefined :: ValueProxy a b)
 
 --
 
 ----
 
 -- |Take a unit and return one deca(unit).
-deca :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Deca b), POne) ]
+deca :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Deca b))
 deca _ = one
 
 -- |Take a unit and return one hecto(unit).
-hecto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Hecto b), POne) ]
+hecto :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Hecto b))
 hecto _ = one
 
 -- |Take a unit and return one kilo(unit).
-kilo :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Kilo b), POne) ]
+kilo :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Kilo b))
 kilo _ = one
 
 -- |Take a unit and return one mega(unit).
-mega :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Mega b), POne) ]
+mega :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Mega b))
 mega _ = one
 
 -- |Take a unit and return one giga(unit).
-giga :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Giga b), POne) ]
+giga :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Giga b))
 giga _ = one
 
 -- |Take a unit and return one tera(unit).
-tera :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Tera b), POne) ]
+tera :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Tera b))
 tera _ = one
 
 -- |Take a unit and return one peta(unit).
-peta :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Peta b), POne) ]
+peta :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Peta b))
 peta _ = one
 
 -- |Take a unit and return one exa(unit).
-exa :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Exa b), POne) ]
+exa :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Exa b))
 exa _ = one
 
 -- |Take a unit and return one zetta(unit).
-zetta :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Zetta b), POne) ]
+zetta :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Zetta b))
 zetta _ = one
 
 -- |Take a unit and return one yotta(unit).
-yotta :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Yotta b), POne) ]
+yotta :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Yotta b))
 yotta _ = one
 
 -- |Take a unit and return one deci(unit).
-deci :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Deci b), POne) ]
+deci :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Deci b))
 deci _ = one
 
 -- |Take a unit and return one centi(unit).
-centi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Centi b), POne) ]
+centi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Centi b))
 centi _ = one
 
 -- |Take a unit and return one mili(unit).
-mili :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Mili b), POne) ]
+mili :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Mili b))
 mili _ = one
 
 -- |Take a unit and return one micro(unit).
-micro :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Micro b), POne) ]
+micro :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Micro b))
 micro _ = one
 
 -- |Take a unit and return one nano(unit).
-nano :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Nano b), POne) ]
+nano :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Nano b))
 nano _ = one
 
 -- |Take a unit and return one pico(unit).
-pico :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Pico b), POne) ]
+pico :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Pico b))
 pico _ = one
 
 -- |Take a unit and return one femto(unit).
-femto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Femto b), POne) ]
+femto :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Femto b))
 femto _ = one
 
 -- |Take a unit and return one atto(unit).
-atto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Atto b), POne) ]
+atto :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Atto b))
 atto _ = one
 
 -- |Take a unit and return one zepto(unit).
-zepto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Zepto b), POne) ]
+zepto :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Zepto b))
 zepto _ = one
 
 -- |Take a unit and return one yocto(unit).
-yocto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Yocto b), POne) ]
+yocto :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Yocto b))
 yocto _ = one
 
 --
 
 -- |Take a unit and return one kibi(unit).
-kibi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Kibi b), POne) ]
+kibi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Kibi b))
 kibi _ = one
 
 -- |Take a unit and return one mebi(unit).
-mebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Mebi b), POne) ]
+mebi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Mebi b))
 mebi _ = one
 
 -- |Take a unit and return one gibi(unit).
-gibi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Gibi b), POne) ]
+gibi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Gibi b))
 gibi _ = one
 
 -- |Take a unit and return one tebi(unit).
-tebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Tebi b), POne) ]
+tebi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Tebi b))
 tebi _ = one
 
 -- |Take a unit and return one pebi(unit).
-pebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Pebi b), POne) ]
+pebi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Pebi b))
 pebi _ = one
 
 -- |Take a unit and return one exbi(unit).
-exbi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Exbi b), POne) ]
+exbi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Exbi b))
 exbi _ = one
 
 -- |Take a unit and return one zebi(unit).
-zebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Zebi b), POne) ]
+zebi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Zebi b))
 zebi _ = one
 
 -- |Take a unit and return one yobi(unit).
-yobi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Yobi b), POne) ]
+yobi :: (Convertible a b, Fractional f) => Value f a (Unit b) -> Value f a (Unit (Yobi b))
 yobi _ = one