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

71–80 of 130 posts

Re: Names are not type safety

#71

Post by nyanpasu64 »

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

Earlier quoted context omitted.

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

> * 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 is easier for the application to read correctly (int value, bool present). However when a user is editing an Option 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.

Re: Names are not type safety

#72

Post by ChrisSD »

the_mitsuhiko wrote: post #69
ChrisSD wrote: post #65

Earlier quoted context omitted.

Why not? That would seem useful if other code depends on having a validated email address.

I point you to the article.

The article doesn't exactly make a case against it. It even explicitly says it's useful! It just says making a newtype isn't as strong a guarantee as a proper type.

Newtypes do work to assert certain checks have already been done and need not be repeated.

Re: Names are not type safety

#73

Post by nyanpasu64 »

tbroadley wrote: post #4
seanwilson wrote: post #2

> Newtypes are useful when carefully applied, but their safety is not intrinsic, no more than the safety of a traffic cone is somehow contained within the plastic it’s made of. What matters is being placed in the right context—without that, newtypes are just a labeling scheme, a way of giving something a name. What's a better alternative though? I like this approach for tagging e.g. user input that has been checked t…

Applying the author's "parse, don't validate" concept, I think you'd parse the user input into a "safe HTML" type with a definition that excluded the language features that enabled those attacks. It might not be worth writing such code for a single project, but I could get behind a library that did that.

Does "parse, don't validate" apply regardless if the resulting type is a newtype or constrained by construction?

Re: Names are not type safety

#74

Post by lmilcin »

lmm wrote: post #39
lexi-lambda wrote: post #18

Earlier quoted context omitted.

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…

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

Re: Names are not type safety

#75

Post by runeks »

the_mitsuhiko wrote: post #64
aliceryhl wrote: post #63

The Rust standard library has many examples of exactly this, except with unsafe to assert that the unreachable cases can't happen. A classic example is the String type, which is just a newtype around Vec . Other examples include CStr, NonZeroUsize and PathBuf. Arguably even File is an example of this. Internally, it's just an integer for the file descriptor.

> has many examples of exactly this Exactly what? I'm not sure what you're referring to here exactly. Generally newtypes in Rust are not used excessively and largely for sensible safety assertions. I don't see people making `EmailAddress(String)` newtypes.

> Exactly what? I'm not sure what you're referring to here exactly.

"Newtypes as tokens"

Re: Names are not type safety

#76

Post by ImprobableTruth »

runeks wrote: post #60

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

Why would you use Data.List.head rather than just matching on lst?

Re: Names are not type safety

#77

Post by lmm »

copascetic wrote: post #58
lmm wrote: post #56

Earlier quoted context omitted.

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

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

Re: Names are not type safety

#78

Post by ImprobableTruth »

one-punch wrote: post #66
lexi-lambda wrote: post #32

Earlier quoted context omitted.

As was already mentioned in another reply, what you are describing are refinement types . A refinement type system actually exists for Haskell: it’s called LiquidHaskell,[1] and though I have not used it for anything serious, it seems to work well for certain kinds of problems. The main challenge of refinement types is that arbitrary properties are very difficult to check in general. (If that weren’t the case, softwa…

> arbitrary properties are very difficult to check in general. To add to this: In theory, it is not just difficult, but impossible . Imagine that the refinement predicate is whether the String/Text encode a (non-)halting Turing machine/Haskell program. Checking it would solve the halting problem. And this predicate is the proof of Rice theorem.[1] (Granted, this may require some sufficiently powerful logic such as fi…

>In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types.

Could you elaborate on that? Unless you're just saying that formalizing reasonably intuitive properties is difficult in general, I don't see what you mean.

Re: Names are not type safety

#79

Post by ImprobableTruth »

one-punch wrote: post #68
ImprobableTruth wrote: post #62

Earlier quoted context omitted.

>The main challenge of refinement types is that arbitrary properties are very difficult to check in general. While this is true, I'm not sure how constructive types don't face the very same issue. Ultimately, you will have to provide evidence for the required properties, with constructive types the proof is just (more or less) implicitly embedded into the datatype, which imo just makes dealing with these properties h…

> While this is true, I'm not sure how constructive types don't face the very same issue. Not sure if the author claims that constructive types do not face this issue. On constructive types vs refinement types, there is a recent Reddit discussion on this topic,[1] prompted by Facebook’s use of Dependent Haskell to eliminate bugs.[2] [1]: https://www.reddit.com/r/haskell/comments/jh7575/eliminating... [2]: https://www…

>Not sure if the author claims that constructive types do not face this issue.

This might be true, but when they were making the case for constructive types they didn't mention it.

>On constructive types vs refinement types, there is a recent Reddit discussion on this topic

The discussions seems to be mostly dependent types vs refinement types, which I'd argue is a false dichotomy. I'd say that dependent types is a what makes refinement types actually powerful in the first place. It's also how most Coq specifications are written.

Re: Names are not type safety

#80

Post by runeks »

ImprobableTruth wrote: post #76
runeks wrote: post #60

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

Why would you use Data.List.head rather than just matching on lst?

I realized the example doesn't make sense for head, since head should always just return the first item of the tuple.

I still think it would make sense to define e.g. last using Data.List.last:

    last :: NonEmpty a -> a
    last (NonEmpty (a, [])) = a
    last (NonEmpty (_, lst)) = Data.List.last lst
which is safe even though Data.List.last contains error.
Post reply on HN