https://kotlinlang.org logo
#announcements
Title
# announcements
t

tipsy

07/13/2019, 8:41 AM
is there a more compact way to express this?
Copy code
init {
    require(level in 0..9) {
        "Valid range for parameter 'level' is 0 to 9"
    }
}
g

gildor

07/13/2019, 9:05 AM
I don't think so, only by writing own extension function like: level.requireRange(0, 9) // or 0..9
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
t

tipsy

07/13/2019, 9:10 AM
okay, thank you
it just seemed unusually verbose for kotlin
g

gildor

07/13/2019, 9:11 AM
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
r

raulraja

07/13/2019, 10:56 AM
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
Nothing there yet, just think it's possible with plugins and will attempt to do it in arrow meta.
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.
😲 1
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
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
t

tipsy

07/13/2019, 11:32 AM
definitely overkill for my use case (which was just seeing the snippet in a code review), but very interesting
is refined types what idris calls dependent types?
r

raulraja

07/13/2019, 11:34 AM
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
In general most Kotlin and java model could be better typed if languages supported type refinements
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
It allows models to be a lot more expressive and it eliminates the need for many tests
t

tipsy

07/13/2019, 11:56 AM
really cool!
would be nice with built in support for these concepts
2 Views