Hacker News Reader

Read the article more carefully. I wrote in multiple places that the use of newtypes does provide real safety.

> If you are fond of newtypes, this whole argument may seem a bit troubling. It may seem like I’m implying newtypes are scarcely better than comments, albeit comments that happen to be meaningful to the typechecker. Fortunately, the situation is not quite that grim—newtypes can provide a sort of safety, just a weaker one.

> […]

> This tradeoff may not seem all that bad, and indeed, it is often a very good one! Guaranteeing invariants using constructive data modeling can, in general, be quite difficult, which often makes it impractical.

> […]

> Newtypes are useful when carefully applied

The whole point of the blog post is that newtypes are useful, but only when used in certain ways and in a weaker sense than constructive data modeling.

Definitely agree the best approach is doing modelling that results in trustworthy / usable coverage checking. ESP since for constrained ranges of values where new type won’t play great with supporting pattern matching without some fancy pattern synonyms.

I have seen folks write code that’s like

type Name = String

rather than use a new type, and I think really new type is about having enforced abstraction over the representation of a datatype, to prevent silent corruptions from transparently equivalent representations that have different meanings.

I guess I think it’s good to try to split this sort of opinion piece into a part that’s a forward looking tech challenge along side an exposition that hopefully has clear methodological guidance for today

You say that, on its own, a newtype is nothing more than a name and that names are not type safety, but then you give the example of using newtypes to prevent someone from adding a distance and a duration. I think it's a false distinction to say that the safety there is some kind of safety that isn't type safety.

Yes, on its own, a newtype is nothing more than a name. The safety comes from pairing a newtype with an encapsulation mechanism and a carefully-designed trust boundary.

Without an encapsulation mechanism, I do not consider using newtypes to wrap real numbers with units of measure sufficient to be called “type safety”; in my experience it still requires significant discipline to use properly (because the points of wrapping/unwrapping are usually fairly local and require delicate care).

Of course, this is a matter of both subjective definition and relative situation. One can theoretically imagine a codebase that conventionally uses units-of-measure wrappers so pervasively that the safety is genuine, since the places where values are wrapped/unwrapped are so well-defined that any misuse would stick out as wrong. However, I have never in my life seen such a codebase, so anecdotally I can only consider such measures more like the lines painted on a road to delineate lanes than a bona fide safety mechanism.

So basically, "if you don't use newtype to implement an abstract data type, you don't get any type safety because the on-spot wrapping/unwrapping is still possible".

On one hand, yes. On another, no. I am working right now on a Go codebase with lots of newtypes (well, the Go's equivalent), and they're generally casted to/from underlying primitive types basically in two places: when they're serialized into JSON, and where they're deserialized from JSON. And in several places in the middle of the code where you need an explicit cast, well, the cast is explicit. You actually have to consider it.

Mind you, in Go it's almost impossible to hide the newtype's constructor unless you jump through some rather unintuitive hoops. Is Go fundamentally type-unsafe? I don't think it is, although I sometimes wish some structs were impossible to zero-initialize. Then again, that's generally amended by unexporting the struct and exporting its interface instead.

> Is Go fundamentally type-unsafe?

Interface{} and nil pointers point to yes.

Neither of those is incompatible with Cardelli's definition of type safety. `interface{}` is not `void *`. Null pointer errors are not untrapped.

Cardelli's definitions are extremely odd; if you take them literally then Python is type safe but Java is not.

In everyday language a downcast, even a checked one, is not a type-safe operation, and so to the extent that Go's limited type system makes it impractical to write programs without downcasts I'd say that Go is fundamentally type-unsafe.

Well, it's a matter of taste, I guess. In my opinion any downcast that reliably distinguishes between valid and invalid values is type-safe. The behaviour of

    defer func() {
        if e := recover(); e != nil {
            fmt.Printf("not a string %v\n", e)
        }
    }()
    v := interface{}(5)
    u := v.(string)
    fmt.Println(u)

is well-defined: it will print "not a string", always.

By that logic there's no such thing as a non-type-safe language, because all programs have behaviour.

Normally one would say a checked downcast like that is not type-safe, because you can't reason locally about the type behaviour of the downcast based on knowing the type of v. You would have to know the value of v, which is a Turing-complete problem in the general case.

> Read the article more carefully.

This is unnecessarily rude. Maybe you should have written the article more carefully, or read my comment more carefully.

> newtypes are useful, but only when used in certain ways and in a weaker sense than constructive data modeling

Constructive data modelling can be an easier way to provide certain kinds of guarantees in some circumstances, perhaps. But the claim that newtype-based approaches are not type safety remains false.

Hmm asking to read something more carefully is not rude if the commenter is refuting a point that was never made in the article.

It would suffice to say "that point was not made on the article".

That's unnecessarily cautious. Unfounded criticism rightly deserves a slap on the hand, and "Read the article more carefully" is a very light one.

I think the request is rather justified given your response, which is engaging with a strawman version of the thesis presented in the post. What you wrote about the virtues of newtype was explained quite well in the post itself, but you seem to want to disagree about something. You present another strawman in this reply:

> the claim that newtype-based approaches are not type safety

To use your phrasing, the claim is that newtypes do not in and of themselves provide type safety, but that "newtype-based approaches" can and do provide a weaker form of safety than constructive modeling. Further, it's important to understand what the critical additional steps are in such approaches to achieving that safety and avoid cargo-culting "newtypes make things type-safe", and to understand the ways this safety can be violated.

> What you wrote about the virtues of newtype was explained quite well in the post itself

The post implied that the newtype-based approach was somehow "not type safety" and offered significantly less safety in practice than the constructive model approach. The first of those is definitely false, and based on my own experiences I don't believe the second.

> Further, it's important to understand what the critical additional steps are in such approaches to achieving that safety and avoid cargo-culting "newtypes make things type-safe", and to understand the ways this safety can be violated.

Naively it sounds like that would be important, but I'm not convinced it actually is in practice. My experience is that even a cargo-culty use of newtypes delivers most (maybe even all) of the defect rate benefit, and that these vigorous warnings about newtypes are more likely to reduce real-world safety (because people faced with cases that they can't produce a constructive model for will be encouraged to use an alias, or no type at all, rather than a newtype) than improve it.

Again, you are conflating newtypes per se with approaches using newtype as part of an overall abstraction and interface design including constructor hiding. The post makes this quite clear and the author and others have pointed out this distinction to you multiple times here. Just because you made an inference and argued against it doesn't mean the article was making such an implication.

Your second point is certainly arguable and does represent a substantive disagreement with the post unlike your first comment. I think the post makes a solid case that gratuitous use of newtype absent any abstraction boundary is an anti-pattern that provides little benefit if conversions are done ad hoc. Sprinkling on some newtype can certainly help some cases, but the post encourages critical thinking about these issues and explores where this reasoning falls down. If your claim is that critical thinking gets in the way of cargo-culting approaches that lead to "nominal" type safety then you would be right. Your last parenthetical doesn't seem like a reasonable response of someone who has read and understood this post. The post specifically encourages the use of newtype with abstraction boundaries where practical and works through an example.

> Again, you are conflating newtypes per se with approaches using newtype as part of an overall abstraction and interface design including constructor hiding. The post makes this quite clear and the author and others have pointed out this distinction to you multiple times here. Just because you made an inference and argued against it doesn't mean the article was making such an implication.

The author is still carefully avoiding describing any newtype-based approach as "type safety", to the point that they would mislead anyone who wasn't already familiar with the subject.

> Your last parenthetical doesn't seem like a reasonable response of someone who has read and understood this post. The post specifically encourages the use of newtype with abstraction boundaries where practical and works through an example.

It works through an example and follows that with a long list of (IMO exaggerated) weaknesses of that example, which seems more designed to dismiss it. It does not "specifically encourage" using newtypes at all (indeed it says "if you are fond of newtypes" as though one would only ever use newtypes for private emotional reasons). It concludes with "correctness by construction should be preferred whenever practical".

If you'd carefully reread the post you'll see that your first assertion is false. It contains this sentence: "But it is a meaningfully distinct kind of type safety from the one I highlighted a year ago, one that is far weaker." The antecedent of "one" is "type safety", which is being provided, just, weaker, not "not type safety" as you claim.

As for whether the example is being "dismissed" or not, I also think that's manifestly false. See: "[this tradeoff] is often a very good one!" while still diving into exactly what the tradeoff is.

From the article:

"newtypes can provide a sort of safety, just a weaker one. The primary safety benefit of newtypes is derived from abstraction boundaries. If a newtype’s constructor is not exported, it becomes opaque to other modules. The module that defines the newtype—its “home module”—can take advantage of this to create a trust boundary where internal invariants are enforced by restricting clients to a safe API."

From an outside perspective, you seem to be arguing the same things the author has already stated in the article, which is why he's asking you to read the article more carefully.

> "newtypes can provide a sort of safety, just a weaker one. The primary safety benefit of newtypes is derived from abstraction boundaries. If a newtype’s constructor is not exported, it becomes opaque to other modules. The module that defines the newtype—its “home module”—can take advantage of this to create a trust boundary where internal invariants are enforced by restricting clients to a safe API."

The author appears to be claiming that this is somehow distinct from (and qualitatively weaker than) "type safety", without any justification for that claim.

The justification from the article:

"To some readers, these pitfalls may seem obvious, but safety holes of this sort are remarkably common in practice. ... Proper use of this technique demands caution and care:

* All invariants must be made clear to maintainers of the trusted module...

* Every change to the trusted module must be carefully audited to ensure it does not somehow weaken the desired invariants.

* Discipline is needed to resist the temptation to add unsafe trapdoors that allow compromising the invariants if used incorrectly.

* Periodic refactoring may be needed to ensure the trusted surface area remains small...

In contrast, datatypes that are correct by construction suffer none of these problems."

The article lists a few specific pitfalls. I don't think this justifies the claim that "it is a meaningfully distinct kind of type safety": newtype-based approaches may have further pitfalls that ground-up construction approaches do not, but ground-up construction approaches do still have pitfalls.

To get more specific:

* Safety holes of this sort are remarkably uncommon in practice, in my experience.

* Modules should be small and easily understood. If maintaining a module's invariants becomes too complex then you can, and should, recursively apply the same techniques within the module, breaking it up into smaller modules. This is good development practice anyway, as is periodic refactoring. So these cautions are a lot less costly than they sound; in fact the cost may well be zero.

* You need to resist the temptation to add unsafe trapdoors in any other approach as well; this simply isn't a disadvantage that's in any way specific to using newtypes.

> * You need to resist the temptation to add unsafe trapdoors in any other approach as well; this simply isn't a disadvantage that's in any way specific to using newtypes.

In fact, in some cases, it's useful to retain (redundant or invalid) state that's discarded in "correct by construction" data structures. For example, saving application configuration as Option<int> is easier for the application to read correctly (int value, bool present). However when a user is editing an Option<T> through a GUI (checkbox, number) pair, then unchecking the checkbox will set the value to None and discard the last entered value, which is a poor user experience in my view.

This isn’t necessarily so, though. I don’t see why unchecking the checkbox can’t create an Option<T> that is passed (int value, bool false). It just means that you accept this as a valid construction state, and that it must therefore be handled.

I admit that I might be missing something fundamental to this discussion.

I meant to say "saving application configuration as Option<int> (either int value or None) is easier for the application to read correctly then a tuple (int value, bool present)."

For those who may not be familiar with the Haskell ecosystem, Alexis King (lexi-lambda) writes many blogs and libraries related to Haskell.

For example, you may be interested in her recent talk on effect systems in Haskell at ZuriHac 2020,[1] based on the eff library she mainly contributes to.[2]

[1]: https://www.youtube.com/watch?v=0jI-AlWEwYI

[2]: https://github.com/hasura/eff

> he's asking you to read the article more carefully

she

I agree with the OP but for a slightly different reason.

Type safety is valuable in that it relatively easily helps achieve a goal of alerting the programmer that he/she is mixing together things that should have not been mixed. Ie. using something in a context where it should not be used.

That goal can be achieved in other ways and it is not even the best way to achieve that goal.

Type safety is valuable in that:

* does a lot of sense for a user of the programming language (ie. programmer) IF it is done sensibly (forget about template metaprogramming, that is not sensible). Thinking about things in terms of types is natural to our brain structure.

* warns early (ie. your program does not compile)

* enforces on everybody working on the application (you can ignore conventions but you can't ignore compilation error)

Now, what I don't like is that people forget that types and type safety is there to achieve the goal (making programs better, easier to read, easier to reason about, harder to make a mistake).

Thinking about type safety as if it was some kind of security mechanism to prevent any and all kinds of mistakes is IMO very misguided. I don't want to battle with my type system, I want to write working code and I want to use type safety mechanism that lets me get there reasonably without spending huge amount of extra effort.

So, I think, there is a sweet spot for type safety, where it is enough to help prevent most mistakes and make reading the code easier, but not enough to make you reduce your productivity.

Not only that, the sweet spot will depend on what task you are working on.

For example, languages with relaxed type safety are good for rapid development -- ie. "scripts". There sweet spot is shifted to less type safety because your program is much smaller and you don't need help remembering what are different things and there is probably less developers working on it.

On the other hand, for large projects with many people working on them, long build times, expensive testing, etc. you would very likely want a language with stronger typing (like Java that is very poor language but offers very good practical type system).

Now, Rust type safety is a special IMO compared to other type safety mechanism in that it is very hard for the user (ie. programmer) but I still am ok with this. The reason is because there the type safety is used to get so much more that would not otherwise be possible (at least not with our current knowledge).

>> I disagree, and I think this kind of fundamentalism hurts the adoption of type safety.

For what it's worth, I got a similar impression: An excessively narrow (implied) definition of "type safety", based on which newtype wrappers are criticized, while minimizing or denying the benefit of newtypes over type aliases in preventing errors matching arguments to functions. E.g. the `newtype Email = Email String` example someone mentions down-thread, which has clear benefits as soon as there's a function `sendEmail :: Email -> IO ()`. Benefits that I'd argue many people would be happy to see as part of "type safety".

> It's like saying that a non-machine-checkable mathematical proof is not a proof - something few working mathematicians would agree with.

Only because we're not ready for that yet. Given the current technology (Coq, Agda, Mizar etc.), writing a machine-checkable proof is unbelievably tedious. That doesn't mean it wouldn't be welcome; many published papers, even widely accepted ones, have later been found to contain errors. [1] [2]

[1] https://mathoverflow.net/questions/35468/widely-accepted-mat...

[2] https://lamport.azurewebsites.net/tla/proof-statistics.html

> In a well-formed program it is impossible to have a OneToFive that has not passed through toOneToFive.

I think this is the key. In any (type) system, there’s an opportunity to chicanery the compiler. The degree to which you have to treat users of that system like children depends on how likely you think they are to behave badly.

If a “well-formed program” is something you can reasonably expect in your environment, you can also reasonably assume you also received a nominal type because it was validated. If it’s not, the expectation is that someone is lying to the compiler... and then you treat someone like they’re misbehaving. Even if they’re not.

The whole conceit of fancy type systems is that it's generally useful to move as many things as possible from the realm of "humans must verify" to "computers can automatically verify on behalf of humans". Relying on data representations which are richer or more constrained than newtypes, and treating with suspicion promises the computer can't automatically verify, isn't "treating your users like children," it's acknowledging that you and your users are, eventually and probably frequently, going to forget important assumptions and make mistakes.

What I mean is that in a system where you’ve defined a type that requires validation to be assigned safely, and where you’ve provided means to validate untrusted input, functions which don’t handle untrusted input should be able to use those types freely... unless you don’t trust other people assigning types in the system.

In TypeScript we sometimes define nominal types with a technique called “branding”, and it works the same way: validate untrusted input and cast; trust at layers beneath that surface area.

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.

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.

>In a well-formed program it is impossible to have a OneToFive that has not passed through toOneToFive.

It does seem more likely that the program over times becomes less well formed and you end up with a OneToFive that has not passed through toOneToFive than having a good type definition for OneToFive is changed to be less precise and open to abuse.

Note the seems more likely is just in my opinion of course as I have not ever seen any statistics on this kind of degradation of program quality and must thus just rely on my own experience of how these kinds of things go.