CC: Functional dependencies question
Andrew J Bromage
ajb@spamcop.net
Tue, 13 May 2003 12:42:17 +1000
G'day all.
On Mon, May 12, 2003 at 12:35:39PM -0700, oleg@pobox.com wrote:
> bar ::tbar
> = (foo::(Char->tbar)) 'a'
>
> instance Foo Char Bool where
> foo c = c == 'a'
> *Main> bar
> True
>
> and the code even runs.
That's a very ingenious solution, but unfortunately it doesn't solve
the "larger" problem.
The full ugly details of what I'm trying to do is that I'm trying
to support unit-safe physical computations. For that, we need a way
to encode phyics units (e.g. mass, force, energy etc) in Haskell's
type system and then use phantom types to guarantee correctness.
We know how to encode natural numbers:
data Peano0 = Peano0
data PeanoSucc n = PeanoSucc
with operations such as:
class PeanoAdd l r n | l r -> n
instance PeanoAdd Peano0 r r
instance (PeanoAdd l r n) => PeanoAdd (PeanoSucc l) r (PeanoSucc n)
That's straightforward. However, we actually need integers (hereafter
called "whole numbers" so as not to confuse with Haskell Integers), not
just natural numbers. We can do this using a pair of natural numbers
(m,n) which corresponds to the integer m-n:
data Whole m n = Whole
Each Whole number has a unique representation where at least one of
m or n is zero:
class WholeUniqueRep m n | m -> n
instance WholeUniqueRep (Whole Peano0 Peano0)
(Whole Peano0 Peano0)
instance WholeUniqueRep (Whole (PeanoSucc m) Peano0)
(Whole (PeanoSucc m) Peano0)
instance WholeUniqueRep (Whole Peano0 (PeanoSucc n))
(Whole Peano0 (PeanoSucc n))
instance (WholeUniqueRep (Whole m n) uniq) =>
WholeUniqueRep (Whole (PeanoSucc m) (PeanoSucc n)) uniq
Some sample whole numbers in unique form include:
type WholeN1 = Whole Peano0 Peano1
type Whole0 = Whole Peano0 Peano0
type Whole3 = Whole Peano3 Peano0
where Peano1 = Succ Peano0 etc.
We can then do operations on Whole numbers such as addition:
class WholeAdd l r n | l r -> n
instance (PeanoAdd m1 m2 m3, PeanoAdd n1 n2 n3,
WholeUniqueRep (Whole m3 n3) w) =>
WholeAdd (Whole m1 n1) (Whole m2 n2) w
A physical unit is some product of integral powers of some set of
basis units, such as a length unit and a mass unit. For example:
newtype PhysicalUnit length mass time
= PhysicalUnit Double
Sample units include:
-- basis units
type Length -- e.g. metre
= PhysicalUnit Whole1 Whole0 Whole0
type Mass -- e.g. kilogram
= PhysicalUnit Whole0 Whole1 Whole0
type Time -- e.g. second
= PhysicalUnit Whole0 Whole0 Whole1
-- derived units
type Acceleration -- e.g. m/s^2
= PhysicalUnit Whole1 Whole0 WholeN2
type Force -- e.g. Newton
= PhysicalUnit Whole1 Whole1 WholeN2
type Energy -- e.g. Joule
= PhysicalUnit Whole2 Whole1 WholeN2
Addition and subtraction can only be done on matching units:
class Add l r n | l r -> n where
add :: l -> r -> n
instance Add (PhysicalUnit a1 b1 c1)
(PhysicalUnit a1 b1 c1)
(PhysicalUnit a1 b1 c1) where
add (PhysicalUnit m) (PhysicalUnit n) = PhysicalUnit (m+n)
Multiplication is done by adding powers:
class Mult l r n | l r -> n where
mult :: l -> r -> n
instance (WholeAdd a1 a2 a3,
WholeAdd b1 b2 b3,
WholeAdd c1 c2 c3) =>
Mult (PhysicalUnit a1 b1 c1)
(PhysicalUnit a2 b2 c2)
(PhysicalUnit a3 b3 c3)
where
mult (PhysicalUnit m) (PhysicalUnit n) = PhysicalUnit (m*n)
We can now write functions such as:
newtonsSecondLaw :: Mass -> Acceleration -> Force
newtonsSecondLaw m a = m `mult` a
OK, that's the part that works. Now here's the problem...
I want people to be able to specify PhysicalUnit types without worrying
about how they're implemented at the _type_ level. Suppose, for
example, you want to declare Planck's constant. It's units are Joule
seconds, i.e. the Energy unit multiplied by the Time unit. I want
people to be able to write something like:
hbar :: (Mult Energy Time t) => t
hbar = PhysicalUnit 6.62606876e-34
rather than give the full type of t. I can't give a type synonym
for it, either, because I don't know the full set of physical units
that people will want to work with.
Besides, I want to be able to extend or change the PhysicalUnit type
without requiring people to rewrite their code.
Today, we only need length, mass and time. Tomorrow we might need the
full SI basis set:
newtype PhysicalUnit length mass time current temperature
lightIntensity amount
= PhysicalUnit Double
Cheers,
Andrew Bromage