I always thought this kind of thing was abstruse and impractical until I read Type-Driven Development with Idris[0], which made basic dependent type examples--like those demonstrated in the posted article--completely straightforward. Turns out that this kind of thing isn't actually that hard with the right language and tooling.
I highly recommend buying the book and checking out Idris if you found this article interesting. Read the free "overview" chapter[1] at least.
This was one of the reasons I felled in love with Turbo Pascal back in the day.
Algol derived languages, while not as powerful as ML ones regarding the type system offer quite a few possibilities to ensure safer code via type definitions, ranges, enumerations and ADTs (Abstract Data Types not to confuse with Algebraic data types).
C++ also allows for this, but requires a bit of boilerplate with templates, classes and operator overloading, which is way more work than a few type declarations in Haskell or Idris.
Yes, this was exactly my feeling reading through the Idris book. In the same way that a few lines of elegant Haskell can sometimes describe functionality that takes all kinds of technically-works-but-only-the-author-understands-it C++ template abuse, a few lines of straightforward Idris can sometimes replace all kinds of Haskell "type family abuse".
all kinds of s can be elegantly described in a few lines of Haskell,
I highly recommend buying the book and checking out Idris if you found this article interesting. Read the free "overview" chapter[1] at least.
[0] https://www.manning.com/books/type-driven-development-with-i...
[1] https://manning-content.s3.amazonaws.com/download/a/580d6ba-...