3 ms·
There's a small difference between type-level programming and type-driven programming, Idris does the latter while Rust the former (at least in my opinion). The
by sondr3 3y ago
There's a small difference between type-level programming and type-driven programming, Idris does the latter while Rust the former (at least in my opinion). The library uses types to make illegal states impossible and therefore should qualify as type-level programming.
- mrkeen 3y agoBut there's no programming at the type level. The programming in the article is at the level of values (insofar as what is shown.).