Names are not type safety • Hacker News Board

Re: Names are not type safety

#121

Post by nyanpasu64 » Mon, Nov 02, 2020, 9:04 PM UTC

IggleSniggle wrote: post #111

nyanpasu64 wrote: post #71

Earlier quoted context omitted.

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

I meant to say "saving application configuration as Option (either int value or None) is easier for the application to read correctly then a tuple (int value, bool present)."

Re: Names are not type safety

#122

Post by codygman » Mon, Nov 02, 2020, 10:28 PM UTC

Joker_vD wrote: post #89

lexi-lambda wrote: post #29

Earlier quoted context omitted.

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…

So basically, "if you don't use newtype to implement an abstract data type, you don't get any type safety because the on-spot wrapping/unwrapping is still possible". On one hand, yes. On another, no. I am working right now on a Go codebase with lots of newtypes (well, the Go's equivalent), and they're generally casted to/from underlying primitive types basically in two places: when they're serialized into JSON, and w…

> Is Go fundamentally type-unsafe?

Interface{} and nil pointers point to yes.

Re: Names are not type safety

#123

Post by lexi-lambda » Mon, Nov 02, 2020, 10:38 PM UTC

steveklabnik wrote: post #119

chrisoverzero wrote: post #114

Earlier quoted context omitted.

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.

In Haskell, a newtype can be a single-field record with a named field, so from a Haskell perspective, I would definitely consider both of them “newtypes.”

Re: Names are not type safety

#124

Post by codebje » Mon, Nov 02, 2020, 11:57 PM UTC

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.

When I say range types I mean a type like '5..23' - a sub-range of some other type. Haskell doesn't have these. Most languages don't - one example that does is Ada:

https://en.wikibooks.org/wiki/Ada_Programming/Types/range

As you can see from that link, it's bounds checked at runtime. You could have a modulo type that wraps on overflow, which is of course what most numeric types are in most programming languages, including Haskell, but the modulus is fixed at some power of two for obvious reasons.

There's only one thing I truly value out of a good type (or static analysis) system, and that's enabling fearless refactoring. I want the type system to pick up on any downstream consequences of a change I make rather than finding out by phone call at 3am the day after a deploy that some edge case got overlooked.

Dependent types can (in theory) give that over smart constructors. If my parser should leave me with, say, a sorted vector, or an assertion that if one field is some value then some other field is Just something, then I'd like to be able to rely on those facts in downstream code making use of the results of the parser. If it's just a smart constructor as we usually write them a later refactor (sorting on a different key, for example) doesn't change anything that any other bit of code can be verified against.

A dependent type carrying a proof that a vector is sorted based on some criteria and an assertion about the existed of some value can be verified at compile time.

I'm not sure what the status is of dependent types for Haskell. You could do similar propositional assertions now with Ghosts of Departed Proofs, and LiquidHaskell exists for these sorts of assertions, so dependent types aren't the only path to this kind of static safety, either. I won't claim that this is practical - though I would be surprised if it's not practical to do in small doses.

Nevertheless, I would still just be reaching for smart constructors in current day Haskell.

Re: Names are not type safety

#125

Post by platinumrad » Tue, Nov 03, 2020, 12:46 AM UTC

codygman wrote: post #122

Joker_vD wrote: post #89

Earlier quoted context omitted.

So basically, "if you don't use newtype to implement an abstract data type, you don't get any type safety because the on-spot wrapping/unwrapping is still possible". On one hand, yes. On another, no. I am working right now on a Go codebase with lots of newtypes (well, the Go's equivalent), and they're generally casted to/from underlying primitive types basically in two places: when they're serialized into JSON, and w…

> Is Go fundamentally type-unsafe? Interface{} and nil pointers point to yes.

Neither of those is incompatible with Cardelli's definition of type safety. `interface{}` is not `void *`. Null pointer errors are not untrapped.

Re: Names are not type safety

#126

Post by ronlobo » Tue, Nov 03, 2020, 3:24 AM UTC

Very interesting read, thanks for putting that together.

I am wondering how these ideas relate to "value objects", a term formed many years ago via domain driven design.

Re: Names are not type safety

#127

Post by lmm » Tue, Nov 03, 2020, 12:22 PM UTC

nimih wrote: post #115

eyelidlessness wrote: post #105

Earlier quoted context omitted.

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

So I think that's true as far as it goes, but vastly overstates how much difference fully constructive types actually make. Starting to use types, even nominal ones, to express your requirements is a real game changer, a step change in your defect rate: it turns making a correct program from an intractable global problem into a compositional problem that you can reason about locally. Using constructive types is a technique that eliminates a couple of rare classes of errors. It's fine, and if you can do it cheaply (which is pretty rare in practice IME) then it's worth doing, but it's really not a major difference-maker. And I think a post like this could easily give the impression that newtypes aren't all that, so to speak, when nothing could be further from the truth.

Re: Names are not type safety

#128

Post by lmm » Wed, Nov 04, 2020, 12:33 AM UTC

platinumrad wrote: post #125

codygman wrote: post #122

Earlier quoted context omitted.

> Is Go fundamentally type-unsafe? Interface{} and nil pointers point to yes.

Neither of those is incompatible with Cardelli's definition of type safety. `interface{}` is not `void *`. Null pointer errors are not untrapped.

Cardelli's definitions are extremely odd; if you take them literally then Python is type safe but Java is not.

In everyday language a downcast, even a checked one, is not a type-safe operation, and so to the extent that Go's limited type system makes it impractical to write programs without downcasts I'd say that Go is fundamentally type-unsafe.

Re: Names are not type safety

#129

Post by Joker_vD » Thu, Nov 05, 2020, 2:44 PM UTC

lmm wrote: post #128

platinumrad wrote: post #125

Earlier quoted context omitted.

Neither of those is incompatible with Cardelli's definition of type safety. `interface{}` is not `void *`. Null pointer errors are not untrapped.

Cardelli's definitions are extremely odd; if you take them literally then Python is type safe but Java is not. In everyday language a downcast, even a checked one, is not a type-safe operation, and so to the extent that Go's limited type system makes it impractical to write programs without downcasts I'd say that Go is fundamentally type-unsafe.

Well, it's a matter of taste, I guess. In my opinion any downcast that reliably distinguishes between valid and invalid values is type-safe. The behaviour of

    defer func() {
        if e := recover(); e != nil {
            fmt.Printf("not a string %v\n", e)
        }
    }()
    v := interface{}(5)
    u := v.(string)
    fmt.Println(u)

is well-defined: it will print "not a string", always.

Re: Names are not type safety

#130

Post by lmm » Fri, Nov 06, 2020, 7:37 AM UTC

Joker_vD wrote: post #129

lmm wrote: post #128

Earlier quoted context omitted.

Cardelli's definitions are extremely odd; if you take them literally then Python is type safe but Java is not. In everyday language a downcast, even a checked one, is not a type-safe operation, and so to the extent that Go's limited type system makes it impractical to write programs without downcasts I'd say that Go is fundamentally type-unsafe.

Well, it's a matter of taste, I guess. In my opinion any downcast that reliably distinguishes between valid and invalid values is type-safe. The behaviour of defer func() { if e := recover(); e != nil { fmt.Printf("not a string %v\n", e) } }() v := interface{}(5) u := v.(string) fmt.Println(u) is well-defined: it will print "not a string", always.

By that logic there's no such thing as a non-type-safe language, because all programs have behaviour.

Normally one would say a checked downcast like that is not type-safe, because you can't reason locally about the type behaviour of the downcast based on knowing the type of v. You would have to know the value of v, which is a Turing-complete problem in the general case.