Adding examples, with dependent types we can write the type-safe printf in Idris: https://github.com/chrisdone/sandbox/blob/master/dependently-typed-printf.idr

Adding examples, with dependent types we can write the type-safe printf in Idris: https://github.com/chrisdone/sandbox/blob/master/dependently-typed-printf.idr https://github.com/chrisdone/sandbox/blob/master/dependently... Meanwhile with Liquid Haskell (refinement types), it was really easy for me to define a date data type that can only construct valid year-month-day combinations: https://github.com/chrisdone/sandbox/blob/master/liquid-haskell-dates.hs https://github.com/chrisdone/sandbox/blob/master/liquid-hask... The `if ..` tests are all required, otherwise Liquid Haskell rejects the program. So I see value in both directions, if you extrapolate from these examples to harder problems.