Remix.run Logo
Names are not type safety (2020)(lexi-lambda.github.io)
26 points by azhenley 4 hours ago | 11 comments
b_e_n_t_o_n 4 minutes ago | parent | next [-]

Perhaps it's because I'm not a haskeller but I'm not sure if I'm sold on encoding this into the type system. In go (and other languages for example), you would simply use a struct with a hidden Int, and receiver methods for construction/modification/access. I'm not sure I see the benefit of the type ceremony around it.

5pl1n73r 2 hours ago | parent | prev | next [-]

My peers and I work on a language centered around "constructive data modeling" (first time I hear it called that). We implement integers, and indeed, things like non empty lists using algebraic data types, for example. You can both have a theory of values that doesn't rely on trapdoors like "int32" or "string", as well as encode invariants, as this article covers.

As I understand it, the primary purpose of newtypes is actually just to work around typeclass issues like in the examples mentioned at the end of the article. They are specifically designed to be zero cost, because you want to not pay when you work around the type class instance already being taken for the type you want to make an instance for. When you make an abstract data type by not exporting the data constructors, that can be done with or without newtype.

eru an hour ago | parent [-]

The alternative to newtypes is probably to go the same route as OCaml and have people explicitly bring their own instances for typeclasses, instead of allowing each type only one instance?

I think OCaml calls these things modules or so. But the concepts are similar. For most cases, when there's one obvious instance that you want, having Haskell pick the instance is less of a hassle.

lmm an hour ago | parent | prev | next [-]

IME this is exactly backwards: type safety is mostly about names, everything else is a nice-to-have. Yes, you can bypass your name checks if you want to, but you can bypass any type check if you want to. Most relevant type relationships in most programming are business relationships that would be prohibitively expensive to express in a full formalism if that was even possible. But putting names on them is cheap, easy, and effective. The biggest win from typed languages comes from using these basic techniques.

b_e_n_t_o_n 17 minutes ago | parent [-]

Hmm, IME the preferred type systems are structural - a function shouldn't care what the name is of the struct passed to it, it should just work if it has the correct fields.

o11c 6 minutes ago | parent | next [-]

The critical problem with structural typing is that it requires weird and arbitrary branding when dealing with unions of singletons.

stirfish 7 minutes ago | parent | prev [-]

> should just work if it has the correct fields.

Correct fields by...name? By structure? I'm trying to understand.

b_e_n_t_o_n a minute ago | parent [-]

By name, type, and structure. In typescript for example:

   let full_name = (in: { first: string, last: string }) => in.first + " " + in.last
Then you can use this function on any data type that satisfies that signature, regardless of if it's User, Dog, Manager etc.
nixpulvis 2 hours ago | parent | prev | next [-]

In Rust I find myself gaining a good bit of type safety without losing ergonomics by wrapping types in a newtype then implementing Deref for them. At first it might seem like a waste, but it prevents accidentally passing the wrong type of thing to a function (e.g. a user UUID as a post UUID).

skybrian 33 minutes ago | parent | prev | next [-]

The author seems concerned about compile-time range checking: did you handle the full range of inputs?

Range checking can be very annoying to deal with if you take it too seriously. This comes up when writing a property testing framework. It's easy to generate test data that will cause out of memory errors - just pass in maximum-length strings everywhere. Your code accepts any string, right? That's what type signature says!

In practice, setting compile-time limits on string sizes for the inputs to every internal function would be unreasonable. Limits on inputs need to be set at system boundaries.

kazinator an hour ago | parent | prev [-]

What if I want a type called MinusIntMaxToPlusIntMax?

In other words the full range of Int?

Is newtype still bad?

In other words how much of this criticism has to do with newtype not providing sub-ranging for enumerable types?

It seems that it could be extended to do that.