Hacker News Reader

Comment by defanor | Hacker News Reader

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).

View on HN

To 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.

Reply on news.ycombinator.com