Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Names are not type safety

lexi-lambda.github.io

Post reply on HN
Print view View original

51–60 of 130 posts

Re: Names are not type safety

#51

Post by bryanrasmussen »

lmm wrote: post #12

I disagree, and I think this kind of fundamentalism hurts the adoption 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. In a well-formed program it is impossible to have a OneToFive that has not passed through toOneToFive. That's type safety by any reasonable definition. It's not as much type safety as you'd gain t…

>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.

Re: Names are not type safety

#52

Post by lmm »

kstenerud wrote: post #49
lmm wrote: post #39

Earlier quoted context omitted.

> 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…

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.…

> "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.

Re: Names are not type safety

#53

Post by one-punch »

kstenerud wrote: post #49
lmm wrote: post #39

Earlier quoted context omitted.

> 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…

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.…

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

Re: Names are not type safety

#54

Post by quietbritishjim »

CyberRabbi wrote: post #46
lmm wrote: post #39

Earlier quoted context omitted.

> 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…

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".

Re: Names are not type safety

#55

Post by one-punch »

lmm wrote: post #52
kstenerud wrote: post #49

Earlier quoted context omitted.

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.…

> "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 app…

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."

Re: Names are not type safety

#56

Post by lmm »

copascetic wrote: post #47
lmm wrote: post #39

Earlier quoted context omitted.

> 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…

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…

> 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.

Re: Names are not type safety

#57

Post by lmm »

one-punch wrote: post #55
lmm wrote: post #52

Earlier quoted context omitted.

> "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 app…

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. * Discipl…

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.

Re: Names are not type safety

#58

Post by copascetic »

lmm wrote: post #56
copascetic wrote: post #47

Earlier quoted context omitted.

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…

> 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 addit…

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.

Re: Names are not type safety

#59

Post by alexmingoia »

codebje wrote: post #45
alexmingoia wrote: post #14

Earlier quoted context omitted.

Are you suggesting using Proxy to create a type that masks an Int? How would you deal with text that can only contain certain characters for example?

In the Length case I'm more suggesting to use an unsigned integer type than any more complex type system trickery to specifically limit the range. There are type systems that let you declare a new type to be a sub-range of an existing type, but Haskell's is not one of them.

Dependent types don't provide any safety over smart constructors for parsing, which is the most common use case for types with restricted values. Validating user input, parsing emails or URLs, etc. all must deal with an invalid case at runtime, and dependent types are of no use there.

Re: Names are not type safety

#60

Post by runeks »

It should be noted that the -- to use the terminology of the article -- extrinsically safe example module Data.List.NonEmpty.Newtype can be converted into an intrinsically safe one by changing the definition of the NonEmpty type from

    newtype NonEmpty a = NonEmpty [a]
to:

    newtype NonEmpty a = NonEmpty (a, [a])
(and changing the associated functions accordingly -- which can now be implemented without the use of error).

EDIT: Upon further thought, I'm not sure the above distinction makes sense. The implementation of e.g. Data.List.NonEmpty.Newtype.head would still involve the use of "error" through the use of Data.List.head:

    head :: NonEmpty a -> a
    head (NonEmpty (x, []))  = x
    head (NonEmpty (_, lst)) = Data.List.head lst
Post reply on HN