is there a more compact way to express this ``` init require

Question

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 · Answer

I don t think so only by writing own extension function like level requireRange 0 9 or 0 9

gildor · Answer

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 · Answer

okay thank you

tipsy · Answer

it just seemed unusually verbose for kotlin

gildor · Answer

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 · Answer

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 · Answer

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

raulraja · Answer

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 · Answer

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 · Answer

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 · Answer

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

tipsy · Answer

is refined types what idris calls dependent types

raulraja · Answer

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 · Answer

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

raulraja · Answer

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 · Answer

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

raulraja · Answer

tipsy · Answer

really cool

tipsy · Answer

would be nice with built in support for these concepts