A modern programming language that makes developers happier.

kotlinlang

In the type proofs demo of the Twitter username, the casts returned nullables to model that a String was not a valid Twitter username. Wouldn't it be better if it returned a `Validated`, so it's possible to get the reason why it failed?

Refinement types can check the refined implications of your type at compile time and are in a sense more powerful than runtime checks which you get with data types such as `Validated` . With the Ide support we ship in Meta, Users can see in real time, why their input fails, given the set of refinements that are set.

I see the point for compile-time, but I thought this could be used as well for tests at runtime with `as?` to validate user data?

Each  refined type has this function `from(a : A): B?` , which is what you maybe implying.
So you can do:
`TwitterHandle.from("@SiempreJuan")`

“validation” is now subject to `Null` ,as it is more succinct to Kotlins goal to remove unnecessary wrappers. The existence of a refined value corresponds to the value not being `Null` , which is `Valid` or `Invalid` in the `Validated`  world. Only that those checks happen at compile time and a zero-cost abstraction over the type `A`  one cares about.

And things like Error accumulation boil down to `map` or `mapNotNull`  or a failFast strategy corresponds to vanilla Kotlin working with nullable types.

Sorry, I don't think I explained my question well. When using the `from` function at runtime, is there a way to get the message of why it failed? I get that at compile-time it will show up in the IDE, but it could be interesting to know why something failed at runtime to display a message to the user or something similar

Yes, there is access to the validation map that contains all the entries already validated

it’s in the Refined interface and inherited by the refined type companion, you can call validate instead of from