3 ms·
Dialyzer solves certain problems for me that still exist in many "typed" languages. A great example is pos_integer(). In something like Typescript I can use "nu
by technion 6y ago
Dialyzer solves certain problems for me that still exist in many "typed" languages. A great example is pos_integer(). In something like Typescript I can use "number", but that doesn't assert I can't receive a negative number, or a zero.
- eru 6y agoIn general, you'd need something like dependent types for solving this properly. Like eg Agda has.
- wwright 6y agoAda has this without general dependent types AFAIK
- mcguire 6y agoYes and no. The definitions are in the type system, but the checks are done at runtime, just like you would do manually. You don't really get the benefit of typing. The reason I can say that: you don't have to provide proofs that a value has to be positive to get things to compile.
- eru 6y agoChecks at runtime are also a good idea, but yes, very different from static dependent types. There's some interesting work on making such contracts work well in a lazy language with higher-order functions.