is there a more compact way to express this? ``` ...

# announcements

[tipsy]

is there a more compact way to express this?

init {
    require(level in 0..9) {
        "Valid range for parameter 'level' is 0 to 9"
    }
}

[gildor]

I don't think so, only by writing own extension function like:
level.requireRange(0, 9) // or 0..9

[gildor]

You cannot get name of property with this code, but you can pass it separately. You also can use property reference of course, but it will create method reference lambda on each usage, so not sure that it worth to do

[tipsy]

okay, thank you

[tipsy]

it just seemed unusually verbose for kotlin

[gildor]

How would you make it less verbose without introduction separate function explicitly for this use case?
And imo it's good, Kotlin stdlib is not an assert library to have all kinds of checks

[raulraja]

It may overkill for your use case but we are in Arrow currently exploring compiler plugins and we discussed an implementation of refined types that would compile time check literals and provide a safe validation API for runtime values. https://github.com/47deg/arrow-meta-prototype/issues/6

[raulraja]

Nothing there yet, just think it's possible with plugins and will attempt to do it in arrow meta.

[raulraja]

This would allow in the future to have a type that represents the positive values from the singleton type literal Nat 0 to Nat 9 and it's able to not compile if there is an Int literal out of range of that type.

[raulraja]

I think it may be possible with a custom TypeChecker and a custom CallChecker which are services compiler plugins can contribute today to the storage component container

[raulraja]

I did something similar with a custom TypeChecker where we make kinds and concrete values be of the same type when compiled and it eliminates the need for kind casts in arrow. If you are interested in this support at compile time in the future feel free to watch the evolution of the issue I linked above

[tipsy]

definitely overkill for my use case (which was just seeing the snippet in a code review), but very interesting

[tipsy]

is refined types what idris calls dependent types?

[raulraja]

Yes, it's a kind of dependent type since it has constrains on other types that come materialized after itself. For example Int with Positive . Positive can be derived also from Order

[raulraja]

In general most Kotlin and java model could be better typed if languages supported type refinements

[raulraja]

In Scala we have the library refined which shows all that it's possible and most mature code based in the Scala industry seem to be using it

[raulraja]

It allows models to be a lot more expressive and it eliminates the need for many tests

[raulraja]

https://speakerdeck.com/raulraja/types-vs-tests?slide=27

[tipsy]

really cool!

[tipsy]

would be nice with built in support for these concepts