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.

[0] https://www.manning.com/books/type-driven-development-with-i...

[1] https://manning-content.s3.amazonaws.com/download/a/580d6ba-...