4 ms·
Those invariants look to me pretty much like additional constructor arguments in languages with dependent types. Which both do "Make Illegal States Unrepresenta
by defanor 4y ago
Those invariants look to me pretty much like additional constructor arguments in languages with dependent types. Which both do "Make Illegal States Unrepresentable" and can provide "natural" ways to represent the data, along with the additional arguments (those proving the desired properties).
- Tainnor 4y agoTo be more precise, in Idris something like: data Interval : Type where From : (start : Int) -> Interval Until : (end : Int) -> Interval Bounded : (start : Int) -> (end : Int) -> {auto lt : LT start end} -> Interval could work (I haven't used Idris in a bit, so this might not compile as is). With this declaration this would compile: intervals : List Interval intervals = [ From 2 , Until 5 , Bounded 2 5 ] while this would not: interval : List Interval interval = Bounded 5 2 However, supplying that "lt" proof (implicitly or explicitly) could become tedious in some cases. The proof burden is often kind of a problem with dependent types. In such a case, the "start + offset" based approach might be preferable, even if it leads to a more complicated API.