Add types representing ranges of numbers

[zimri-leisher]

FPP should support "refinement types" https://en.wikipedia.org/wiki/Refinement_type

Apparently this has already been done in Haskell, TypeScript, Rust and Scala (although I don't know if they are first-class language features, or just libraries inside of the language).

A good design should start by looking at how these languages implement this feature.

Adding this would implicitly allow parameter and command argument verification. It could also be used in cases such as port arg types, port return types, telemetry types, etc for various use cases, many of which I don't know if we've fully explored.

As a first draft, I propose a syntax/semantics somewhat like:

[ dictionary ] type identifier = type-name where type-refinement

The "identifier" is the name R of the refined type.

"type-refinement" is a type refinement expression. A type refinement expression must evaluate to a Boolean. We could create a "dummy variable" called value or something which is in scope only in the type refinement expression, and nowhere else. The type of the dummy variable would be the type T referred to by type-name. For a given value V of T, V would be a value of R iff the type refinement expression evaluates to True when the dummy variable is assigned value V.

Likely, a common usage pattern would look like this:

SomeComponentParams.fppi:

type ValidTemperatureRange = F32 where value > -120 and value < 150
param HEATER_ON_MIN: ValidTemperatueRange

So these types would often be defined right next to the parameter. Even better, we could allow "anonymous" definitions of these types, so you could say:

param HEATER_ON_MIN: F32 where value > -120 and value < 150

In this case, F32 where value > -120 and value < 150 would be a new nameless type.

[bocchino]

"type-refinement" is a type refinement expression. A type refinement expression must evaluate to a Boolean.

I think we should start with a simple version of this -- for example, a constraint that a numeric value has to be within a specified constant range. That would be easy to check statically and would cover many cases.

[zimri-leisher]

Okay, so you're suggesting that the type refinement expression be limited to a subset of expressions with Boolean values, maybe of the form:
value > -10 and value < 100
Is that correct?

Or are you suggesting that we use some different syntax to denote the valid range?
Some ideas:

type ValidTemperatureRange  = F32 min -100 max 100

type ValidTemperatureRange  = F32 valid -100 to 100

type ValidTemperatureRange  = F32 in {-100, 100] # this one seems like one you'd like haha

type ValidTemperatureRange  = F32 in -100 .. 100

The con of having new syntax instead of just reusing the existing expression syntax is that if we were to allow arbitrary boolean expressions in the future, we would be in the awkward place of supporting both the old syntax and the new. Probably bad to have two ways to do it. So I think using custom syntax would probably lock us into place.

[bocchino]

I was not suggesting any particular syntax. I was suggesting that semantically we start by supporting ranges of numbers, because they seem to be the most useful case, and it's easy to compute subtypes (set inclusions) for ranges. The suggestion sketched above allows (at least) arbitrary unions and intersections of ranges, e.g.,

F32 where (value > 0 and value < 1) or (value >= 10 and value <= 11)

This could be written as a set comprehension as follows:

F32 in { x : ( x > 0 and x < 1 ) or (x >= 10 and x <= 11 ) }

or as a union of ranges as follows:

F32 in (0, 1) U [10, 11]

Computing common types and subtypes for these types may not be hard if each subexpression is a constant or a single free variable, but it may be more complexity than we need. In the presence of choice (e.g., at a choice in a state machine), the terms might accumulate, and the checking might be at least linear in the number of terms. For example, in general the common type of F32 in X and F32 in Y might be F32 in (X U Y); but if X and Y are intervals with constant bounds, then (X U Y) could be approximated by an interval Z that could be computed in common time.

The con of having new syntax instead of just reusing the existing expression syntax is that if we were to allow arbitrary boolean expressions in the future, we would be in the awkward place of supporting both the old syntax and the new.

I am not following this argument. FPP currently doesn't support Boolean expressions in any form except the Boolean values true and false. So whatever we add to express type constraints is going to be new.

My preference at this time would be to add ranges such as F32 in [0, 1] or F32 in (0, 1) or F32 in [0, 1). This is what we did before when we prototyped command validation. If we eventually wanted to allow more general set comprehensions, we could do that. The range syntax [0, 1] would just be syntax sugar for the more general (and more verbose) set comprehension { x : x >= 0 and x <= 1 }. This seems fine. But do we need this? What can we express with general comprehensions that we can't express with ranges? Also, I don't want to use a magic variable name like value for the free variable in the set comprehension. If we introduce a variable, it should be declared.

[bocchino]

Computing common types and subtypes for these types may not be hard if each subexpression is a constant or a single free variable, but it may be more complexity than we need.

In general, if S and T are arbitrary sets, then you need a SAT solver (or something like it) to decide whether the type F32 in S can be assigned to the type F32 in T. And rules like this can quickly become undecidable. If you're not careful, you can easily create a set of typing rules that cause the system to hang or to give up.

[bocchino]

In general, if S and T are arbitrary sets, then you need a SAT solver (or something like it) to decide whether the type F32 in S can be assigned to the type F32 in T.

If you restrict to constant ranges and the operations union and intersection, then I think every set can be represented as a union of disjoint ranges. Then computing a common type or a subtype for a union of n disjoint ranges and a union of m disjoint ranges can be done in mn operations. This seems doable, but it may be more complex than necessary.

[bocchino]

Other reasons to keep the types and the type checking simple:

• If you restrict to intervals, then it's clear how to cast values. For example, the value 3 at the type U8 in [0, 2] is 2. The value 3 at the type U8 in [0, 2] U [4, 5] or U8 in { x : e(x) } where e is some arbitrary expression is less clear.
• We may need to check type constraints at runtime. For example, suppose you define a port with an argument whose type is U32 in S where S is some set. We probably want to generate code to assert that the value passed into the port is in set S and/or cast an out-of-range value so it is in range. We don't want to generate very complicated code here.

[zimri-leisher]

I am not following this argument. FPP currently doesn't support Boolean expressions in any form except the Boolean values true and false. So whatever we add to express type constraints is going to be new.

For some reason I mistakenly thought comparison operators and other similar Boolean operators were in FPP, my bad. A little hallucination.

What can we express with general comprehensions that we can't express with ranges?

Honestly, good point, I'm not able to immediately think of any reason we couldn't do with just ranges.

If you restrict to constant ranges and the operations union and intersection, then I think every set can be represented as a union of disjoint ranges.

Is there a particular reason we need union and intersection? I think you've convinced me that we should keep this quite simple.

For example, the value 3 at the type U8 in [0, 2] is 2. The value 3 at the type U8 in [0, 2] U [4, 5] or U8 in { x : e(x) }

Is there a world where we disallow casting to one of these refinement types if the original value is outside the defined range? For instance, I think it would be somewhat confusing to be able to do this:

type RefinedType = U8 in [0, 2]

param RefinedParam: RefinedType default 255 # should this really be allowed? seems potentially dangerous

We may need to check type constraints at runtime.

We definitely need to check them at runtime. I was assuming that the constraints would be enforced both by the GDS and the FSW, for commands, params, telemetry, ports

[zimri-leisher]

We would need some way to express just a minimum (no explicit maximum), and vice versa. Maybe something like:

type RefinedType = U8 in [0, inf)

maybe U8 in [0, ...) could work?

[bocchino]

Is there a particular reason we need union and intersection? I think you've convinced me that we should keep this quite simple.

OK, sounds good.

Is there a world where we disallow casting to one of these refinement types if the original value is outside the defined range?

In the modeling, it's probably best to disallow the conversion by default. We could also have an explicit cast operation.

We would need some way to express just a minimum (no explicit maximum), and vice versa.

When we prototyped this before, we used a missing bound as "no bound." For example, (0, ) represented the positive integers.

[zimri-leisher]

One comment I thought of about the use of mathematical set notation: it may be error prone to allow ( and [ in the same spot with a different meaning. I'm not aware of any standard PLs where these two are commonly semantically valid in the same spot. My worry is that reviewers may not be used to differentiating between them. They are quite similarly shaped, and a mistake could be easy to miss.
It's worth considering syntax like: (=-10, 11), so maybe the (= or =) together could replace [ or ]