Remix.run Logo
GhosT078 3 days ago

This tradeoff sounds similar to the choice to use "tagged types" versus "variant records" in Ada. Ada has provided variant records since 1983 and tagged types since 1995 (and both with a very nice syntax).

wk_end 3 days ago | parent [-]

According to this [0] tutorial, variant records in Ada have the downside that you only get an error at runtime if you use them incorrectly, i.e. access data from one branch of the sum type when the actual value is on another. That's a pretty huge drawback.

https://learn.adacore.com/courses/intro-to-ada/chapters/more...

csb6 3 days ago | parent | next [-]

Ada doesn’t have pattern matching, so there is no way for it to enforce that only the valid fields are accessed except at runtime (beyond warnings if the discriminant is known at compile time). Most people would just use a case statement that checks the variant discriminant before accessing any fields.

I believe the SPARK subset can (through static analysis) ensure that only valid fields are accessed for the current discriminant.

GhosT078 3 days ago | parent | prev [-]

I'm not sure I understand your point. Is it about such an error being reported at run time versus compile time? The GNAT compiler will often provide compile time warnings that "Constraint_Error will be raised at run time" in many such scenarios. Other Ada type checks would make this scenario improbable (although it could be contrived).