News for hackers. Stuff that matters.

A comment on Types as Interfaces. Parent comment

Re:Types as Interfaces by andsoitis on Tuesday July 23, 2024 @08:33AM (#41045297)
> arbitrary rules a programmer knows about the bounds of a value

Ada's generalized type contracts using subtype predicates work pretty well for this: https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel...

You can use it for something as simple as expressing ranges, or to represent types with arbitrary constraints, including types with discontinuities.

[ Parent | on HN ]
Re:Types as Interfaces by kqr on Tuesday July 23, 2024 @09:04AM (#41045554)
But these are only promised to be checked at runtime, even though the compiler can sometimes hint at things earlier.
[ Parent | on HN ]
Re:Types as Interfaces by docandrew on Tuesday July 23, 2024 @09:13AM (#41045646)
With SPARK mode you can check them at compile-time with provers and elide the runtime checks. You can do _very_ sophisticated type predicates this way.
[ Parent | on HN ]