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

91–100 of 130 posts

Re: Names are not type safety

#91

Post by piaste »

mcv wrote: post #61

I don't know much about Haskell, but I was struck by this: > "Suppose we want a type for “an integer between 1 and 5, inclusive.” The natural constructive modeling would be an enumeration with five cases" Does that really make sense? Using an enum for a limited integer type? I realise most languages don't actually support true limited integer types, but if I recall correctly from my introductory programming classes 2…

Range types in the Pascal family, unless I'm mistaken, are not checked for legitimate values at compile time - they just crash at runtime if you try to create one with an invalid value. Syntactic sugar for an assert statement in the constructor. It's usually quick and straightforward to replicate the feature in a modern language with generics and first-class functions.

When people refer to 'type safety', they almost always mean compile-time safety. Not just ensuring that a value of 6 cannot exists, but ensuring that none of your code is trying to create one. The unwieldy enumeration allows that.

Re: Names are not type safety

#92

Post by devit »

The real issue is the lack of dependent types in Haskell (and unfortunately Rust and all languages with a vast ecosystem).

With dependent types, you can just include a type-level proof that x A newtype including such a dependently-typed proof is the correct solution to this problem, since it can be generalized to any range, unlike the enum with 5 variants.

Re: Names are not type safety

#93

Post by rowanG077 »

devit wrote: post #92

The real issue is the lack of dependent types in Haskell (and unfortunately Rust and all languages with a vast ecosystem). With dependent types, you can just include a type-level proof that x A newtype including such a dependently-typed proof is the correct solution to this problem, since it can be generalized to any range, unlike the enum with 5 variants.

It's possible to do this in haskell but it's quite clunky.

Re: Names are not type safety

#94

Post by runeks »

ImprobableTruth wrote: post #88
runeks wrote: post #80

Earlier quoted context omitted.

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 .

You can avoid the error of Data.List.last by 'inlining' it (just like you could in your first example) last :: NonEmpty a -> a last (NonEmpty (a, [])) = a last (NonEmpty (a, x:[])) = x last (NonEmpty (a, x:xs)) = last (NonEmpty (a, xs))

I see your point. But I’d argue that you avoid it in both cases, since without inlining the error-call is unreachable anyway.

Re: Names are not type safety

#95

Post by tbroadley »

nyanpasu64 wrote: post #73
tbroadley wrote: post #4

Earlier quoted context omitted.

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?

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

By contrast, suppose you have a type like `type SafeHtml = TextNode Text | DivNode SafeHtml | ...`. You parse the user input into a value of this type. If the parse fails, it's because the user input contained something unsafe. The article contends that it's harder to accidentally wrap an unsafe string, since you have to parse a safe HTML string to get a value of type `SafeHtml`.

(Although I'm not sure I buy that last point. With both methods you'd want to keep the `SafeHtml` type's constructors in a module and not export them. Otherwise you could wrap arbitrary text in the newtype or in the `TextNode` constructor. Both seem equally possible to me.)

Re: Names are not type safety

#96

Post by benibela »

0xFluegel wrote: post #84
benibela wrote: post #81

In Pascal you can easily create such a type OneToFive = 1..5 It should inherit all the normal arithmetic, but does not allow values outside the range However, these kind of types are causing a lot of problems. You do arithmetic on them, get a value outside of the range, and then it throws an exception. And an unhandled exception crashes the program, which is often worse than an invalid value. And it is slow when it h…

> And an unhandled exception crashes the program, which is often worse than an invalid value. Please elaborate. Why is working with garbage better than not working at all? Would it not also rather make it easier to find these out-of-range cases with fuzzing?

It is better in GUI applications.

You have 1% of code dealing with user data, and 99% of code doing other things

For example, a text editor. If it crashes, you lose all your text since the last save, which is very bad. But the editor also does other things like playing animations when you click somewhere, a lowering button, or a show a rotating hourglass as mouse cursor. If it would show a wrong animation, that is completely irrelevant. Or it has syntax highlighting with a range type for possible user-defined colors. If it shows the wrong color, that is no big deal. But if you have a new version of the editor, adding more colors, and you use those colors in the user's setting, you cannot downgrade to an older version, because it would crash when it does not know the new colors.

I just had an actual problem with such an exception when calling GetFileAttributes. It returns INVALID_FILE_ATTRIBUTES (unsigned 0xFFFFFFFF) on failure. But I was calling a wrapper around it, which casts it to a signed value and then return -1. Storing the return value in an unsigned variable and then comparing it to 0xFFFFFFFF gave me a range check error. But compiled with range checking disabled, it works perfectly fine.

Re: Names are not type safety

#98

Post by aliceryhl »

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.

Of newtypes. I gave several examples of them. The String type _is_ a newtype that outlaws some of the possible values of the underlying type, namely non-utf8 byte sequences. I wasn't talking about people using Rust, but about the standard library.

That said, I have personally used newtypes a reasonable amount, mostly for making sure I don't mess up different kinds of database ids.

Re: Names are not type safety

#99

Post by chriswarbo »

Thinking about safety and security can benefit from a threat model: what sort of things do we expect to happen, and are we trying to prevent?

I think of safe handling of user input as "first order safety". Server-side code handling arbitrary input from the network should use an adversarial model: assume that users will exploit any weakness we expose, no matter how convoluted.

Program/library architecture and design is more like "higher order safety": we're not directly preventing attacks, we're preventing code-which-allows-attacks. I don't follow an adversarial approach here: I'm not trying to stop a rogue developer from inserting backdoors into a project, I'm trying to catch and prevent mistakes from being made.

If there's a correct-by-construction way to approach certain problems then I'll gladly use it (e.g. one of my current projects uses NonEmptyString, NonEmptySet and NonEmptyList, which use a (head, tail) pair to guarantee non-emptiness). If that's not practical, but there is a way to encapsulate problematic code using newtypes and modularity, then I'll take that (e.g. this project has a NoSpace newtype for strings without whitespace). If it's not practical to encapsulate problematic code, then I'd still rather make it obvious when something dodgy is happening, e.g. even if a 'StatusCode' is isomorphic to a String, the minor cost of wrapping it up in a newtype is worth it to prevent obvious mistakes like appending semantically distinct values. It's all about bang-for-buck.

I also agree that type synonyms usually aren't worth it. The extra cost of introducing a newtype isn't much, and it buys us a lot more in terms of ruling out problems, making conversions more explicit, better error messages, etc.

Re: Names are not type safety

#100

Post by wtetzner »

benibela wrote: post #96
0xFluegel wrote: post #84

Earlier quoted context omitted.

> And an unhandled exception crashes the program, which is often worse than an invalid value. Please elaborate. Why is working with garbage better than not working at all? Would it not also rather make it easier to find these out-of-range cases with fuzzing?

It is better in GUI applications. You have 1% of code dealing with user data, and 99% of code doing other things For example, a text editor. If it crashes, you lose all your text since the last save, which is very bad. But the editor also does other things like playing animations when you click somewhere, a lowering button, or a show a rotating hourglass as mouse cursor. If it would show a wrong animation, that is co…

> It is better in GUI applications.

Unless it's in that one percent of code that deals with user data, in which case it might be much better to just crash. Depending on what the GUI application is for, giving incorrect values could be very bad.

I would think you could catch all exceptions at the top level, save a backup of whatever data the user has loaded, and then continue to crash normally.

Post reply on HN