Add proper support for units

[snowleopard]

For example, Variable Milli Watt. To be able to use Num instance, we should probably allow arbitrary addition and multiplication, but still reflect meaningless results in the type:

• 1 :: Variable Milli Watt + 2 :: Variable Milli Watt == 3 :: Variable Milli Watt.
• 1 :: Variable Milli Watt + 2 :: Variable Micro Watt == 3 :: Variable Error Watt.
• 1 :: Variable Milli Watt + 2 :: Variable Milli Seconds == 3 :: Variable Milli Error.

[geo2a]

I implemented a limited support for units of measurement via units package, please see Redfin.Language.Units and changes to Redfin.Examples.Energy.

For now, units are only used in the verification constraints (as we do in the paper). To be used as an underlying representation for units, a numeric type must be an instance of Fractional, therefore I'm not sure if the high-level language can be easily enriched with units considering the current design. We can do it for fixed-point numbers, but I'm not sure if the full power of the units package may be used for integer values.

At this moment, we have everything we claimed to have in the paper, and the syntax closely resembles our examples, but the proper support for units in the high-level language is still to be implemented.

[snowleopard]

@geo2a Thank you, looks promising!

Can't GHC infer Time here: (30 % Year :: Time) # Second? Presumably, Second implies Time? I think it would be a bit cleaner if we could write (30 % Year) # Second in the example.

At this moment, we have everything we claimed to have in the paper

But we can't do integers, can we? So the example from the paper doesn't really work.

[geo2a]

Can't GHC infer Time here: (30 % Year :: Time) # Second? Presumably, Second implies Time? I think it would be a bit cleaner if we could write (30 % Year) # Second in the example.

No, it can't, since the Time type, declared in Redfin.Language.Units, resolves the internal representation of units (Fixed in this case). In the units package, units of measurement are not tied to a concrete numeric type, therefore the abstract Second unit doesn't imply the concrete Time dimension.

I made the examples more ad-hoc, and now they resemble the paper ones as closely as possible

constrain $ t1 .>= 0 &&& t1 .<= toMilliSeconds (30 % Year)

toMilliSeconds :: Time -> Value
toMilliSeconds t = unsafeFixedToValue (t # milli Second)

But we can't do integers, can we? So the example from the paper doesn't really work.

We can, and we do, but with a limitation. The current implementation of fixed-point numbers (see Redfin.Data.Fixed has 8 out of 64 bits devoted to the fractional part. Therefore, we can cook up 56-bit values as Fixed and then convert the result to integral Value type. This is of suboptimal since we must make sure to use only integer literals to avoid rounding and also tracking the overflow by ourselves.

[snowleopard]

constrain $ t1 .>= 0 &&& t1 .<= toMilliSeconds (30 % Year)

Looks good!

The current implementation of fixed-point numbers (see Redfin.Data.Fixed has 8 out of 64 bits devoted to the fractional part.

What about switching from newtype Fixed = Fixed { getFixed :: Value } to something like this?

data Fixed = Fixed { getFixed :: Value, fixedToValue :: Value }

unsafeValueToFixed :: Value -> Fixed
unsafeValueToFixed x = Fixed (sShiftLeft x $ literal fracBits) x

Or something similar. Perhaps, we could also split integer and fractional parts into separate fields.