Comment by crabbone | Hacker News Reader

Comment by crabbone | Hacker News Reader

Parent Full thread

Your type doesn't describe prime numbers. You just named it "prime number", but there's no proof or any other guarantee that it's a prime number.

> People get too caught up in thinking that the type _has_ to express intricate properties

Where do you get this from? Did you even read what you are replying to? I never said anything like that... What I'm saying is that the approach taken by OP is worthless when it comes to real-life uses of validation.

So, continuing with your example: you will either end up doing validation instead of parsing (i.e. you will implement parsePrime validator function), or your will not actually validate that your input is a prime number... The whole point OP was trying to make is that they wanted to capture the constraints on data in a type describing those constraints, but outside of trivial examples s.a. non-empty list, that's used by OP, that leads to programs that are either impossible or are extremely complex.

> One can quite easily create a closed module that encapsulates a ValidPassword

And, again, that would be doing _validation_ not parsing. I'm not sure if you even understand what the conflict here is, or are you somehow agreeing with me w/o saying so?

If you can't create a value of type PrimeNumber that doesn't contain a prime number, there's a bit more to it than naming. Not all type-level guarantees need to come from structural properties of the type. They can also come from structural properties of the environment of the type. Providing no public constructor is such a property.

The example was written rather badly, though. It should have pointed out that the module was exporting the type and a couple helper functions, but not the data constructor.

But despite that, the key point was correct. Validating is examining a piece of data and returning "good" or "bad". Parsing is returning a new piece of data which encodes the goodness property at the type level, or failing to return anything. It's a better paradigm because the language prevents you from forgetting what situation you're in.

> If you can't create a value of type PrimeNumber that doesn't contain a prime number, there's a bit more to it than naming.

Yes, indeed. This is quite useful! But crabbone isn’t entirely wrong that it isn’t quite what the original article was about.

I’ve written quite a bit of code where constructive data modeling (which is what the original article is really about) was both practical and useful. Obviously it is not a practical approach everywhere, and there are lots of examples where other techniques are necessary. But it would be quite silly to write it off as useless outside of toy examples. A pretty massive number of domain concepts really can be modeled constructively!

But when they can’t, using encapsulation to accomplish similar things is absolutely a helpful approach. It’s just important to be thoughtful about what guarantees you’re actually getting. I wrote more about that in a followup post here: https://lexi-lambda.github.io/blog/2020/11/01/names-are-not-...

> If you can't create a value of type PrimeNumber that doesn't contain a prime number

Because you wrote a validation function, the exact thing OP told you not to do. Hooray?!

The goal of OP was to create a type that incorporates constraints on data, just like in their example about the non-empty list they created a type that in the type itself contains the constraints s.t. it's impossible to implement this type in a way that it will have an empty list.

You did the opposite. You created a type w/o any constraints whatsoever, and then added a validation function to it to make sure you only create values validated by that function. So... you kind of proved my point: it's nigh impossible to create a program intelligible to human beings that has a "prime number" type, and that's why we use validation -- it's easy to write, easy to understand.

Your type isn't even a natural number, let alone a prime number.

Are you aware that it's impossible to do any kind of parsing without validating the data? Saying "you have a validation function" is not some sort of disproof of parsing.

Parsing is an additional job on top of validation - providing type-level evidence that the data is good. That's what makes it valuable. It's not some theoretical difference in power. It's better software engineering.

Reply on news.ycombinator.com