cucapra/dahlia

Adding literal to represent fixed type

Closed this issue · 5 comments

Fixed type is tricky since 0.2 has no way to be represented as precise binary number.
So we will add a new inference rule for the syntax "Let". Using "f'0.5" means the number is going to be represented in minimal number of required, <1,0> in this case. If a number is not able to be represented by fixed point, the program will give an error.
On the other hand, if one does not specify the literal"f'", the implicit inference will take the number as double if there is a decimal point. For example, "Let x = 0.5" says x will be inferred as 0.5 by default.

Indeed! It does seem like let x = 0.5 should declare a double by default. It might be nice to support something like let x: bit<1, 0> = 0.5 but that might be too annoying to make work in general…

However, about flagging an error when representation isn't exact: it is worth keeping in mind that 0.2 also can't be represented exactly in floating point, even in 64 bits. So in that sense, I'm not sure it makes sense to make it an error to treat 0.2 as fixed point but not to treat it as floating point. But I do see your point (ha) about the literal itself, like f0.2 or whatever, not having a reasonable fixed-point type you can infer.

Yes, it's so hard to come up with any idea other than introducing a literal.
Consider let x:bit<2> = 10, let y:fix<2,1>=0.2, let y:fix<2,1>=f'0.2.
10 is SizedInt so Fuse knows minimal bit to represent 10 is 4 and this let x syntax is not valid.
In the case of fix point, Fuse find it hard to know minimal number of bit to represent 0.2, so we have to store it in double.
However, [let y: fix<2,1> = some number] should be valid. In that case, the only method we have discussed till now is introducing literal.

Or, we can ignore type inferring for any decimal number since there will always be a way to represent it. But it seems inconsistent with Integer/bit inference.

I'm still in favor of having separate fixed point literals. More precisely (ha):

  • let x = 1.2 gives x the type double.
  • let x = f1.25 gives the smallest fixed point type that can represent it. However, fixed point representation might be unintuitive, so we could also take the more radical approach of exactly specifying the size of the literal using f<1,2>1.2 since we generate slightly better error messages for this. This also reminds me of how P4 implements sized integers (section 7.1.6.6).
  • let x = f1.2 errors out since there is no fixed for representation for it.

One thing to realize here is that no matter what solution we implement (removing type inference vs. sized literals), fixed points will be cumbersome to use because a Dahlia program will be tied to it's choice of double vs. fixed point at some level.

The ideal solution would require a thoughtful redesign of the type system to have bitwidth polymorphism (which is surprisingly hard, as the P4 team learned). This is just a stepping stone for that.

Here's a funky idea that might be terrible. The idea would be to let both of these assignments, which both involve rounding, to work the same way:

let x: double = 1.2;
let y: fix<1,2> = 1.2;

Literals could have a new type for representing exact numbers. You could call it Rational, for example, because it can precisely represent any number with a finite number of decimal (or other base?) digits. Rationals can be freely converted to any approximate number type, including double, fix<N, M>, perhaps even bit<M>, and perhaps a future generalized float<N, M>.

Rationals must always be compile-time constants, exactly like our current TStaticInt, because they can't in general be represented at run time. Instead, when they get converted to some other number type, we can statically do the conversion and emit the concrete value of the appropriate type.

If you want to use a literal as part of a larger expression, you use casting to describe the type you want:

let x = (1.2 as double) + some_function();
let y = (1.2 as fix<1,2>) + other_function();

Relying on casts obviates the need for us to cook up special literal syntax for each numeric type. For example, this would free us from coming up with a prefix to distinguish float and double eventually, and perhaps even arbitrary-precision floating-point numbers.

For bonus points, we could even support compile-time arithmetic on these constants.

Fixed by #257.