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

111–120 of 130 posts

Re: Names are not type safety

#111

Post by IggleSniggle »

nyanpasu64 wrote: post #71
lmm wrote: post #57

Earlier quoted context omitted.

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

This isn’t necessarily so, though. I don’t see why unchecking the checkbox can’t create an Option 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.

Re: Names are not type safety

#112

Post by remexre »

alexmingoia wrote: post #59
codebje wrote: post #45

Earlier quoted context omitted.

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.

What dependent types would protect you against would be the parser itself returning data. I think it'd be quite difficult to do this for the case of an email or URL, but for cases like "length values must be non-negative," a parser/validator with a type like

    parseLength :: JSON -> Either Error (Sigma (l : Length). lengthToDouble l >= 0.0)
is reasonable, and I'm sure somewhere in the literature there's an indexed monad or something for building parsers/validators out of these, that keeps track of the properties while combining parsers like these.

Re: Names are not type safety

#113

Post by remexre »

alexmingoia wrote: post #8
shawnz wrote: post #7

Earlier quoted context omitted.

The article gives some examples why smart constructors don't fully solve the problem in the section "Newtypes as tokens"

Yeah, I don’t find those points very convincing. Obviously if you export other ways to construct the type, it doesn’t work... It’s like saying “if you forget to sanitize input it won’t get sanitized.” Okay?

I've gotten bit by the Generic one in real code before... I'm sure if I used Haskell for RESTful web stuff more, I'd eventually get bit by something similar for Aeson too.

Re: Names are not type safety

#114

Post by chrisoverzero »

steveklabnik wrote: post #107
chrisoverzero wrote: post #103

Earlier quoted context omitted.

> The String type _is_ a newtype that […] It is not. `NonZeroUsize` is (though in Rust "newtype" is only a pattern or idiom), and its definition (inside of a macro which provides numeric newtypes a bunch of `impl`s) is: pub struct NonZeroUsize(usize); But here's String: pub struct String { vec: Vec , } …which is a normal `struct` _containing_ a named `Vec `. Of the types you mentioned, only `NonZeroUsize` conforms to…

Do you feel that just because the inner value is named, rather than unnamed, it’s no longer a new type? Trying to figure out what line is crossed here.

I'm going by the Rust documentation: https://doc.rust-lang.org/stable/rust-by-example/generics/ne...

(I was going to be cheeky here, but Git history shows you didn't write any of this part.)

Re: Names are not type safety

#115

Post by nimih »

eyelidlessness wrote: post #105
nimih wrote: post #40

Earlier quoted context omitted.

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

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

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.

Re: Names are not type safety

#116

Post by one-punch »

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

Earlier quoted context omitted.

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

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

Agree.

> The discussions seems to be mostly dependent types vs refinement types, which I'd argue is a false dichotomy.

You are right, I think I confused two notions:

1. constructive vs non-constructive reasoning.

2. intrinsic vs extrinsic types (aka Church vs Curry types[ 1]).

In general, intrinsic types are constructive (because Program-is-Proof due to Brouwer–Heyting–Kolmogorov and Curry–Howard and others).

But extrinsic types could also be constructive, esp. when the external static analyzer has access to the program, such as in refinement reflection [2] (as pointed out in the above Reddit comment thread).

[1]: https://lispcast.com/church-vs-curry-types/

[2]: https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18...

Then I think the author is arguing for constructive proofs, which come naturally with intrinsic types, or at least with extrinsic analyzers accessing program structures; and arguing against non-constructive (extrinsic) types, or anything detached from implementation.

Re: Names are not type safety

#117

Post by MaxBarraclough »

sparsely wrote: post #82

I believe that Ada, or perhaps a specific subset with some extensions, achieves most of these goals. You can definitely restrict types to be a range or enumeration of e.g. ints, and they have some facility for contract based function interfaces.

Yes, this is a feature of standard Ada.

https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Na...

Re: Names are not type safety

#118

Post by kbr »

kylereeve wrote: post #106
kbr wrote: post #26

Earlier quoted context omitted.

I think you might be describing refinement type systems [1]? [1] https://en.wikipedia.org/wiki/Refinement_type

I've been reading about that, can't seem to wrap my head around the difference between refinement and dependent types.

I think dependent types are stronger than refinement types because they can encode types that don't necessarily have to be decidable. Refinement types are used for creating subsets of a type, while dependent types can be used for creating arbitrary types based on values. As a result, dependent types are more powerful, but they might be too much if all you need are some constraints on an existing type.

Re: Names are not type safety

#119

Post by steveklabnik »

chrisoverzero wrote: post #114
steveklabnik wrote: post #107

Earlier quoted context omitted.

Do you feel that just because the inner value is named, rather than unnamed, it’s no longer a new type? Trying to figure out what line is crossed here.

I'm going by the Rust documentation: https://doc.rust-lang.org/stable/rust-by-example/generics/ne... (I was going to be cheeky here, but Git history shows you didn't write any of this part.)

Hehe yeah, I mean, I am not 100% sure myself, which is why I asked.

There's no real difference between a 1-tuple struct and the regular struct, other than the name. So to me, it feels like either are both newtypes. But, I guess I could see some sort of argument the other way too.

Re: Names are not type safety

#120

Post by nyanpasu64 »

tbroadley wrote: post #95
nyanpasu64 wrote: post #73

Earlier quoted context omitted.

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

I'm not sure I see how "parse, don't validate" would apply when using a newtype—would you mind explaining further? I think the main point of this article is that newtypes aren't an application of "parse, don't validate". If you validate that user input doesn't contain XSS, then wrap it in a `SafeHtml` newtype, that's validation, not parsing. The article outlines ways that you could wrap the user input but forget to v…

Returning an Option is closer to "parsing" than returning a bool.
Post reply on HN