AdaCore / ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
62 stars 28 forks source link

[feature] Enumeration values must support a wider range of types #93

Open Joebeazelman opened 2 years ago

Joebeazelman commented 2 years ago

Summary

Ada enumerations offer several advantages over constants:

Enumerations also have constraints. Their values must be either a numeric or a character type. Unfortunately, this creates severe limitations, rendering it anemic compared to other languages. Enumeration values need more type flexibility to enhance their expressive capabilities.

The code below demonstrates such a limitation with a brief explanation. For a more thorough discussion, including workarounds please refer to its source on stackoverflow:

type Bakers_Dozen is range 1 to 13;  -- Indices from 1 to 6 are donuts
subtype Donut is Bakers_Dozen (Plain, Chocolate, Strawberry, Glazed, Blueberry, Cannabis);
for Donut use (Plain=>1, Chocolate=>2, Strawberry=>3, Glazed=>4, Blueberry=>5, Cannabis=>6);  
PastriesBox[Plain].Message = "Plain Donut is boring but costs less";
PastriesBox[Donut'Last].Message = "Please read contradictions and disclaimer inside box.";
PastriesBox[12].Message = "A great tasting muffin with fresh goat milk.";

The intent of the specification is to build a baker's dozen of pastries with 13 numbered slots in a pastry box. The first 6 slots are reserved exclusively for donuts based on their type. Plain donuts go into the first slot, chocolate goes into the second slot, and so on. The rest of the slots are reserved for any other type of pastries. The last few lines are a usage scenario for the model. Clearly, the Donut enumeration values are used to index the slots in the pastry box, while numeric values are used to index regular pastry items.

Even though (NPI) Donut values are numeric, they cannot be subtyped like normal integers, nor can they be the same type as Bakers_Dozen. More broadly, constraining enumerations to only single characters or numeric types gives rise to this inflexibility. There's no reason why enumerations values can't support strings or any kind of value type.

Practical Use Case

Here's a real-world example to help illustrate the use case for this feature:

type Device_Address is mod 16#0F#;          -- 16 unique address location
for Device_Address'Size use 4;              -- Use only 4 bits for the address
subtype Fixed_Address is Device_Address (Serial, Parallel, PS2, Ethernet, Game, USB_1, USB2); -- Fixed addresses for default devices
for Fixed_Address use (0,1,2,3,4,5,6,7); 

Address : Device_Address := Game; 

Unfortunately, the code above will not compile. As a workaround, using a sub-type predicate will not compile either:

type Device_Address is mod 16#0F#;          -- 16 unique address location
for Device_Address'Size use 4;              -- Use only 4 bits for address
subtype Fixed_Address is Device_Address with
Static_Predicate =>
    Fixed_Address in (Serial, Parallel, PS2, Ethernet, Game, USB_1, USB_2);

Rewriting the code using constants works, but loses the aforementioned advantages of enumerations. Specifically, the code isn't as readable, loss of namespace and inability to iterate over the constant values.

    type Device_Address is mod 16#0F#;                                   -- 16 unique address location
    for Device_Address'Size use 4;                                             -- Use only 4 bits for the address space
    subtype Fixed_Address is Device_Address range 0 .. 6;    -- Lower half reserved for fixed devices
    Serial : constant Fixed_Address := 0;
    Parallel : constant Fixed_Address := 1;
    Ethernet : constant Fixed_Address  := 2;
    PS2: constant Fixed_Address := 3
    Game: constant Fixed_Address  := 4; 
    USB_1: constant Fixed_Address := 5; 
    USB_2: constant Fixed_Address  := 6;

Or as an alternative, adding a static predicate:

subtype Fixed_Address is Device_Address with Static_Predicate =>
    Fixed_Address in (Serial, Parallel, PS2, Ethernet, Game, USB_1, USB_2);

Motivation

Ada's enumeration constraints greatly reduce its utility. It often forces awkward, less safe, and less accurate workarounds when specifying a model, which is antithetical to Ada's stated principles. Increasing the flexibility of enumerations greatly expands Ada's expressive power.

Caveats and alternatives

There are workarounds offered on StackOverflow such as using constants and other more convoluted means, but they're incapable of modeling the problem as succinctly with the same level of accuracy, safety, and readability.

So long as Ada's type rules are respected, expanding enumerations values to support a wider range of types won't compromise in Ada's type system. Moreover, enumerations are constant values and should have no real side effects. Moreover, they do not introduce any significant performance or size penalties as constant value types can be optimized away at compilation.