CC: Functional dependencies question

[Andrew J Bromage]

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