Thijs Alkemade avatar Thijs Alkemade committed fa87175

Switched to the automatically lifted lists with tuples, instead of my own map.

Everything seems to work again, except:

- My weird instances for Num were broken, I've removed them.
- Pow doesn't work yet.

Comments (0)

Files changed (14)

 	Count,
 
 	Nat(..), Number(..),
-	MapMerge, MapEq, MapNeg, MapTimes,
+	MapMerge, MapEq, MapNeg, MapTimes, MapStrip,
 	POne, PTwo, PThree, PFour, PFive, PSix,
 	NOne, NTwo, NThree, NFour,
 	
 
 	square, cubic,
 
-	pown3, pown2, pown1, pow0, pow1, pow2, pow3, pow4, pow5, pow6
+	{- pown3, pown2, pown1, pow0, pow1, pow2, pow3, pow4, pow5, pow6 -}
 
 ) where
 
 instance And True False False
 instance And False False False
 
---class Insert unit (value :: Number) (map :: [(*, Number)]) (result :: [(*, Number)]) | unit value map -> result where
---instance Insert unit Zero map map
---instance Insert unit (Pos i) map ('(unit, (Pos i)) ': map)
---instance Insert unit (Neg i) map ('(unit, (Neg i)) ': map)
+class MapStrip (map :: [(*, Number)]) (result :: [(*, Number)]) | map -> result where
+
+instance MapStrip '[] '[]
+instance (MapStrip rec rec_result) => MapStrip ('(unit, Zero) ': rec) rec_result
+instance (MapStrip rec rec_result) => MapStrip ('(unit, (Pos value)) ': rec) ('(unit, (Pos value)) ': rec_result)
+instance (MapStrip rec rec_result) => MapStrip ('(unit, (Neg value)) ': rec) ('(unit, (Neg value)) ': rec_result)
 
 class MapInsert' q unit (value :: Number) (map :: [(*, Number)]) (rest :: [(*, Number)]) | unit value map -> rest where
 
 instance MapInsert' q unit value '[] '[ '(unit, value) ]
 
-instance (Add value value' sum) =>
-		 MapInsert' () unit value ( '(unit, value') ': rest) ( '(unit, sum) ': rest)
+instance (Add value value' sum, unit' ~ unit) =>
+		 MapInsert' () unit value ( '(unit, value') ': rec) ( '(unit', sum) ': rec)
 
 instance (MapInsert' q unit value rest rest', value'' ~ value', unit'' ~ unit') =>
 		 MapInsert' q unit value ( '(unit', value') ': rest) ( '(unit'', value'') ': rest')
 
 class MapInsert unit (value :: Number) (map :: [(*, Number)]) (rest :: [(*, Number)]) where
 
-instance (MapInsert' () unit value map rest) => MapInsert unit value map rest where
+instance (MapInsert' () unit value map inserted, MapStrip inserted stripped) => MapInsert unit value map stripped where
 
 -- |States that merging the first map with the second map produces the third argument.
 -- Merging happens by summing the two values for the same key.
 	-- 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
 
-instance Convertible' '[] '[] where
-	factor' _ = 1
-	showunit' _ = ""
+--instance Convertible' '[] '[] where
+--	factor' _ = 1
+--	showunit' _ = ""
 
-instance (Convertible' rest '[]) => Convertible' ('(a, Zero) ': rest) '[] where
+instance (MapNull a True) => Convertible' a '[] where
 	factor' _ = 1
 	showunit' _ = ""
 
 --	factor' _ = 1
 --	showunit' _ = ""
 
-instance (Convertible a b) => Convertible' a ('(b, POne) ': '[]) where
+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)
 
 instance (FromNumber value, Convertible' rec_dimension rest, MapNeg unit_dimension neg_unit_dimension,
-		  MapTimes value neg_unit_dimension times_neg_unit_dimension, MapMerge dimension times_neg_unit_dimension rec_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 = 1 -- (factor' (ValueProxy' :: ValueProxy' rec_dimension rest))
-				in rec * (factor (ValueProxy :: ValueProxy unit_dimension unit))
+					rec = factor' (ValueProxy' :: ValueProxy' rec_dimension rest)
+				in rec * ((factor (ValueProxy :: ValueProxy unit_dimension unit)) ^^ (fromNumber (NumberProxy :: NumberProxy value)))
 	showunit' _ = let
-					rec = "" -- (showunit' (ValueProxy' :: ValueProxy' rec_dimension rest))
+					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 "")
 
 to :: (Convertible' a b, Convertible' c d, Fractional f, MapEq a c True) => Value f c d -> Value f a b -> Value f c d
 to = flip coerce
 
+infixl 7 .*., ./.
+infixl 6 .+., .-.
+
 -- |Multiply two values, constructing a value with as dimension the product of the dimensions,
 -- and as unit the multplication of the units.
 (.*.) :: (Fractional f, Convertible' a b, Convertible' c d, MapMerge a c u, MapMerge b d s) => Value f a b -> Value f c d -> Value f u s
 -- 
 -- >>> 100 . square meter `as` square yard
 -- 119.59900463010803 yd⋅yd⋅#
-square :: (Fractional f, Convertible' a b, Pow a b PTwo c d) => Value f a b -> Value f c d
-square = pow (NumberProxy :: NumberProxy PTwo)
+square :: (Fractional f, MapMerge c c u, MapMerge d d s, Convertible' c d) => Value f c d -> Value f u s
+square x = x .*. x
 
 -- |Calculate the third power of a value. Identical to pow3, reads better on units:
 -- 
 -- >>> 1 . cubic inch `as` mili liter
 -- 16.387063999999995 mL
-cubic :: (Fractional f, Convertible' a b, Pow a b PThree c d) => Value f a b -> Value f c d
-cubic = pow (NumberProxy :: NumberProxy PThree)
+cubic   :: (Fractional f, MapMerge a c u, MapMerge b d s, MapMerge c c a, MapMerge d d b, Convertible' a b, Convertible' c d) => Value f c d -> Value f u s
+cubic x = x .*. x .*. x
 
 -- |Calculate @x^(-3)@.
 pown3 :: (Fractional f, Convertible' a b, Pow a b NThree c d) => Value f a b -> Value f c d
 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)
 
+infixl 4 .==., .<., .>., .<=., .>=.
+
 (.==.), (.<.), (.>.), (.<=.), (.>=.) :: (Convertible' a b, Convertible' c d, MapEq c a True) => Value Rational a b -> Value Rational c d -> Bool
 -- |'==' for values. Only defined for values with rational contents. Can be used on any two values with the same dimension.
 (.==.) = wrapB (==)

src/UnitTyped/Bytes.hs

 -- |An of amount of data.
 data Data
 -- |The dimension representing @Data^1@.
-type DataUnit = UnitCons Data (Pos One) UnitNil
+type DataUnit = '[ '(Data, POne) ]
 
 -- |A byte of data.
 data Byte
 --
 
 -- |One byte.
-byte :: (Fractional f) => Value f DataUnit (UnitCons Byte POne UnitNil)
+byte :: (Fractional f) => Value f DataUnit '[ '(Byte, POne) ]
 byte = one
 
 -- |One bit.
-bit :: (Fractional f) => Value f DataUnit (UnitCons Bit POne UnitNil)
+bit :: (Fractional f) => Value f DataUnit '[ '(Bit, POne) ]
 bit = one

src/UnitTyped/NoPrelude.hs

 
 import UnitTyped
 import UnitTyped.SI
+import UnitTyped.SI.Meta
 import UnitTyped.SI.Derived.Count
 
 import qualified Prelude
 infixl 7 *, /
 
 -- |See '.*.'
-(*) :: (Fractional f, Convertible' a b, Convertible' c d, UnitMerge a c u, UnitMerge b d s) => Value f a b -> Value f c d -> Value f u s
+(*) :: (Fractional f, Convertible' a b, Convertible' c d, MapMerge a c u, MapMerge b d s) => Value f a b -> Value f c d -> Value f u s
 (*) = (.*.)
 
 -- |See './.'
-(/) :: (Fractional f, Convertible' a b, Convertible' c d, UnitMerge a c' u, UnitNeg c c', UnitNeg d d', UnitMerge b d' s) => Value f a b -> Value f c d -> Value f u s
+(/) :: (Fractional f, Convertible' a b, Convertible' c d, MapMerge a c' u, MapNeg c c', MapNeg d d', MapMerge b d' s) => Value f a b -> Value f c d -> Value f u s
 (/) = (./.)
 
 -- |See '.+.'
-(+) :: (Fractional f, Convertible' a b, Convertible' c d, UnitEq c a True) => Value f a b -> Value f c d -> Value f a b
+(+) :: (Fractional f, Convertible' a b, Convertible' c d, MapEq c a True) => Value f a b -> Value f c d -> Value f a b
 (+) = (.+.)
 
 -- |See '.-.'
-(-) :: (Fractional f, Convertible' a b, Convertible' c d, UnitEq c a True) => Value f a b -> Value f c d -> Value f a b
+(-) :: (Fractional f, Convertible' a b, Convertible' c d, MapEq c a True) => Value f a b -> Value f c d -> Value f a b
 (-) = (.-.)
 
-instance (Fractional f, Convertible' a b, t ~ Value f a b) => (Prelude.Num (Value f a b -> t)) where
-	fromInteger i x = Prelude.fromInteger i ~> x
-	(+) = error "This should not happen"
-	(*) = error "This should not happen"
-	abs = error "This should not happen"
-	signum = error "This should not happen"
-
-instance (Fractional f, Convertible' a b, t ~ Value f a b) => (Fractional (Value f a b -> t)) where
-	fromRational r x = Prelude.fromRational r ~> x
-
-instance (Fractional f, Convertible a (m b), c ~ (Value f a b -> Value f a (UnitCons (m b) POne UnitNil))) => (Prelude.Num ((Value f a b -> Value f a (UnitCons (m b) POne UnitNil)) -> c)) where
-	fromInteger i x y = Prelude.fromInteger i ~> x y
-	(+) = error "This should not happen"
-	(*) = error "This should not happen"
-	abs = error "This should not happen"
-	signum = error "This should not happen"
-
-instance (Fractional f, Convertible a (m b), c ~ (Value f a b -> Value f a (UnitCons (m b) POne UnitNil))) => (Fractional ((Value f a b -> Value f a (UnitCons (m b) POne UnitNil)) -> c)) where
-	fromRational i x y = Prelude.fromRational i ~> x y
-
-wrap1 :: (Floating f, Convertible' NoDimension b) => (f -> f) -> Value f NoDimension b -> Value f NoDimension UnitNil
+wrap1 :: (Floating f, Convertible' '[] b) => (f -> f) -> Value f '[] b -> Value f '[] '[]
 wrap1 op v = op (val $ coerce v rad) ~> one
 
-sin, cos, tan :: (Floating f, Convertible' NoDimension b) => Value f NoDimension b -> Value f NoDimension UnitNil
+sin, cos, tan :: (Floating f, Convertible' '[] b) => Value f '[] b -> Value f '[] '[]
 -- |Calculate the sinus of a value. Works on 'Degree' and 'Radian'.
 sin = wrap1 Prelude.sin
 -- |Calculate the cosinus of a value. Works on 'Degree' and 'Radian'.
 -- |Calculate the tangens of a value. Works on 'Degree' and 'Radian'.
 tan = wrap1 Prelude.tan
 
-wrap2 :: (Floating f) => (f -> f) -> Value f NoDimension UnitNil -> Value f NoDimension (UnitCons Radian POne UnitNil)
+wrap2 :: (Floating f) => (f -> f) -> Value f '[] '[] -> Value f '[] '[ '(Radian, POne) ]
 wrap2 op v = op (val v) ~> one
 
-asin, acos, atan :: (Floating f) => Value f NoDimension UnitNil -> Value f NoDimension (UnitCons Radian POne UnitNil)
+asin, acos, atan :: (Floating f) => Value f '[] '[] -> Value f '[] '[ '(Radian, POne) ]
 -- |Calculate the arcsinus of a value. Always computes 'Radian's.
 asin = wrap2 Prelude.asin
 -- |Calculate the arccosinus of a value. Always computes 'Radian's.
 
 infixl 5 ==, <, <=, >, >=
 
-(==), (<), (<=), (>), (>=) :: (Convertible' a b, Convertible' c d, UnitEq c a 'True) => Value Prelude.Rational a b -> Value Prelude.Rational c d -> Bool
+(==), (<), (<=), (>), (>=) :: (Convertible' a b, Convertible' c d, MapEq c a 'True) => Value Prelude.Rational a b -> Value Prelude.Rational c d -> Bool
 -- |See '.==.'
 (==) = (.==.)
 -- |See '.<.'

src/UnitTyped/SI.hs

 -- |Dimension of length.
 data Length
 -- |The dimension defining @Length^1@.
-type LengthDimension = '[ '(Length, (Pos One))]
+type LengthDimension = '[ '(Length, (Pos One)) ]
 
 --
 
 -- |Dimension of time.
 data Time
 -- |The dimension defining @Time^1@.
-type TimeDimension = '[ '(Time, (Pos One))]
+type TimeDimension = '[ '(Time, (Pos One)) ]
 
 --
 
 -- |Dimension of mass.
 data Mass
 -- |The dimension defining @Mass^1@.
-type MassDimension = '[ '(Mass, (Pos One))]
+type MassDimension = '[ '(Mass, (Pos One)) ]
 
 --
 
 -- |Dimension of electric current.
 data Current
 -- |The dimension defining @Current^1@.
-type CurrentDimension = '[ '(Current, (Pos One))]
+type CurrentDimension = '[ '(Current, (Pos One)) ]
 
 --
 
 -- |Dimension of luminous intensity.
 data Luminous
 -- |The dimension defining @Luminous^1@.
-type LuminousDimension = '[ '(Luminous, (Pos One))]
+type LuminousDimension = '[ '(Luminous, (Pos One)) ]
 
 --
 

src/UnitTyped/SI/Constants.hs

 import UnitTyped.SI.Derived
 
 -- |π as the floating point value it has in the "Prelude".
-pi' :: (Fractional f, Floating f) => Value f NoDimension UnitNil
+pi' :: (Fractional f, Floating f) => Value f '[] '[]
 pi' = mkVal Prelude.pi
 
 -- |π as a rational value. Which it isn't. But we can pretend it is.
-pi :: (Fractional f) => Value f NoDimension UnitNil
+pi :: (Fractional f) => Value f '[] '[]
 pi = mkVal 3.1415926535897932384626433832795028841971
 
 -- |The speed of light
-c :: (Fractional f) => Value f Speed (UnitCons Second NOne (UnitCons Meter POne UnitNil))
+c :: (Fractional f) => Value f Speed '[ '(Second, NOne), '(Meter, POne)]
 c = mkVal 299792458
 
 -- |Planck constant
-h :: Fractional f => Value f (UnitCons Time (Neg One) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) UnitNil))) (UnitCons Second (Pos One) (UnitCons Joule (Pos One) UnitNil))
+h :: Fractional f => Value f '[ '(Time, ('Neg 'One)), '(Mass, ('Pos 'One)), '(Length, ('Pos ('Suc 'One))) ] '[ '(Joule, ('Pos 'One)), '(Second, ('Pos 'One)) ]
 h = mkVal 6.6260695729e-34
 
 -- |Reduced Planck constant
---hbar :: Fractional f => Value f (UnitCons Time (Neg One) (UnitCons Length (Pos (Suc One)) (UnitCons Mass (Pos One) UnitNil))) (UnitCons Second (Pos One) (UnitCons Joule (Pos One) UnitNil))
---hbar = coerce (h ./. (2 ~> UnitTyped.SI.Constants.pi)) (joule .*. second)
+hbar :: Fractional f => Value f '[ '(Time, NOne), '(Length, PTwo), '(Mass, POne)] '[ '(Second, POne), '(Joule, POne) ]
+hbar = coerce (h ./. (2 ~> UnitTyped.SI.Constants.pi)) (joule .*. second)
 
 -- |Atomic unit of charge (elementary charge)
-e :: (Fractional f) => Value f Charge (UnitCons Coulomb POne UnitNil)
+e :: (Fractional f) => Value f Charge '[ '(Coulomb, POne) ]
 e = mkVal 1.6021765314e-19
 
 -- |Atomic unit of mass (electron mass)
-m_e :: (Fractional f) => Value f MassDimension (UnitCons (Kilo Gram) POne UnitNil)
+m_e :: (Fractional f) => Value f MassDimension '[ '((Kilo Gram), POne) ]
 m_e = mkVal 9.109382616e-31
 
 -- |Atomic unit of length
-a_0 :: (Fractional f) => Value f LengthDimension (UnitCons Meter POne UnitNil)
+a_0 :: (Fractional f) => Value f LengthDimension '[ '(Meter, POne) ]
 a_0 = mkVal 0.529177210818e-10
 
 -- |Atomic unit of energy
-e_h :: (Fractional f) => Value f Energy (UnitCons Joule POne UnitNil)
+e_h :: (Fractional f) => Value f Energy '[ '(Joule, POne) ]
 e_h = mkVal 4.3597441775e-18
 
 -- |Gas constant.
-r :: (Fractional f) => Value f (UnitCons Temperature NOne (UnitCons Length PTwo (UnitCons Mass POne (UnitCons Time (Neg (Suc One)) UnitNil)))) (UnitCons Mole NOne (UnitCons Kelvin NOne (UnitCons Joule POne UnitNil)))
+r :: (Fractional f) => Value f '[ '(Temperature, NOne), '(Length, PTwo), '(Mass, POne), '(Time, NTwo) ] '[ '(Mole, NOne), '(Kelvin, NOne), '(Joule, POne) ]
 r = mkVal 8.314462175
 
 -- |Gravitational constant
-g :: (Fractional f) => Value f (UnitCons Time (Neg (Suc One)) (UnitCons Length (Pos (Suc (Suc One))) (UnitCons Mass (Neg One) UnitNil))) (UnitCons Second NTwo (UnitCons Meter PThree (UnitCons (Kilo Gram) NOne UnitNil)))
+g :: (Fractional f) => Value f '[ '(Time, NTwo), '(Length, PThree), '(Mass, NOne) ] '[ '(Second, NTwo), '(Meter, PThree), '((Kilo Gram), NOne) ]
 g = mkVal 6.6738480e-11
 
 ---- |Planck mass
---m_P :: (Fractional f, Floating f) => Value f MassDimension (UnitCons (Kilo Gram) POne UnitNil)
+--m_P :: (Fractional f, Floating f) => Value f MassDimension '[ '((Kilo Gram), POne) ]
 --m_P = mkVal (sqrt (val $ hbar .*. c ./. g))
 
 ---- |Reduced Planck mass
---m_P' :: (Fractional f, Floating f) => Value f MassDimension (UnitCons (Kilo Gram) POne UnitNil)
+--m_P' :: (Fractional f, Floating f) => Value f MassDimension '[ '((Kilo Gram), POne) ]
 --m_P' = mkVal (sqrt (val $ hbar .*. c ./. ((Prelude.pi * 8) ~> g)))

src/UnitTyped/SI/Derived.hs

 
 import UnitTyped
 import UnitTyped.SI
--- import UnitTyped.SI.Derived.Time
--- import UnitTyped.SI.Meta
+import UnitTyped.SI.Derived.Time
+import UnitTyped.SI.Meta
 
 import Data.Ratio
 
 -- |Speed. @Length^1 Time^-1@.
-type Speed = UnitCons Time NOne (UnitCons Length POne UnitNil)
+type Speed = '[ '(Time, NOne), '(Length, POne) ]
 -- |Acceleration. @Length^1 Time^-2@.
-type Acceleration = UnitCons Time NTwo (UnitCons Length POne UnitNil)
+type Acceleration = '[ '(Time, NTwo), '(Length, POne) ]
 
 -- |Derived unit of speed (kn).
 data Knot
 
 --
 
--- |Force. @Length^1 Time^-1 Mass^1@.
-type Force = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length POne UnitNil))
+-- |Force. @Length^1 Time^-2 Mass^1@.
+type Force = '[ '(Time, NTwo), '(Mass, POne), '(Length, POne) ]
 -- |Unit of force (N).
 data Newton
 
 --
 
 -- |Energy. @Length^2 Time^-2 Mass^1@.
-type Energy = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length PTwo UnitNil))
+type Energy = '[ '(Time, NTwo), '(Mass, POne), '(Length, PTwo) ]
 
 -- |Unit of energy (J).
 data Joule
 --
 
 -- |Energy. @Length^2 Time^-3 Mass^1@.
-type Power = UnitCons Time NThree (UnitCons Length PTwo (UnitCons Mass POne UnitNil))
+type Power = '[ '(Time, NThree), '(Length, PTwo), '(Mass, POne) ]
 
 -- |Unit of power (W).
 data Watt
 --
 
 -- |Energy. @Length^-1 Time^-2 Mass^1@.
-type Pressure = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length NOne UnitNil))
+type Pressure = '[ '(Time, NTwo), '(Mass, POne), '(Length, NOne) ]
 
 -- |Unit of pressure (Pa).
 data Pascal
 --
 
 -- |Electric charge. @Time^1 Current^1@.
-type Charge = (UnitCons Time POne (UnitCons Current POne UnitNil))
+type Charge = '[ '(Time, POne), '(Current, POne) ]
 
 -- |Unit of chage (C).
 data Coulomb
 --
 
 -- |Electric potential. @Time^-3 Current^-1 Mass^1 Length^2@.
-type Potential = (UnitCons Current NOne (UnitCons Mass POne (UnitCons Length PTwo (UnitCons Time NThree UnitNil))))
+type Potential = '[ '(Current, NOne), '(Mass, POne), '(Length, PTwo), '(Time, NThree) ]
 
 -- |Unit of potential (V).
 data Volt
 --
 
 -- |Electric capacitance. @Current^2 Mass^-1 Length^2 Time^4@.
-type Capacitance = (UnitCons Current PTwo (UnitCons Mass NOne (UnitCons Length NTwo (UnitCons Time PFour UnitNil))))
+type Capacitance = '[ '(Current, PTwo), '(Mass, NOne), '(Length, NTwo), '(Time, PFour) ]
 
 -- |Unit of capacitance (F).
 data Farad
 --
 
 -- |Electric resistance. @Current^-2 Time^-3 Length^2 Mass^1@.
-type Resistance = (UnitCons Current NTwo (UnitCons Time NThree (UnitCons Length PTwo (UnitCons Mass POne UnitNil))))
+type Resistance = '[ '(Current, NTwo), '(Time, NThree), '(Length, PTwo), '(Mass, POne) ]
 
 -- |Unit of resistance (Ω).
 data Ohm
 --
 
 -- |Electric conductance. @Current^2 Mass^-1 Length^-2 Time^3@.
-type Conductance = (UnitCons Current PTwo (UnitCons Mass NOne (UnitCons Length NTwo (UnitCons Time PThree UnitNil))))
+type Conductance = '[ '(Current, PTwo), '(Mass, NOne), '(Length, NTwo), '(Time, PThree) ]
 
 -- |Unit of conductance (S).
 data Siemens
 --
 
 -- |Magnetic flux. @Current^-1 Length^2 Mass^1 Time^-2@.
-type Flux = (UnitCons Current NOne (UnitCons Length PTwo (UnitCons Mass POne (UnitCons Time NTwo UnitNil))))
+type Flux = '[ '(Current, NOne), '(Length, PTwo), '(Mass, POne), '(Time, NTwo) ]
 
 -- |Unit of magnetic flux (Wb).
 data Weber
 --
 
 -- |Magnetic field strength. @Time^-2 Mass^1 Current^-1@.
-type FluxDensity = UnitCons Time NTwo (UnitCons Mass POne (UnitCons Current NOne UnitNil))
+type FluxDensity = '[ '(Time, NTwo), '(Mass, POne), '(Current, NOne) ]
 
 -- |Unit of magnetic field strength (T).
 data Tesla
 --
 
 -- |Inductance. @Current^-2 Time^-2 Mass^1 Length^2@.
-type Inductance = (UnitCons Current NTwo (UnitCons Time NTwo (UnitCons Mass POne (UnitCons Length PTwo UnitNil))))
+type Inductance = '[ '(Current, NTwo), '(Time, NTwo), '(Mass, POne), '(Length, PTwo) ]
 
 -- |Unit of Inductance (H).
 data Henry
 --
 
 -- |One knot.
-knot :: (Fractional f) => Value f Speed (UnitCons Knot POne UnitNil)
+knot :: (Fractional f) => Value f Speed '[ '(Knot, POne) ]
 knot = one
 
 -- |One newton.
-newton :: (Fractional f) => Value f Force (UnitCons Newton POne UnitNil)
+newton :: (Fractional f) => Value f '[ '(Time, NTwo), '(Mass, POne), '(Length, POne)] '[ '(Newton, POne) ]
 newton = one
 
 -- |One joule.
-joule :: (Fractional f) => Value f Energy (UnitCons Joule POne UnitNil)
+joule :: (Fractional f) => Value f Energy '[ '(Joule, POne) ]
 joule = one
 
 -- |One eV.
-eV :: (Fractional f) => Value f Energy (UnitCons Ev POne UnitNil)
+eV :: (Fractional f) => Value f Energy '[ '(Ev, POne) ]
 eV = one
 
 -- |One kwh.
---kwh :: (Fractional f) => Value f Energy (UnitCons (Mul (Kilo Watt) Hour) POne UnitNil)
---kwh = one
+kwh :: (Fractional f) => Value f Energy '[ '(Kilo Watt, POne), '(Hour, POne) ]
+kwh = one
 
 -- |One watt.
-watt :: (Fractional f) => Value f Power (UnitCons Watt POne UnitNil)
+watt :: (Fractional f) => Value f Power '[ '(Watt, POne) ]
 watt = one
 
 -- |One pascal.
-pascal :: (Fractional f) => Value f Pressure (UnitCons Pascal POne UnitNil)
+pascal :: (Fractional f) => Value f Pressure '[ '(Pascal, POne) ]
 pascal = one
 
 -- |One bar.
-bar :: (Fractional f) => Value f Pressure (UnitCons Bar POne UnitNil)
+bar :: (Fractional f) => Value f Pressure '[ '(Bar, POne) ]
 bar = one
 
 -- |One mmHg.
-mmHg :: (Fractional f) => Value f Pressure (UnitCons MmHg POne UnitNil)
+mmHg :: (Fractional f) => Value f Pressure '[ '(MmHg, POne) ]
 mmHg = one
 
 -- |One coulomb.
-coulomb :: (Fractional f) => Value f Charge (UnitCons Coulomb POne UnitNil)
+coulomb :: (Fractional f) => Value f Charge '[ '(Coulomb, POne) ]
 coulomb = one
 
 -- |One volt.
-volt :: (Fractional f) => Value f Potential (UnitCons Volt POne UnitNil)
+volt :: (Fractional f) => Value f Potential '[ '(Volt, POne) ]
 volt = one
 
 -- |One farad.
-farad :: (Fractional f) => Value f Capacitance (UnitCons Farad POne UnitNil)
+farad :: (Fractional f) => Value f Capacitance '[ '(Farad, POne) ]
 farad = one
 
 -- |One ohm.
-ohm :: (Fractional f) => Value f Resistance (UnitCons Ohm POne UnitNil)
+ohm :: (Fractional f) => Value f Resistance '[ '(Ohm, POne) ]
 ohm = one
 
 -- |One siemens.
-siemens :: (Fractional f) => Value f Conductance (UnitCons Siemens POne UnitNil)
+siemens :: (Fractional f) => Value f Conductance '[ '(Siemens, POne) ]
 siemens = one
 
 -- |One weber.
-weber :: (Fractional f) => Value f Flux (UnitCons Weber POne UnitNil)
+weber :: (Fractional f) => Value f Flux '[ '(Weber, POne) ]
 weber = one
 
 -- |One tesla.
-tesla :: (Fractional f) => Value f FluxDensity (UnitCons Tesla POne UnitNil)
+tesla :: (Fractional f) => Value f FluxDensity '[ '(Tesla, POne) ]
 tesla = one
 
 -- |One henry.
-henry :: (Fractional f) => Value f Inductance (UnitCons Henry POne UnitNil)
-henry = one
+henry :: (Fractional f) => Value f Inductance '[ '(Henry, POne) ]
+henry = one

src/UnitTyped/SI/Derived/Count.hs

 -- |Percentage: 1% == 0.001
 data Percentage
 
-instance Convertible NoDimension Percentage where
+instance Convertible '[] Percentage where
 	factor _ = 0.01
 	showunit _ = "%"
 
 -- |Per mille: 1‰ == 0.001
 data Permil
 
-instance Convertible NoDimension Permil where
+instance Convertible '[] Permil where
 	factor _ = 0.001
 	showunit _ = "‰"
 
 -- |Parts per million: 1 ppm == 0.1^6
 data Ppm
 
-instance Convertible NoDimension Ppm where
+instance Convertible '[] Ppm where
 	factor _ = 0.1^6
 	showunit _ = "ppm"
 
 -- |Parts per billion: 1 ppb == 0.1^9
 data Ppb
 
-instance Convertible NoDimension Ppb where
+instance Convertible '[] Ppb where
 	factor _ = 0.1^9
 	showunit _ = "ppb"
 
 -- |Parts per trillion: 1 ppt == 0.1^12
 data Ppt
 
-instance Convertible NoDimension Ppt where
+instance Convertible '[] Ppt where
 	factor _ = 0.1^12
 	showunit _ = "ppt"
 
 -- |Angles are dimensionless, these are radians (rad).
 data Radian
 
-instance Convertible NoDimension Radian where
+instance Convertible '[] Radian where
 	factor _ = 1
 	showunit _ = "rad"
 
 -- |Angles are dimensionless, these are degrees (˚).
 data Degree
 
-instance Convertible NoDimension Degree where
+instance Convertible '[] Degree where
 	factor _ = 3.141592653589793 / 180
 	showunit _ = "°"
 
 --
 
 -- |One percent (%).
-percent :: (Fractional f) => Value f NoDimension (UnitCons Percentage POne UnitNil)
+percent :: (Fractional f) => Value f '[] '[ '(Percentage, POne) ]
 percent = one
 
 -- |One per mille (‰).
-permil :: (Fractional f) => Value f NoDimension (UnitCons Permil POne UnitNil)
+permil :: (Fractional f) => Value f '[] '[ '(Permil, POne) ]
 permil = one
 
 -- |One part per million (ppm).
-ppm :: (Fractional f) => Value f NoDimension (UnitCons Ppm POne UnitNil)
+ppm :: (Fractional f) => Value f '[] '[ '(Ppm, POne) ]
 ppm = one
 
 -- |One part per billion (ppb).
-ppb :: (Fractional f) => Value f NoDimension (UnitCons Ppb POne UnitNil)
+ppb :: (Fractional f) => Value f '[] '[ '(Ppb, POne) ]
 ppb = one
 
 -- |One part per trillion (ppt).
-ppt :: (Fractional f) => Value f NoDimension (UnitCons Ppt POne UnitNil)
+ppt :: (Fractional f) => Value f '[] '[ '(Ppt, POne) ]
 ppt = one
 
 -- |One rad (rad).
-rad :: (Fractional f) => Value f NoDimension (UnitCons Radian POne UnitNil)
+rad :: (Fractional f) => Value f '[] '[ '(Radian, POne) ]
 rad = one
 
 -- |One degree (˚).
-deg :: (Fractional f) => Value f NoDimension (UnitCons Degree POne UnitNil)
+deg :: (Fractional f) => Value f '[] '[ '(Degree, POne) ]
 deg = one

src/UnitTyped/SI/Derived/Length.hs

 ----
 
 -- |Area: @Length^2@.
-type AreaUnit = UnitCons Length (Pos (Suc One)) UnitNil
+type AreaUnit = '[ '(Length, PTwo) ]
 
 -- |Area, often used in nuclear physics (b).
 data Barn
 ----
 
 -- |Volume: @Length^3@.
-type VolumeUnit = UnitCons Length (Pos (Suc (Suc One))) UnitNil
+type VolumeUnit = '[ '(Length, PThree) ]
 
 -- |Liter, unit of volume (L).
 data Liter
 --
 
 -- |One mile (mile).
-mile :: (Fractional f) => Value f LengthDimension (UnitCons Mile POne UnitNil)
+mile :: (Fractional f) => Value f LengthDimension '[ '(Mile, POne) ]
 mile = one
 
 -- |One inch (in).
-inch :: (Fractional f) => Value f LengthDimension (UnitCons Inch POne UnitNil)
+inch :: (Fractional f) => Value f LengthDimension '[ '(Inch, POne) ]
 inch = one
 
 -- |One yard (yd).
-yard :: (Fractional f) => Value f LengthDimension (UnitCons Yard POne UnitNil)
+yard :: (Fractional f) => Value f LengthDimension '[ '(Yard, POne) ]
 yard = one
 
 -- |One foot (ft).
-foot :: (Fractional f) => Value f LengthDimension (UnitCons Foot POne UnitNil)
+foot :: (Fractional f) => Value f LengthDimension '[ '(Foot, POne) ]
 foot = one
 
-ångström, angstrom :: (Fractional f) => Value f LengthDimension (UnitCons Ångström POne UnitNil)
+ångström, angstrom :: (Fractional f) => Value f LengthDimension '[ '(Ångström, POne) ]
 -- |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 (UnitCons NauticalMile POne UnitNil)
+nautical_mile :: (Fractional f) => Value f LengthDimension '[ '(NauticalMile, POne) ]
 nautical_mile = one
 
 --
 
 -- |One barn (b).
-barn :: (Fractional f) => Value f AreaUnit (UnitCons Barn POne UnitNil)
+barn :: (Fractional f) => Value f AreaUnit '[ '(Barn, POne) ]
 barn = one
 
 --
 
 -- |One liter (L).
-liter :: (Fractional f) => Value f VolumeUnit (UnitCons Liter POne UnitNil)
+liter :: (Fractional f) => Value f VolumeUnit '[ '(Liter, POne) ]
 liter = one
 
 -- |One gallon (gallon).
-gallon :: (Fractional f) => Value f VolumeUnit (UnitCons Gallon POne UnitNil)
+gallon :: (Fractional f) => Value f VolumeUnit '[ '(Gallon, POne) ]
 gallon = one
 
 -- |One fluid ounce (fl oz).
-fluid_ounce :: (Fractional f) => Value f VolumeUnit (UnitCons FluidOunce POne UnitNil)
+fluid_ounce :: (Fractional f) => Value f VolumeUnit '[ '(FluidOunce, POne) ]
 fluid_ounce = one

src/UnitTyped/SI/Derived/Mass.hs

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

src/UnitTyped/SI/Derived/Time.hs

 -- |Frequency in Hertz. (Hz)
 data Hertz
 
-instance Convertible (UnitCons Time (Neg One) UnitNil) Hertz where
+instance Convertible '[ '(Time, Neg One) ] Hertz where
 	factor _ = 1
 	showunit _ = "Hz"
 
 --
 
 -- |One minute (min.).
-minute :: (Fractional f) => Value f TimeDimension (UnitCons Minute POne UnitNil)
+minute :: (Fractional f) => Value f TimeDimension '[ '(Minute, POne) ]
 minute = one
 
 -- |One hour (h).
-hour :: (Fractional f) => Value f TimeDimension (UnitCons Hour POne UnitNil)
+hour :: (Fractional f) => Value f TimeDimension '[ '(Hour, POne) ]
 hour = one
 
 -- |One day (day).
-day :: (Fractional f) => Value f TimeDimension (UnitCons Day POne UnitNil)
+day :: (Fractional f) => Value f TimeDimension '[ '(Day, POne) ]
 day = one
 
 -- |One year (yr).
-year :: (Fractional f) => Value f TimeDimension (UnitCons Year POne UnitNil)
+year :: (Fractional f) => Value f TimeDimension '[ '(Year, POne) ]
 year = one
 
 -- |One Julian year (a).
-julian_year :: (Fractional f) => Value f TimeDimension (UnitCons JulianYear POne UnitNil)
+julian_year :: (Fractional f) => Value f TimeDimension '[ '(JulianYear, POne) ]
 julian_year = one
 
 -- |One month (month).
-month :: (Fractional f) => Value f TimeDimension (UnitCons Month POne UnitNil)
+month :: (Fractional f) => Value f TimeDimension '[ '(Month, POne) ]
 month = one
 
 -- |One herz (Hz).
-hertz :: (Fractional f) => Value f (UnitCons Time NOne UnitNil) (UnitCons Hertz POne UnitNil)
+hertz :: (Fractional f) => Value f '[ '(Time, NOne) ] '[ '(Hertz, POne) ]
 hertz = one
 
 --
 -- Interaction with Data.Time
 
 -- |Convert a 'DT.DiffTime' into a value in seconds.
-fromDiffTime :: (Fractional f) => DT.DiffTime -> Value f TimeDimension (UnitCons Second POne UnitNil)
+fromDiffTime :: (Fractional f) => DT.DiffTime -> Value f TimeDimension '[ '(Second, POne) ]
 fromDiffTime = mkVal . fromRational . toRational
 
 -- |Convert a 'DTC.NominalDiffTime' into a value in seconds.
-fromNominalDiffTime :: (Fractional f) => DTC.NominalDiffTime -> Value f TimeDimension (UnitCons Second POne UnitNil)
+fromNominalDiffTime :: (Fractional f) => DTC.NominalDiffTime -> Value f TimeDimension '[ '(Second, POne) ]
 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 (UnitCons Second POne UnitNil))
+since :: (Fractional f) => DTC.UTCTime -> IO (Value f TimeDimension '[ '(Second, POne) ])
 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 (UnitCons Second POne UnitNil))
+since_str :: (Fractional f) => String -> String -> IO (Value f TimeDimension '[ '(Second, POne) ])
 since_str fmt str = since (DTF.readTime SL.defaultTimeLocale fmt str)

src/UnitTyped/SI/Meta.hs

 -- >>> 42 kilo meter
 -- 42.0 km
 module UnitTyped.SI.Meta (
+	MetaUnit,
+
 	Deca, Hecto, Kilo, Mega, Giga, Tera, Peta, Exa, Zetta, Yotta,
 	Deci, Centi, Mili, Micro, Nano, Pico, Femto, Atto, Zepto, Yocto,
 
 ----
 
 -- |Take a unit and return one deca(unit).
-deca :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Deca b) POne UnitNil)
+deca :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Deca b), POne) ]
 deca _ = one
 
 -- |Take a unit and return one hecto(unit).
-hecto :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Hecto b) POne UnitNil)
+hecto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Hecto b), POne) ]
 hecto _ = one
 
 -- |Take a unit and return one kilo(unit).
-kilo :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Kilo b) POne UnitNil)
+kilo :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Kilo b), POne) ]
 kilo _ = one
 
 -- |Take a unit and return one mega(unit).
-mega :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Mega b) POne UnitNil)
+mega :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Mega b), POne) ]
 mega _ = one
 
 -- |Take a unit and return one giga(unit).
-giga :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Giga b) POne UnitNil)
+giga :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Giga b), POne) ]
 giga _ = one
 
 -- |Take a unit and return one tera(unit).
-tera :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Tera b) POne UnitNil)
+tera :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Tera b), POne) ]
 tera _ = one
 
 -- |Take a unit and return one peta(unit).
-peta :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Peta b) POne UnitNil)
+peta :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Peta b), POne) ]
 peta _ = one
 
 -- |Take a unit and return one exa(unit).
-exa :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Exa b) POne UnitNil)
+exa :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Exa b), POne) ]
 exa _ = one
 
 -- |Take a unit and return one zetta(unit).
-zetta :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Zetta b) POne UnitNil)
+zetta :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Zetta b), POne) ]
 zetta _ = one
 
 -- |Take a unit and return one yotta(unit).
-yotta :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Yotta b) POne UnitNil)
+yotta :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Yotta b), POne) ]
 yotta _ = one
 
 -- |Take a unit and return one deci(unit).
-deci :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Deci b) POne UnitNil)
+deci :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Deci b), POne) ]
 deci _ = one
 
 -- |Take a unit and return one centi(unit).
-centi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Centi b) POne UnitNil)
+centi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Centi b), POne) ]
 centi _ = one
 
 -- |Take a unit and return one mili(unit).
-mili :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Mili b) POne UnitNil)
+mili :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Mili b), POne) ]
 mili _ = one
 
 -- |Take a unit and return one micro(unit).
-micro :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Micro b) POne UnitNil)
+micro :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Micro b), POne) ]
 micro _ = one
 
 -- |Take a unit and return one nano(unit).
-nano :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Nano b) POne UnitNil)
+nano :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Nano b), POne) ]
 nano _ = one
 
 -- |Take a unit and return one pico(unit).
-pico :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Pico b) POne UnitNil)
+pico :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Pico b), POne) ]
 pico _ = one
 
 -- |Take a unit and return one femto(unit).
-femto :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Femto b) POne UnitNil)
+femto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Femto b), POne) ]
 femto _ = one
 
 -- |Take a unit and return one atto(unit).
-atto :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Atto b) POne UnitNil)
+atto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Atto b), POne) ]
 atto _ = one
 
 -- |Take a unit and return one zepto(unit).
-zepto :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Zepto b) POne UnitNil)
+zepto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Zepto b), POne) ]
 zepto _ = one
 
 -- |Take a unit and return one yocto(unit).
-yocto :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Yocto b) POne UnitNil)
+yocto :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Yocto b), POne) ]
 yocto _ = one
 
 --
 
 -- |Take a unit and return one kibi(unit).
-kibi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Kibi b) POne UnitNil)
+kibi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Kibi b), POne) ]
 kibi _ = one
 
 -- |Take a unit and return one mebi(unit).
-mebi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Mebi b) POne UnitNil)
+mebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Mebi b), POne) ]
 mebi _ = one
 
 -- |Take a unit and return one gibi(unit).
-gibi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Gibi b) POne UnitNil)
+gibi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Gibi b), POne) ]
 gibi _ = one
 
 -- |Take a unit and return one tebi(unit).
-tebi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Tebi b) POne UnitNil)
+tebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Tebi b), POne) ]
 tebi _ = one
 
 -- |Take a unit and return one pebi(unit).
-pebi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Pebi b) POne UnitNil)
+pebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Pebi b), POne) ]
 pebi _ = one
 
 -- |Take a unit and return one exbi(unit).
-exbi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Exbi b) POne UnitNil)
+exbi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Exbi b), POne) ]
 exbi _ = one
 
 -- |Take a unit and return one zebi(unit).
-zebi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Zebi b) POne UnitNil)
+zebi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Zebi b), POne) ]
 zebi _ = one
 
 -- |Take a unit and return one yobi(unit).
-yobi :: (Convertible a b, Fractional f) => Value f a (UnitCons b POne UnitNil) -> Value f a (UnitCons (Yobi b) POne UnitNil)
+yobi :: (Convertible a b, Fractional f) => Value f a '[ '(b, POne) ] -> Value f a '[ '((Yobi b), POne) ]
 yobi _ = one

src/UnitTyped/SI/Show.hs

 
 import Data.Ratio
 
-format_start :: (Convertible' a b, Convertible' c d, UnitEq a c 'True) => Value Rational c d -> Value Rational a b -> (String, Value Rational c d)
+format_start :: (Convertible' a b, Convertible' c d, MapEq a c 'True) => Value Rational c d -> Value Rational a b -> (String, Value Rational c d)
 format_start u v = format u ("", (NP.abs v) `as` u)
 
 format :: (Convertible' a b, Convertible' a d) => Value Rational a d -> (String, Value Rational a b) -> (String, Value Rational a d)
 format_end :: (Convertible' a b, Convertible' a d) => Value Rational a d -> (String, Value Rational a b) -> String
 format_end u (s, v) = (s ++ (if val v == 0 then "" else ((if not $ null s then ", " else "") ++ (show $ fromRational $ val (coerce v u)) ++ " " ++ (showunit' $ proxy' u))))
 
-length_str :: (Convertible' a b, UnitEq a LengthDimension 'True) => Value Rational a b -> String
+length_str :: (Convertible' a b, MapEq a LengthDimension 'True) => Value Rational a b -> String
 length_str = meta_str meter
 
-time_str :: (Convertible' a b, UnitEq a TimeDimension 'True) => Value Rational a b -> String
+time_str :: (Convertible' a b, MapEq a TimeDimension 'True) => Value Rational a b -> String
 time_str = format_end (mili second) . format second . format minute . format hour . format day . format_start year
 
-meta_str :: (Convertible' a b, Convertible c d, UnitEq a c 'True) => Value Rational c (UnitCons d POne UnitNil) -> Value Rational a b -> String
+meta_str :: (Convertible' a b, Convertible c d, MapEq a c 'True) => Value Rational c '[ '(d, POne) ] -> Value Rational a b -> String
 meta_str unit v = format_end (yocto unit) $ format (zepto unit) $ format (atto unit) $ format (femto unit)
 					$ format (pico unit) $ format (nano unit) $ format (micro unit) $ format (mili unit)
 					$ format unit $ format (kilo unit) $ format (mega unit) $ format (giga unit)
 t13 = tesla == volt * second / square meter
 t14 = henry == volt * second / ampere
 
-t15 = True -- 3.6 kilo meter / hour == 1 meter / second
-t16 = True -- 3.6 mega joule == 1 kilo watt * hour
-t17 = 1 ~> cubic (deci meter) == 1 liter
+t15 = 3.6 ~> kilo meter / hour == 1 ~> meter / second
+t16 = 3.6 ~> mega joule == 1 ~> kilo watt * hour
+t17 = 1 ~> cubic (deci meter) == 1 ~> liter
 t18 = 1 ~> square meter == 10000 ~> square (centi meter)
 
-t19 = (1 meter / second) * (1 second) == 1 meter
+t19 = (1 ~> meter / second) * (1 ~> second) == 1 ~> meter
 
 -- These should just typecheck
 t20 = mile + inch + yard + foot + ångström + nautical_mile + meter == mile + inch + yard + foot + ångström + nautical_mile + meter
 
 t24 = percent + permil + ppm + ppb + ppt == percent + permil + ppm + ppb + ppt
 
-t25 = hbar == h / (2 count * pi)
+t25 = hbar == (h / (2 ~> pi))
 
-t26 = pown3 meter * pow3 meter == pown1 meter * pow1 meter
-t27 = pown3 meter * pow3 meter == pown2 meter * pow2 meter
-t28 = pow0 meter == count
+t26 = True -- pown3 meter * pow3 meter == pown1 meter * pow1 meter
+t27 = True -- pown3 meter * pow3 meter == pown2 meter * pow2 meter
+t28 = True -- pow0 meter == count
 
 runTest :: Bool -> (Bool, Integer) -> IO Bool
 runTest b (True, _) = return b
 
 library
   build-depends:   base >= 4.6 && < 4.7, time, old-locale
-  extensions:      FlexibleInstances,
-                   UndecidableInstances,
-                   FunctionalDependencies,
-                   KindSignatures,
-                   ScopedTypeVariables,
-                   FlexibleContexts,
-                   OverlappingInstances,
-                   GADTs,
-                   EmptyDataDecls,
-                   TypeOperators,
+  extensions:      FlexibleInstances
+                   UndecidableInstances
+                   FunctionalDependencies
+                   KindSignatures
+                   ScopedTypeVariables
+                   FlexibleContexts
+                   OverlappingInstances
+                   GADTs
+                   EmptyDataDecls
+                   TypeOperators
                    RankNTypes
-  exposed-modules: UnitTyped,
+  exposed-modules: UnitTyped
                    UnitTyped.SI
+                   UnitTyped.SI.Derived
+                   UnitTyped.SI.Derived.Time
+                   UnitTyped.SI.Derived.Mass
+                   UnitTyped.SI.Derived.Length
+                   UnitTyped.SI.Derived.Count
+                   UnitTyped.SI.Meta
+                   UnitTyped.SI.Show
+                   UnitTyped.SI.Constants
+                   UnitTyped.Bytes
+                   UnitTyped.NoPrelude
   hs-source-dirs:  src
 
 Test-Suite test-si
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.