Hi I'm experimenting with a unit system in haskell where users can add "base units". I want to reduce units after multiplication and bring it into a canonical form. The problem is what kind of types can the units have. 1) data UnitA data UnitB Problem: They can't be ordered so UnitA * UnitB can be compared to UnitB * UnitA, but I can't make a canonical form, which would make type inference a lot better. 2) type UnitA = Zero type UnitB = Suc Zero Problem: Now they can be ordered. But users can create conflicting "basic units" Silvio
http://hackage.haskell.org/package/units is a pretty deep example of how to have type-safe units. On Wed, Aug 12, 2015 at 4:20 PM, Silvio Frischknecht < silvio.frischi@gmail.com> wrote:
Hi I'm experimenting with a unit system in haskell where users can add "base units". I want to reduce units after multiplication and bring it into a canonical form. The problem is what kind of types can the units have.
1)
data UnitA data UnitB
Problem: They can't be ordered so UnitA * UnitB can be compared to UnitB * UnitA, but I can't make a canonical form, which would make type inference a lot better.
2)
type UnitA = Zero type UnitB = Suc Zero
Problem: Now they can be ordered. But users can create conflicting "basic units"
Silvio _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-- Chris Allen Currently working on http://haskellbook.com
Looks very nice. A bit large for my taste though. Anyway, it seems they can't order their units either. That's why (|+|) :: (d1 @~ d2, Num n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l n and not (|+|) :: (Num n) => Qu d l n -> Qu d l n -> Qu d l n This will always be a bit annoying. You can almost never safely write Qu (Foo :* Bar) l n but will always have to write (d @~ (Foo :* Bar)) => Qu d l n in your types. Silvio
Btw I think I found a solution in https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html there is a type level sort type family CmpSymbol m n :: Ordering This might work. Silvio
Hi Silvio, I'm the author of the units package. Yes, the types are annoying and painfully indirect, exactly because of the problem you identify. CmpSymbol might work for you. Note that it works only on Symbols (type-level strings) and not arbitrary types. I didn't like it because I wanted it to be possible to leverage Haskell's module system to allow distinct units but with the same name, declared in different modules. (For example, "pound" can refer to a plethora of different units.) This requirement may have been a step too far, and I'd be curious to see how much the system could be simplified without it. Good luck! Richard On Aug 12, 2015, at 7:41 PM, Silvio Frischknecht <silvio.frischi@gmail.com> wrote:
Btw I think I found a solution in
https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html
there is a type level sort
type family CmpSymbol m n :: Ordering
This might work.
Silvio _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
CmpSymbol might work for you. Note that it works only on Symbols (type-level strings) and not arbitrary types. I didn't like it because I wanted it to be possible to leverage Haskell's module system to allow distinct units but with the same name, declared in different modules. (For example, "pound" can refer to a plethora of different units.) This requirement may have been a step too far, and I'd be curious to see how much the system could be simplified without it.
I'm currently trying to achieve this by combining Symbols with Typeable and TemplateHaskell. Should be possible. Silvio
What kind of units are these? dimensional normalizes units by representing them like Foo Int Int Int. (Those are type-level "ints".) So if length is Foo 1 0 0 and time is Foo 0 1 0, then length* time = Foo 1 1 0 = time* length. Does this work for your application? --Will
On Aug 12, 2015, at 14:20, Silvio Frischknecht <silvio.frischi@gmail.com> wrote:
Hi I'm experimenting with a unit system in haskell where users can add "base units". I want to reduce units after multiplication and bring it into a canonical form. The problem is what kind of types can the units have.
1)
data UnitA data UnitB
Problem: They can't be ordered so UnitA * UnitB can be compared to UnitB * UnitA, but I can't make a canonical form, which would make type inference a lot better.
2)
type UnitA = Zero type UnitB = Suc Zero
Problem: Now they can be ordered. But users can create conflicting "basic units"
Silvio _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
participants (4)
-
Christopher Allen -
Richard Eisenberg -
Silvio Frischknecht -
Will Yager