4 ms·
Maybe I'm missing the point of Dependent Types and there's more to it than I understood from the article, but in the example given of a divide function that req
by peterashford 12y ago
Maybe I'm missing the point of Dependent Types and there's more to it than I understood from the article, but in the example given of a divide function that requires a proof of a non-zero denominator: isn't this already achieved by languages that employ design by contract, such as Eiffel?
- dllthomas 12y agoMy understanding of DbC in Eiffel is that checks are done at runtime, rather than having a proof at compile time that the behavior cannot occur.
- tel 12y agoEiffel can promise that it will halt at runtime if a contract is violated. DT languages can promise that no contracts could ever be violated by any possible runtime evaluation pathway. The latter is much stronger, but weird sounding. What it typically means is that you are required to not cut corners. The type system will detect your failure to handle edge cases and refuse to compile until you either handle or explicitly ignore them.