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

21–30 of 130 posts

Re: Names are not type safety

#21

Post by carterschonwald »

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…

Definitely agree the best approach is doing modelling that results in trustworthy / usable coverage checking. ESP since for constrained ranges of values where new type won’t play great with supporting pattern matching without some fancy pattern synonyms.

I have seen folks write code that’s like

type Name = String

rather than use a new type, and I think really new type is about having enforced abstraction over the representation of a datatype, to prevent silent corruptions from transparently equivalent representations that have different meanings.

I guess I think it’s good to try to split this sort of opinion piece into a part that’s a forward looking tech challenge along side an exposition that hopefully has clear methodological guidance for today

Re: Names are not type safety

#23

Post by platinumrad »

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…

You say that, on its own, a newtype is nothing more than a name and that names are not type safety, but then you give the example of using newtypes to prevent someone from adding a distance and a duration. I think it's a false distinction to say that the safety there is some kind of safety that isn't type safety.

Re: Names are not type safety

#24

Post by p1necone »

skybrian wrote: post #11
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…

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?

Re: Names are not type safety

#25

Post by _28jh »

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 types) but there is nothing you can do to actually put this into the type system. In some assertion based system, you would write something like: `type Norm3 = Vec3 v given(len(v) == 1)`. You could cast a Vec3 to a Norm3 which would run the assertion at run time, or you could write a function like `normalize` which always returns a Norm3 (maybe even it comes with its own assertion that len(v) != 0). Then you can safely pass your Norm3s to functions that expect normalized vectors. It's always recommended to make bad states unrepresentable, but it's weird how no language has ever given you a system like this.

Re: Names are not type safety

#26

Post by kbr »

_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

Re: Names are not type safety

#27

Post by seanwilson »

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

Sounds like you're describing dependent types. You've now got the problem that showing your program is correct involves writing maths proofs that show your properties hold in all cases (which is an undecidable problem).

Re: Names are not type safety

#28

Post by [deleted] »

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

[deleted]

Re: Names are not type safety

#29

Post by lexi-lambda »

platinumrad wrote: post #23
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…

You say that, on its own, a newtype is nothing more than a name and that names are not type safety, but then you give the example of using newtypes to prevent someone from adding a distance and a duration. I think it's a false distinction to say that the safety there is some kind of safety that isn't type safety.

Yes, on its own, a newtype is nothing more than a name. The safety comes from pairing a newtype with an encapsulation mechanism and a carefully-designed trust boundary.

Without an encapsulation mechanism, I do not consider using newtypes to wrap real numbers with units of measure sufficient to be called “type safety”; in my experience it still requires significant discipline to use properly (because the points of wrapping/unwrapping are usually fairly local and require delicate care).

Of course, this is a matter of both subjective definition and relative situation. One can theoretically imagine a codebase that conventionally uses units-of-measure wrappers so pervasively that the safety is genuine, since the places where values are wrapped/unwrapped are so well-defined that any misuse would stick out as wrong. However, I have never in my life seen such a codebase, so anecdotally I can only consider such measures more like the lines painted on a road to delineate lanes than a bona fide safety mechanism.

Re: Names are not type safety

#30

Post by chongli »

codebje wrote: post #10
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…

In Haskell, you would use an algebraic data type that can only hold legal values. You would typically only use a newtype when you're just giving a new name to the same type. Having a Magnitude newtype over Int doesn't change the range of permissible values but does prevent using a Length where a Magnitude was expected, for example. In all typed languages you'll eventually see a function with multiple arguments of the…

How do you write a data type which can only hold legal email addresses? Or URLs? ZIP codes? Or even dates and times? Expressing all of the requirements of these real-world data formats, within a type system such as Haskell's, seems like an extremely daunting task to me. I have programmed in Haskell a fair bit in the past and I have no idea where I'd begin with those.
Post reply on HN