5 ms·
Dependent typing can do that sort of thing. In fact, here's a stackoverflow answer that uses even numbers as an example of a dependent type: https://stackoverfl
by DennisP 5y ago
Dependent typing can do that sort of thing. In fact, here's a stackoverflow answer that uses even numbers as an example of a dependent type: https://stackoverflow.com/questions/9338709/what-is-dependent-typing https://stackoverflow.com/questions/9338709/what-is-dependen...
- taeric 5y agoRight. And I look forward to advances in them. I can count how many times this would have actually helped my program, though...
- exdsq 5y agoWhy do you think that? It might require a different mental model of types in order to see the benefits but I can't believe anyone is working on a project that doesn't have any sort of properties or 'business' logic that dependent types wouldn't help encode. Have you read anything about type-driven development? https://blog.ploeh.dk/2015/08/10/type-driven-development/ https://blog.ploeh.dk/2015/08/10/type-driven-development/
- taeric 5y agoI didn't mean for that to read as dismissive as it clearly does. Should have waited till I had more to say. :) I don't think the number of places dependent typing could have helped me is zero. Just like linear typing is nice. I just know that many of the dependencies I work with are much more dynamic in nature, such that getting them in static types has tough ROI to justify. Bluntly, the hardest program failures I've ever seen have been second systems from people learning generics and higher kinded types. I'm convinced these techniques are worth learning. I'm not convinced that they provide the immediate return on effort that they are usually sold with.
- exdsq 5y agoThat's fair, I somewhat agree - especially regarding the ROI to begin with :)
- Akronymus 5y agoEdit: It seems I confused dependant and algebraic types. Wouldn't you love the compiler giving an error when you write something that could result in illegal state? (Business rule violations for example) This is where such types shine. https://fsharpforfunandprofit.com/posts/designing-with-types-making-illegal-states-unrepresentable/ https://fsharpforfunandprofit.com/posts/designing-with-types...
- taeric 5y agoI actually meant my "looking forward" to be sincere. I've used tooling that can point out exactly where an injection attack is possible, and that was quite nice. That said, u expect more of these tricks in my tooling, not necessarily cuffed by me. Elsewhere I pointed to format strings checked at compile time for valid shape and arguments. This is actually common in lisps, ironically enough, and is akin to this sort of affordance. I have just also seen too many projects fail that thought they could get it all in the types. It is very frustrating.