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