Names are not type safety • Hacker News Board

Re: Names are not type safety

#41

Post by quickthrower2 » Mon, Nov 02, 2020, 7:07 AM UTC

The idea of needing a 1-5 compile-time constrained value is rare in any application I have worked with, because either you'd use an enum, or the "5" isn't really known at compile time. (I thought about this when doing some basic Idris lesson.).

It makes me wonder what the constrained type might be that I do need?

A non-negative floating point number would be a common one I think, e.g. for a coordinate. I've not been keeping up with Haskell but can you guarantee this at compile time?

I guess it would be hard to do so, because every assignment to this from a normal floating point would need to be checked, requiring you "prove" that the number is non-negative at compile time, so back to Idris I guess?

E.g. x:Positive, x+5 -> this is now a normal float, or I need to prove x+5:Positive.

I have only haskelled a little bit, but I would think most of the newtypes are mostly to trace the meaning of something. E.g. Latitude, Longitude, X, Y, WeightKg, and so on. These would be hard to constrain (and to what..?) they are just floating points.

Re: Names are not type safety

#42

Post by [deleted] » Mon, Nov 02, 2020, 7:14 AM UTC

lexi-lambda wrote: post #29

platinumrad wrote: post #23

Earlier quoted context omitted.

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

[deleted]

Re: Names are not type safety

#43

Post by codebje » Mon, Nov 02, 2020, 7:14 AM UTC

chongli wrote: post #30

codebje wrote: post #10

Earlier quoted context omitted.

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.

You're combining acceptable structural representations with validated as correct inputs - this is a trap to be careful of.

It's real-world data, which is rarely 100% clean and correct. If you can only represent clean and correct data, you probably can't handle all the data you'll need to.

For an email, a "newtype Email = Text" is, IMO, correct. You can break it down as far as you need though: "data Email = Email (Maybe Name) LocalPart Domain" eg, with the three sub-types being newtypes of text. If you try to go further you'll run into problems that the best definition of "valid" is "works when used."

The situation for URLs is similar.

ZIP codes is an even trickier one - if you can only represent genuine ZIP codes, what happens if you need to represent an address where someone's accidentally transposed two digits and wound up with an unused ZIP code? If you're not US domestic only, what do you do for the four billion or so humans who don't have a structured address at all?

(There's a reason vCard gave up on forcing structured addresses and added a "just whatever this text chunk here says" alternative).

If you want to represent "validated version" data then IMO it's sufficient to use a "data ValidatedEmail = ValidatedEmail Email" with a non-exported constructor and a "validateEmail :: Email -> Maybe ValidatedEmail" function.

If you're, say, the USPS and really must represent valid ZIP codes and only valid ZIP codes, you'll perhaps wind up in the rabbit hole of defining a hierarchical hot mess of sum types. Or pragmatically accept you will risk invalid ZIP codes to avoid needing to do that.

Re: Names are not type safety

#44

Post by codebje » Mon, Nov 02, 2020, 7:15 AM UTC

embwbam wrote: post #37

chongli wrote: post #30

Earlier quoted context omitted.

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.

Practically, I disagree with the GP. A newtype is fine in these cases. You don't have to say you know what to do with negative Lengths if you have a smart constructor that won't let you create one.

Can you subtract lengths as in "let length3 = length1 - length2" ?

Re: Names are not type safety

#45

Post by codebje » Mon, Nov 02, 2020, 7:16 AM UTC

alexmingoia wrote: post #14

codebje wrote: post #10

Earlier quoted context omitted.

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…

Are you suggesting using Proxy to create a type that masks an Int? How would you deal with text that can only contain certain characters for example?

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.

Re: Names are not type safety

#46

Post by CyberRabbi » Mon, Nov 02, 2020, 7:19 AM UTC

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…

Hmm asking to read something more carefully is not rude if the commenter is refuting a point that was never made in the article.

Re: Names are not type safety

#47

Post by copascetic » Mon, Nov 02, 2020, 7:24 AM UTC

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 think the request is rather justified given your response, which is engaging with a strawman version of the thesis presented in the post. What you wrote about the virtues of newtype was explained quite well in the post itself, but you seem to want to disagree about something. You present another strawman in this reply:

> the claim that newtype-based approaches are not type safety

To use your phrasing, the claim is that newtypes do not in and of themselves provide type safety, but that "newtype-based approaches" can and do provide a weaker form of safety than constructive modeling. Further, it's important to understand what the critical additional steps are in such approaches to achieving that safety and avoid cargo-culting "newtypes make things type-safe", and to understand the ways this safety can be violated.

Re: Names are not type safety

#48

Post by bsza » Mon, Nov 02, 2020, 7:35 AM UTC

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…

> It's like saying that a non-machine-checkable mathematical proof is not a proof - something few working mathematicians would agree with.

Only because we're not ready for that yet. Given the current technology (Coq, Agda, Mizar etc.), writing a machine-checkable proof is unbelievably tedious. That doesn't mean it wouldn't be welcome; many published papers, even widely accepted ones, have later been found to contain errors. [1] [2]

[1] https://mathoverflow.net/questions/35468/widely-accepted-mat...

[2] https://lamport.azurewebsites.net/tla/proof-statistics.html

Re: Names are not type safety

#49

Post by kstenerud » Mon, Nov 02, 2020, 7:42 AM UTC

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…

From the article:

"newtypes can provide a sort of safety, just a weaker one. The primary safety benefit of newtypes is derived from abstraction boundaries. If a newtype’s constructor is not exported, it becomes opaque to other modules. The module that defines the newtype—its “home module”—can take advantage of this to create a trust boundary where internal invariants are enforced by restricting clients to a safe API."

From an outside perspective, you seem to be arguing the same things the author has already stated in the article, which is why he's asking you to read the article more carefully.

Re: Names are not type safety

#50

Post by runeks » Mon, Nov 02, 2020, 7:55 AM UTC

quickthrower2 wrote: post #41

The idea of needing a 1-5 compile-time constrained value is rare in any application I have worked with, because either you'd use an enum, or the "5" isn't really known at compile time. (I thought about this when doing some basic Idris lesson.). It makes me wonder what the constrained type might be that I do need? A non-negative floating point number would be a common one I think, e.g. for a coordinate. I've not been…

> The idea of needing a 1-5 compile-time constrained value is rare in any application I have worked with, because either you'd use an enum, or the "5" isn't really known at compile time.

The OneToFive-type is used to illustrate a point, not because it’s practically useful.

> A non-negative floating point number would be a common one I think, e.g. for a coordinate. I've not been keeping up with Haskell but can you guarantee this at compile time?

No. It’s not possible.

But, as you point out, this is not a problem since values like these are rarely known at compile-time.

And, more importantly, if you can’t trust a programmer to write the correct constant, how can you trust the same programmer to write the correct type for this constant (“non-negative float”)?

Except by using a quasi-quoter (which amounts to parsing a string into a float at compile-time)