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

101–110 of 130 posts

Re: Names are not type safety

#101

Post by pwm »

sillysaurusx wrote: post #13

(The following comment may not have anything to do with Haskell’s use of the word “name,” but I’ve wondered about this for a long time.) Forcing someone to write iFoo instead of foo isn’t type safety, but it’s a certain kind of safety that I haven’t seen clearly spelled out. Actually I recall Joel on Software mentioning it once. I don’t like it, but it’s always seemed interesting. Another example is in lisp: *current…

> Forcing someone to write iFoo instead of foo isn’t type safety, but it’s a certain kind of safety

The term I'd use (at least from the top of my head) is hygiene. The article uses the word safety in a restrictive sense, ie. preventing errors. Forcing iFoo instead of foo, to me, is more about hygiene where one could still potentially make an (accidental or deliberate) error but that would go against said hygiene. Maybe another way to put it is that safety prevent misuse while hygiene guides correct use. Or another is that with safety the letter and spirit of the law are one and the same while with hygiene it's not.

Haskell's `newtype` is an amazing tool for (proactive) hygiene and, as the article says, a limited tool for safety. By proactive hygiene I mean that if you have:

  bmi :: Float -> Float -> Float
Looking at it you don't know what those params are. They are all just `Float`s. There's not vocabulary to them. Meanwhile here:

  newtype Height = MkHeight Float
  newtype Weight = MkWeight Float

  bmi :: -> Height -> Weight -> Float
It is both clear what they are as well as the compiler will prevent you from passing `Weight` as the 1st param. Now it's not safety as you can still wrap the wrong `Float` as `Height` but that would go against the hygiene.

Re: Names are not type safety

#102

Post by PhineasRex »

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…

So in the example where you're constructing HTML, you would never use strings to represent your HTML. So your template might look something like ``` P(Text(someUserText), I(someItalicized)) ```

This is essentially how React.js works; you don't need to tag strings as safe or unsafe because strings are never treated as HTML, only constructed HTML values (via JSX) are treated as HTML.

Re: Names are not type safety

#103

Post by chrisoverzero »

aliceryhl wrote: post #98
the_mitsuhiko wrote: post #64

Earlier quoted context omitted.

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

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

Re: Names are not type safety

#104

Post by rstarast »

lexi-lambda wrote: post #18
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…

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…

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

Re: Names are not type safety

#105

Post by eyelidlessness »

nimih wrote: post #40
eyelidlessness wrote: post #16

Earlier quoted context omitted.

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

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 works the same way: validate untrusted input and cast; trust at layers beneath that surface area.

Re: Names are not type safety

#106

Post by kylereeve »

kbr wrote: post #26
_28jh wrote: post #25

I've been thinking for a while about something like an "assertion based type system." Rather than types being variants of other types, types can be described as other types + restrictions. Functions take variables with types but also come with a list of assertions. For example, it is sometimes useful in graphics to differentiate, in the type system, a 3D vector and a normalized vector (e.g. separate Vec3 and Norm3 ty…

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.

Re: Names are not type safety

#107

Post by steveklabnik »

chrisoverzero wrote: post #103
aliceryhl wrote: post #98

Earlier quoted context omitted.

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.

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

Re: Names are not type safety

#108

Post by skybrian »

p1necone wrote: post #24
skybrian wrote: post #11

Earlier quoted context omitted.

It seems to me that there is no practical alternative. The impractical alternative is to extend the language so that its type system implements the feature you want. (For example, adding bounded integers.) I don't see how that helps, though, because there could be bugs in your language extension, and it has to be maintained. It's just going about it the hard way. It would be sort of like avoiding "unsafe" in Rust by…

There's a lot to be gained by isolating the place where the validation needs to be done, and the source of the bugs could be to one place though. Would you rather have one bit of code that checks 1<=X<=5, or 100 call sites all doing the same thing slightly differently?

There ways to do that without type system level hacking.

Re: Names are not type safety

#109

Post by hwayne »

ImprobableTruth wrote: post #62
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…

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

> is supposed to mean exactly. If your predicate makes some data invalid, it's just not representable in the refined type.

Author here. It's representable; the type checker has to prove it never happens in practice. This requires very different techniques from typechecking constructive types. Liquid Haskell shells out to Z3, which can return "unknown" as an answer in addition to "sat" or "unsat".

(There's actually a fourth option, which is that Z3 runs forever, but I think LH does a bunch of clever design to avoid that case.)

You can also `assume` that refinements are satisfied without proving them, in which case they can be violated at runtime. This would be impossible if the invalid data was unrepresentable.

Other approaches to refinement types, such as the original ML paper [0], implemented them constructively and didn't have this problem.

[0]: https://www.cs.cmu.edu/~fp/papers/pldi91.pdf

Re: Names are not type safety

#110

Post by aliceryhl »

chrisoverzero wrote: post #103
aliceryhl wrote: post #98

Earlier quoted context omitted.

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.

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

The point of a newtype is that it allows you to create a wrapper around some other type for one of the following two purposes:

1. Marking the kind of data to prevent mixing up values of different kinds. (e.g. Email)

2. Outlawing some of the values of the underlying type. (e.g. OneToFive)

I do not think it being a tuple-struct or not is important at all when deciding whether something uses the newtype pattern, as long as it has a single field.

Post reply on HN