Re: Extensible static checking of dimensions?
Mike Gunter <m <at> ryangunter.com> wrote: | The very nice Buckwalter and Denney dimensional-numbers packages both | work on a fixed set of base dimensions. This is a significant | restriction for me--I want to avoid adding apples to oranges as well | as avoiding adding meters to grams. Is it possible to have an | extensible set of base dimensions? If so, how usable can such a | system be made? Is it very much worse than a system with a fixed set | of base dimensions? Mike, I apologize for not having replied to your message earlier, I have not been subscribing to the café and only recently noticed your post in the archives. As for you question, please see the literate haskell module below. It allows you to extend the set of SI base dimensions in 'Buckwalter.Dimensional' with an arbitrary number of extra dimensions. My hope is that it lifts the significant restriction you saw previously. As for the usability of such a system, once you have set up the dimensions relevant to your problem domain usage should be identical to (and seamless with) the original base dimensions. You will have to be the judge as to whether it is usable enough for you. I would certainly appreciate comments on usability. In fact I would also be interested to hear how you envision applying the functionality you requested, regardless of this modules usefulness. Also, I can't promise that the module is rock solid -- I haven't done a whole lot of testing. If you don't have the 'Buckwalter.NumTypes' and 'Buckwalter.Dimensional' modules already you can download the latest tarball with all three modules from the project web site at: http://code.google.com/p/dimensional/ Thanks, Björn Buckwalter ~~~~~~~~~~ BEGIN 'Buckwalter/Dimensional/Extensible.lhs' ~~~~~~~~~~ Buckwalter.Dimensional.Extensible -- Extensible physical dimensions Bjorn Buckwalter, bjorn.buckwalter@gmail.com License: BSD3 = Summary = On January 3 Mike Gunter asked[1]: | The very nice Buckwalter and Denney dimensional-numbers packages | both work on a fixed set of base dimensions. This is a significant | restriction for me--I want to avoid adding apples to oranges as | well as avoiding adding meters to grams. Is it possible to have | an extensible set of base dimensions? If so, how usable can such | a system be made? Is it very much worse than a system with a fixed | set of base dimensions? In this module we facilitate the addition an arbitrary number of "extra" dimensions to the seven base dimensions defined in 'Buckwalter.Dimensional'. A quantity or unit with one or more extra dimensions will be referred to as an "extended dimensional". = Preliminaries = Similarly with 'Buckwalter.Dimensional' this module requires GHC 6.6 or later.
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
module Buckwalter.Dimensional.Extensible where
import Prelude hiding ((*), (/), (+), (-), (^), sqrt, negate, pi, sin, cos, exp) import qualified Prelude as P ((*), sin, cos, exp) import Buckwalter.NumType (NumType, Add, Sub, Halve, Negate, Zero, Pos1) import Buckwalter.Dimensional hiding (square, cubic, sin, cos, exp)
= DExt, Apples and Oranges = We define the datatype 'DExt' which we will use to increase the number of dimensions from the seven SI base dimensions to an arbitrary number of dimensions. We make 'DExt' an instance of 'Dims' allowing us to use the 'Dimensional' type without change.
data (NumType n, Dims d) => DExt n d instance Dims (DExt n d)
Using 'DExt' we can define type synonyms for extended dimensions applicable to our problem domain. For exampel, Mike Gunter could define the 'Apples' and 'Oranges' dimensions and the corresponding quantities. ] type DApples = DExt Pos1 (DExt Zero DOne) ] type DOranges = DExt Zero (DExt Pos1 DOne) ] type Apples = Quantity DApples ] type Oranges = Quantity DOranges And while he was at it he could define corresponding units. ] apple :: Num a => Unit DApples a ] apple = Dimensional 1 ] orange :: Num a => Unit DOranges a ] orange = Dimensional 1 = Arithmetic = We get negation, addition and subtracton for free with extended dimensionals. However, we will need instances of the 'Mul', 'Div' and 'Sqrt' classes for the corresponding operations to work.
instance (Add n n' n'', Mul d d' d'') => Mul (DExt n d) (DExt n' d') (DExt n'' d'')
instance (Sub n n' n'', Div d d' d'') => Div (DExt n d) (DExt n' d') (DExt n'' d'')
instance (Halve n n', Sqrt d d') => Sqrt (DExt n d) (DExt n' d')
Now, in order to work seamlessly with the quantities and units defined in 'Buckwalter.Dimensional' we must be able to automatically extend their dimensions when multiplying or dividing by an extended dimensional.
instance (Mul d (Dim l m t i th n j) d') => Mul (DExt x d) (Dim l m t i th n j) (DExt x d') instance (Mul (Dim l m t i th n j) d d') => Mul (Dim l m t i th n j) (DExt x d) (DExt x d')
instance (Div d (Dim l m t i th n j) d') => Div (DExt x d) (Dim l m t i th n j) (DExt x d') instance (Div (Dim l m t i th n j) d d', Negate x x') => Div (Dim l m t i th n j) (DExt x d) (DExt x' d')
The above instances also enable taking integer powers of extended dimensionals. To allow dimensionless quantities to be raised to the power of any other dimensionless quantity (where either or both of the quantities may be an extended dimensional) some new 'Power' instances are required.
instance (Floating a, Power a d (Dimensionless a) DOne) => Power a (DExt Zero d) (Dimensionless a) DOne where (Dimensional x) ^ (Dimensional y) = Dimensional (x ** y)
instance (Floating a, Power a DOne (Quantity d a) DOne) => Power a DOne (Quantity (DExt Zero d) a) DOne where (Dimensional x) ^ (Dimensional y) = Dimensional (x ** y)
instance (Floating a, Power a d (Quantity d' a) DOne) => Power a (DExt Zero d) (Quantity (DExt Zero d') a) DOne where (Dimensional x) ^ (Dimensional y) = Dimensional (x ** y)
Note that the extra dimensions are dropped from the result. This is acceptable since they will be added again as necessary when multiplying or dividing by extended dimensionals. = Elementary functions, 'square' and 'cubic' = In 'Buckwalter.Dimensional' the elementary functions where restricted to dimensionals with the physical dimension 'DOne'. The same applies to the 'square' and 'cubic' functions and the 'DLength' dimension respectively. Unfortunately this implementation is inflexible in that it will not accomodate extended dimensionals even if they have no extend into the extra dimensions (i.e. the powers are all 'Zero'). To solve this problem we must provide new, generalized implementations of such functions. We start by defining the class 'BaseDim' which relates extended dimensions to the corresponding base dimension if applicable. An extended dimension has a corresponding base dimension if the powers of all extra dimensions are 'Zero'. Two 'BaseDim' instances are required.
class BaseDim d d' | d -> d' instance BaseDim (Dim l m t i th n j) (Dim l m t i th n j) instance (BaseDim d d') => BaseDim (DExt Zero d) d'
Using 'BaseDim' in the constraints we can now redefine the elementary functions. As with the 'Power' instances above we drop the extra dimensions from the results.
sin, cos :: (Floating a, BaseDim d DOne) => Quantity d a -> Dimensionless a sin (Dimensional x) = Dimensional (P.sin x) cos (Dimensional x) = Dimensional (P.cos x)
exp :: (Floating a, BaseDim d DOne) => Quantity d a -> Dimensionless a exp (Dimensional x) = Dimensional (P.exp x)
Ditto for 'square' and 'cubic'.
square :: (Num a, BaseDim d DLength) => Unit d a -> Unit DArea a square (Dimensional x) = Dimensional (x P.* x) cubic :: (Num a, BaseDim d DLength) => Unit d a -> Unit DVolume a cubic (Dimensional x) = Dimensional (x P.* x P.* x)
(As a side note we could probably use 'BaseDim' to clean up the constraints and/or reduce the instances of 'Power' above, and perhaps for 'Mul' and 'Div'.) = References = [1] http://www.haskell.org/pipermail/haskell-cafe/2007-January/021069.html
participants (1)
-
Björn Buckwalter