3 ms·

My reading of the OP is that these techniques (branding, nominal typing, &c) are good and useful, but it's even better if you can remove/minimize the necessity

by nimih 6y ago

My reading of the OP is that these techniques (branding, nominal typing, &c) are good and useful, but it's even better if you can remove/minimize the necessity of ever trusting software developers to make reasonable decisions. Speaking from experience, even on personal projects where I am fully in control of my requirements and deadlines and the only person who has ever and will ever touch a codebase is me, I have regretted trusting software developers to make reasonable decisions w/r/t an internal (let alone external) API. Less cynically, if you have assumptions and facts present about your data at runtime, it makes good sense to spend some extra effort encoding them explicitly in the data representation when your type system supports it, rather than allowing them to exist implicitly (or by documentation only) as a tag. Even if you discount the advantages provided in shrinking how much you are forced to trust your users, reifying your knowledge about a piece of data gives the compiler (and other static analysis tools) more information to help you write the code in the first place: The article provides some examples in terms of exhaustiveness checking, but you can also leverage such things if you have access to fancy toys like refinement types, dependent types, or a development environment that can do tactics-style interactive transformations. IMO it also makes your code easier to read and understand, but that might just be a matter of taste.

lmm 6y ago
So I think that's true as far as it goes, but vastly overstates how much difference fully constructive types actually make. Starting to use types, even nominal ones, to express your requirements is a real game changer, a step change in your defect rate: it turns making a correct program from an intractable global problem into a compositional problem that you can reason about locally. Using constructive types is a technique that eliminates a couple of rare classes of errors. It's fine, and if you can do it cheaply (which is pretty rare in practice IME) then it's worth doing, but it's really not a major difference-maker. And I think a post like this could easily give the impression that newtypes aren't all that, so to speak, when nothing could be further from the truth.

by nimih 6y ago

lmm 6y ago

So I think that's true as far as it goes, but vastly overstates how much difference fully constructive types actually make. Starting to use types, even nominal ones, to express your requirements is a real game changer, a step change in your defect rate: it turns making a correct program from an intractable global problem into a compositional problem that you can reason about locally. Using constructive types is a technique that eliminates a couple of rare classes of errors. It's fine, and if you can do it cheaply (which is pretty rare in practice IME) then it's worth doing, but it's really not a major difference-maker. And I think a post like this could easily give the impression that newtypes aren't all that, so to speak, when nothing could be further from the truth.