simple-units (empty) → 1.0.0.0
raw patch · 9 files changed
+579/−0 lines, 9 filesdep +basedep +first-class-familiessetup-changed
Dependencies added: base, first-class-families
Files
- LICENSE +18/−0
- README.md +24/−0
- Setup.hs +2/−0
- simple-units.cabal +44/−0
- src/Units/Simple.hs +115/−0
- src/Units/Simple/Arithmetic.hs +154/−0
- src/Units/Simple/Internals.hs +79/−0
- src/Units/Simple/Quantity.hs +80/−0
- src/Units/Simple/Unit.hs +63/−0
+ LICENSE view
@@ -0,0 +1,18 @@+Copyright Gustavo Roscoe (c) 2019++Permission is hereby granted, free of charge, to any person obtaining a copy of+this software and associated documentation files (the "Software"), to deal in+the Software without restriction, including without limitation the rights to+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of+the Software, and to permit persons to whom the Software is furnished to do so,+subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,24 @@+# simple-units+A Haskell library for simple arithmetic with SI units using type-checked dimensional analysis.++```haskell+>>> let newton = kilogram .* meter ./ (second .* second)+>>> 23*newton+23.0 kg*m/s^2+>>> let g = 6.67408e-11 * newton .* (meter .* meter) ./ (kilogram .* kilogram)+>>> g -- gravitational constant+6.67408e-11 m^3/kg*s^2+>>> let gravity m1 m2 r = g .* (m1 * kilogram) .* (m2 * kilogram) ./ (r*meter .* r*meter)+>>> let earth_mass = 5.972e24 * kilogram+>>> let mars_mass = 6.417e23 * kilogram+>>> let earth_radius = 6371e3 * meter+>>> let mars_radius = 3389.5e3 * meter+>>> let weight_on_earth mass = gravity mass earth_mass earth_radius+>>> let weight_on_mars mass = gravity mass mars_mass mars_radius+>>> weight_on_earth (80 * kilogram)+785.5719790179963 kg*m/s^2+>>> weight_on_mars (80 * kilogram)+298.22370259533704 kg*m/s^2+>>> weight_on_mars 1 ./ weight_on_earth 1+0.3796261966575378 <adimensional>+```
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ simple-units.cabal view
@@ -0,0 +1,44 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.1.+--+-- see: https://github.com/sol/hpack+--+-- hash: 1bf2ea2a4041479d0c14336601f236f12e4c746191ab5dff6a13b335a3e29fef++name: simple-units+version: 1.0.0.0+synopsis: Simple arithmetic with SI units using type-checked dimensional analysis.+description: Please see the README on GitHub at <https://github.com/groscoe/simple-units#readme>+category: Numeric, Numerical+homepage: https://github.com/groscoe/simple-units#readme+bug-reports: https://github.com/groscoe/simple-units/issues+author: Gustavo Roscoe+maintainer: gustavo@gustavoroscoe.com+copyright: 2019 Gustavo Roscoe+license: MIT+license-file: LICENSE+build-type: Simple+extra-source-files:+ README.md++source-repository head+ type: git+ location: https://github.com/groscoe/simple-units++library+ exposed-modules:+ Units.Simple+ other-modules:+ Units.Simple.Arithmetic+ Units.Simple.Internals+ Units.Simple.Quantity+ Units.Simple.Unit+ Paths_simple_units+ hs-source-dirs:+ src+ ghc-options: -Wall -Wcompat+ build-depends:+ base >=4.9 && <5+ , first-class-families >=0.5 && <0.6+ default-language: Haskell2010
+ src/Units/Simple.hs view
@@ -0,0 +1,115 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+module Units.Simple+ (-- *The @Quantity@ type+ Quantity ()+ , fromQuantity+ , Unit (..)+ , Units+ , SingleUnit+ , UnitRepr+ , showUnits++ -- * Basic arithmetic with quantities+ , (.+)+ , (.-)+ , (.*)+ , (./)++ -- *Base SI Units+ -- |Smart constructors for quantities in all the base SI Units.+ -- The constructors are provided in both unitary (non-ticked) and+ -- function (ticked) forms.+ --+ -- Examples:+ --+ -- >>> 273.0*kelvin -- unitary form+ -- 273.0 K+ -- >>> kelvin' 273.0 -- function form+ -- 273.0 K+ , adim+ , adim'+ , meter+ , meter'+ , kilogram+ , kilogram'+ , second+ , second'+ , ampere+ , ampere'+ , kelvin+ , kelvin'+ , mole+ , mole'+ , candela+ , candela'+ ) where+++import Units.Simple.Quantity+import Units.Simple.Arithmetic+import Units.Simple.Unit++type SingleUnit (u :: Unit) = '( '[ '(u, 1)], '[])+type Adimensional = '( '[], '[])++-- | A quantity with no associated dimension. Can be multiplied or divided+-- by any other quantity, but can only be added to or subtracted from+-- other adimensional quantities.+--+-- >>> 2*adim + 4*adim+-- 6 <adimensional>+-- >>> adim .+ meter+-- <BLANKLINE>+-- <interactive>:79:1-13: error:+-- • Unit mismatch: <adimensional> and m+-- • In the expression: adim .+ meter+-- In an equation for ‘it’: it = adim .+ meter+adim :: Num a => Quantity Adimensional a+adim = Quantity 1++meter :: Num a => Quantity (SingleUnit 'Meter) a+meter = Quantity 1++kilogram :: Num a => Quantity (SingleUnit 'Kilogram) a+kilogram = Quantity 1++second :: Num a => Quantity (SingleUnit 'Second) a+second = Quantity 1++ampere :: Num a => Quantity (SingleUnit 'Ampere) a+ampere = Quantity 1++kelvin :: Num a => Quantity (SingleUnit 'Kelvin) a+kelvin = Quantity 1++mole :: Num a => Quantity (SingleUnit 'Mole) a+mole = Quantity 1++candela :: Num a => Quantity (SingleUnit 'Candela) a+candela = Quantity 1++adim' :: Num a => a -> Quantity Adimensional a+adim' = Quantity++meter' :: Num a => a -> Quantity (SingleUnit 'Meter) a+meter' = Quantity++kilogram' :: Num a => a -> Quantity (SingleUnit 'Kilogram) a+kilogram' = Quantity++second' :: Num a => a -> Quantity (SingleUnit 'Second) a+second' = Quantity++ampere' :: Num a => a -> Quantity (SingleUnit 'Ampere) a+ampere' = Quantity++kelvin' :: Num a => a -> Quantity (SingleUnit 'Kelvin) a+kelvin' = Quantity++mole' :: Num a => a -> Quantity (SingleUnit 'Mole) a+mole' = Quantity++candela' :: Num a => a -> Quantity (SingleUnit 'Candela) a+candela' = Quantity
+ src/Units/Simple/Arithmetic.hs view
@@ -0,0 +1,154 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+module Units.Simple.Arithmetic+ ( (.+)+ , (.-)+ , (.*)+ , (./)+ ) where++import Data.Kind+import GHC.TypeLits as TL++import Fcf++import Units.Simple.Unit+import Units.Simple.Quantity+import Units.Simple.Internals (Foldl, DeleteBy, Sort)+++data Lookup' :: [(k, b)] -> k -> Exp (Maybe b)+type instance Eval (Lookup' as a) = Eval (Lookup a as)++type InList (as :: [(k, b)]) = IsJust <=< Lookup' as++type And (f :: a -> Exp Bool) (as :: [a]) = Foldr (&&) 'True (Eval (Map f as))++type AllInSecond (l1 :: [(k, a)]) (l2 :: [(k, a)]) = And (InList l2 <=< Fst) l1++type SameMaps (l1 :: [(k, a)]) (l2 :: [(k, a)]) = Eval (AllInSecond l1 l2) && Eval (AllInSecond l2 l1)++type SameUnits' (u1 :: Units) (u2 :: Units) = Eval (SameMaps (Eval (Fst u1)) (Eval (Fst u2)))+ && Eval (SameMaps (Eval (Snd u1)) (Eval (Snd u2)))++type family SameUnits (u1 :: Units) (u2 :: Units) :: Constraint where+ SameUnits u1 u2 = If (Eval (SameUnits' u1 u2))+ (Eval (SameUnits' u1 u2) ~ 'True)+ (TypeError+ ('Text "Unit mismatch: "+ ':<>: 'Text (UnitRepr u1)+ ':<>: 'Text " and "+ ':<>: 'Text (UnitRepr u2)))++type CleanUnitList = Filter (Not <=< TyEq 0 <=< Snd)+type CleanUnits us = (CleanUnitList *** CleanUnitList) us++data CancelUnit :: Unit' -> Unit' -> Exp (Unit', Unit')+type instance Eval (CancelUnit '(a, m) '(b, n)) =+ If (Eval (LiftM2 (&&) (TyEq a b) (n >= m)))+ '( '(a, 0), '(b, n TL.- m))+ '( '(a, m TL.- n), '(b, 0))++type GetMatchingUnits l1 l2 =+ (Filter (Flip UnitInList l2) *** Filter (Flip UnitInList l1)) =<< (Sort *** Sort) '(l1, l2)+type CancelMatchingUnitLists l1 l2 =+ Unzip (Uncurry (ZipWith CancelUnit) (Eval (GetMatchingUnits l1 l2)))+type CancelUnitLists l1 l2 =+ ((++) (Eval (l1 \\ l2)) *** (++) (Eval (l2 \\ l1))) =<< CancelMatchingUnitLists l1 l2+type CancelUnits (a :: Units) = CancelUnitLists (Eval (Fst a)) (Eval (Snd a))++data SameUnit :: Unit' -> Unit' -> Exp Bool+type instance Eval (SameUnit a b) = Eval (LiftM2 TyEq (Fst a) (Fst b))+type (\\) = Foldl (Flip (DeleteBy SameUnit))++data MergeUnit :: Unit' -> Unit' -> Exp Unit'+type instance Eval (MergeUnit '(a, m) '(b, n)) =+ If (Eval (TyEq a b))+ '(a, (TL.+) m n)+ '(b, n)++data UnitInList :: Unit' -> [Unit'] -> Exp Bool+type instance Eval (UnitInList '(u, n) '[]) = 'False+type instance Eval (UnitInList '(u, n) ('(v, _) ': xs)) = Eval (Eval (TyEq u v) || Eval (UnitInList '(u, n) xs))++data MergeUnitFromList :: u -> [us] -> Exp [us]+type instance Eval (MergeUnitFromList u us) = Eval (Map (MergeUnit u) us)++type MergeUnitLists (us1 :: [Unit']) (us2 :: [Unit']) = Foldr MergeUnitFromList us2 us1+data MergeUnits' :: Units -> Units -> Exp Units+type instance Eval (MergeUnits' '(num1, denom1) '(num2, denom2)) =+ Eval (CancelUnits+ '( Eval (Eval (MergeUnitLists num1 num2) ++ Eval (Filter (Not <=< Flip UnitInList num2) num1))+ , Eval (Eval (MergeUnitLists denom1 denom2) ++ Eval (Filter (Not <=< Flip UnitInList denom2) denom1))))++type MergeUnits us1 us2 = Eval (CleanUnits (Eval (MergeUnits' us1 us2)))++data Recip' :: Units -> Exp Units+type instance Eval (Recip' '(num, denom)) = '(denom, num)+type Recip a = Eval (Recip' a)++-- |Sums two quantities with the same units. Summing quantities with different units+-- results in a type error.+--+-- Examples:+--+-- >>> 2*meter .+ 3*meter+-- 5 m+-- >>> 2*meter .+ 1*second+-- <BLANKLINE>+-- <interactive>:16:1-19: error:+-- • Unit mismatch: m and s+-- • In the expression: 2 * meter .+ 1 * second+-- In an equation for ‘it’: it = 2 * meter .+ 1 * second+(.+) :: (SameUnits u1 u2, Num a) => Quantity u1 a -> Quantity u2 a -> Quantity u1 a+Quantity x .+ Quantity y = Quantity (x + y)+infixl 5 .+++-- |Subtracts two quantities with the same units. Subtracting quantities with different units+-- results in a type error.+--+-- Examples:+--+-- >>> let newton = kilogram .* meter ./ (second .* second)+-- >>> 10*newton - 2*newton+-- 8.0 kg*m/s^2+(.-) :: (SameUnits u1 u2, Num a) => Quantity u1 a -> Quantity u2 a -> Quantity u1 a+Quantity x .- Quantity y = Quantity (x - y)+infixl 5 .-++-- |Multiplies two quantities correctly merging their units.+--+-- Examples:+--+-- >>> meter .* meter+-- 1 m^2+-- >>> let mps = meter ./ second+-- >>> 20*mps .* 60*second+-- 1200.0 m+--+-- __Important:__ Though @Quantity a@ has a @Num@ instance for convenience, it+-- __must not__ be used for anything other than interacting with literals, otherwise+-- the units will __not__ be correct:+--+-- >>> 2*meter * 3*meter -- note that (*) was used in place of (.*)+-- 6 m+-- >>> 2*meter .* 3*meter -- this is the correct usage+-- 6 m^2+(.*) :: Num a => Quantity us1 a -> Quantity us2 a -> Quantity (MergeUnits us1 us2) a+Quantity x .* Quantity y = Quantity (x * y)+infixl 6 .*++-- | Divides a quantity by another correctly merging their units.+--+-- Examples:+--+-- >>> let coulomb = second .* ampere+-- >>> 20*coulomb ./ 2*second+-- 10.0 A+(./) :: Fractional a => Quantity us1 a -> Quantity us2 a -> Quantity (MergeUnits us1 (Recip us2)) a+Quantity x ./ Quantity y = Quantity (x / y)+infixl 6 ./
+ src/Units/Simple/Internals.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+module Units.Simple.Internals where++import GHC.TypeLits hiding (type (<=))+import qualified GHC.TypeLits as TL++import Fcf hiding (type (<=))+import qualified Fcf+++data ApSep :: Symbol -> Symbol -> Symbol -> Exp Symbol+type instance Eval (ApSep sep x xs) = sep `AppendSymbol` x `AppendSymbol` xs++type Intersperse' sep xs = Foldr (ApSep sep) "" xs++data Intersperse :: Symbol -> [Symbol] -> Exp Symbol+type instance Eval (Intersperse _ '[]) = ""+type instance Eval (Intersperse sep (x ': xs)) = x `AppendSymbol` Eval (Intersperse' sep xs)+++data NatToDigit :: Nat -> Exp Symbol+type instance Eval (NatToDigit 0) = "0"+type instance Eval (NatToDigit 1) = "1"+type instance Eval (NatToDigit 2) = "2"+type instance Eval (NatToDigit 3) = "3"+type instance Eval (NatToDigit 4) = "4"+type instance Eval (NatToDigit 5) = "5"+type instance Eval (NatToDigit 6) = "6"+type instance Eval (NatToDigit 7) = "7"+type instance Eval (NatToDigit 8) = "8"+type instance Eval (NatToDigit 9) = "9"++data (<>) :: Exp a -> Exp a -> Exp a+type instance Eval ((a :: Exp Symbol) <> (b :: Exp Symbol)) = Eval a `AppendSymbol` Eval b++data (/) :: Nat -> Nat -> Exp Nat+type instance Eval (a / b) = a `TL.Div` b++data (%) :: Nat -> Nat -> Exp Nat+type instance Eval (a % b) = a `TL.Mod` b++data Show' :: a -> Exp Symbol+type instance Eval (Show' (n :: Nat)) = Eval (Guarded n+ '[ Flip (Fcf.<=) 9 ':= NatToDigit n+ , Otherwise ':= Show' (Eval (n / 10)) <> Show' (Eval (n % 10))+ ])+++data (<=) :: k -> k -> Exp Bool+type instance Eval ((a :: Nat) <= (b :: Nat)) = a <=? b+type instance Eval ((a :: Symbol) <= (b :: Symbol)) = Eval (Guarded (CmpSymbol a b)+ '[ TyEq 'EQ ':= Pure 'True+ , TyEq 'LT ':= Pure 'True+ , Otherwise ':= Pure 'False+ ])+type instance Eval ('(a, _) <= '(b, _)) = Eval (a <= b)+++data Sort :: [a] -> Exp [a]+type instance Eval (Sort '[]) = '[]+type instance Eval (Sort (pivot ': rest)) =+ Eval (Eval+ (Eval (Sort (Eval (Filter (Flip (<=) pivot) rest)))+ ++ '[pivot])+ ++ Eval (Sort (Eval (Filter (Not <=< Flip (<=) pivot) rest))))++data DeleteBy :: (a -> a-> Exp Bool) -> a -> [a] -> Exp [a]+type instance Eval (DeleteBy _ _ '[]) = '[]+type instance Eval (DeleteBy p x (y ': ys)) =+ If (Eval (x `p` y)) ys (y ': Eval (DeleteBy p x ys))++data Foldl :: (b -> a -> Exp b) -> b -> t a -> Exp b+type instance Eval (Foldl _ e '[]) = e+type instance Eval (Foldl f e (x ': xs)) = Eval (Foldl f (Eval (f e x)) xs)+
+ src/Units/Simple/Quantity.hs view
@@ -0,0 +1,80 @@+{-# OPTIONS_GHC -Wno-missing-methods #-}++{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Units.Simple.Quantity+ ( Quantity (..)+ ) where++import GHC.TypeLits++import Units.Simple.Unit++-- |A numerical quantity with some associated unit.+-- Units are not created directly with this constructor,+-- but through the individual unit functions.+--+-- Examples:+--+-- >>> meter -- a unitary quantity associated to meters.+-- 1 m+-- >>> 2.5*ampere -- constructing through literal arithmetic+-- 2.5 A+-- >>> candela' 3.14 -- constructing through the unit constructors+-- 3.14 cd+-- >>> :set -XDataKinds+-- >>> 2 :: Quantity (SingleUnit 'Second) Rational+-- 2 % 1 s+--+-- Associated units are represented through a phantom parameter of the @Units@ kind synonym.+-- These are currently implemented as a type-level pair of lists representing the power+-- to which each unit is raised. Units can be inspected through @showUnits@.+--+-- New constructors may be written by combining the provided ones, such as+--+-- >>> let newton = kilogram .* meter ./ (second .* second)+-- >>> 23*newton+-- 23.0 kg*m/s^2+-- <BLANKLINE>+-- >>> let g = 6.67408e-11 * newton .* (meter .* meter) ./ (kilogram .* kilogram)+-- >>> g -- gravitational constant+-- 6.67408e-11 m^3/kg*s^2+-- >>> let gravity m1 m2 r = g .* (m1 * kilogram) .* (m2 * kilogram) ./ (r*meter .* r*meter)+-- >>> let earth_mass = 5.972e24 * kilogram+-- >>> let mars_mass = 6.417e23 * kilogram+-- >>> let earth_radius = 6371e3 * meter+-- >>> let mars_radius = 3389.5e3 * meter+-- >>> let weight_on_earth mass = gravity mass earth_mass earth_radius+-- >>> let weight_on_mars mass = gravity mass mars_mass mars_radius+-- >>> weight_on_earth (80 * kilogram)+-- 785.5719790179963 kg*m/s^2+-- >>> weight_on_mars (80 * kilogram)+-- 298.22370259533704 kg*m/s^2+-- >>> fromQuantity $ weight_on_mars 1 / (fromQuantity $ weight_on_earth 1)+-- 0.3796261966575378+newtype Quantity (us :: Units) a =+ Quantity {+ fromQuantity :: a -- ^Unwraps a @Quantity@, losing all unit information+ }+ deriving ( Eq+ , Ord+ , Enum+ , Num+ , Real+ , Integral+ , Fractional+ , Floating+ , Functor+ )++instance (KnownSymbol (UnitRepr us), Show a) => Show (Quantity us a) where+ show (Quantity x) = show x <> " " <> showUnits @us++instance Applicative (Quantity us) where+ pure = Quantity+ Quantity f <*> Quantity x = Quantity (f x)
+ src/Units/Simple/Unit.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+module Units.Simple.Unit where++import Data.Proxy+import GHC.TypeLits hiding (type (<=))++import Fcf hiding (type (<=))++import Units.Simple.Internals (Show', Intersperse, Sort, type (<=))++data Unit = Meter+ | Kilogram+ | Second+ | Ampere+ | Kelvin+ | Mole+ | Candela+ deriving (Eq, Ord, Show)++type Unit' = (Unit, Nat)+type Units = ([Unit'], [Unit'])++type family UnitSymbol (u :: Unit) :: Symbol+type instance UnitSymbol 'Meter = "m"+type instance UnitSymbol 'Second = "s"+type instance UnitSymbol 'Kilogram = "kg"+type instance UnitSymbol 'Ampere = "A"+type instance UnitSymbol 'Kelvin = "K"+type instance UnitSymbol 'Mole = "mol"+type instance UnitSymbol 'Candela = "cd"++data ShowUnit :: Unit' -> Exp Symbol+type instance Eval (ShowUnit '(u, n)) =+ If (Eval (TyEq n 1))+ (UnitSymbol u)+ (UnitSymbol u `AppendSymbol` "^" `AppendSymbol` Eval (Show' n))++type ShowUnitList (ul :: [Unit']) = Eval (Intersperse "*" =<< Map ShowUnit =<< Sort ul)++type UnitRepr' (num :: [Unit']) (denom :: [Unit']) =+ If (Eval (Eval (Null num) && Eval (Null denom)))+ "<adimensional>"+ (If (Eval (Null denom))+ (ShowUnitList num)+ (If (Eval (Null num))+ ("1/" `AppendSymbol` ShowUnitList denom)+ (ShowUnitList num `AppendSymbol` "/" `AppendSymbol` ShowUnitList denom)))++type UnitRepr (us :: Units) = UnitRepr' (Eval (Fst us)) (Eval (Snd us))++-- | A string representation of "Units". Useful for debugging.+showUnits :: forall us. KnownSymbol (UnitRepr us) => String+showUnits = symbolVal (Proxy @(UnitRepr us))++type instance Eval ((a :: Unit) <= (b :: Unit)) = Eval (UnitSymbol a <= UnitSymbol b)