https://kotlinlang.org logo
Join Slack
Powered by
As we go into programming we would frequently repr...
# arrow
r
As we go into programming we would frequently represent things like a TwitterHandle with the type String. The ugly truth is that Twitter is already telling us String covers a lot more values than what a TwitterHandle should be. It does not have to be this way. We can get better types in Kotlin that guarantee some constraints at compile time with a flavor of type refinements. I based this example in the talk https://kwark.github.io/refined-in-practice/#1 by @kwark to show how its example around TwitterHandle could be modeled in the upcoming type proofs April release with Arrow Meta. We have an initial draft with some tests that show we can bring expressions that serve both for constant and runtime validation for more precise and safe types. The user does not need to learn any type-level predicates or a specialized DSL since predicates can be expressed as receiver functions whose expressions are evaluated at compile-time without contextual dependencies. The user just provides the rules to describe the type predicates and uses the Apis available in the std lib or other user-supplied libs that can run alongside the compiler class-path in a compiler plugin.
RefinedTypes_kt.kt
arrow 15
🔝 9
❤️ 20
m
One can achieve this using a 
data class
, making the constructor private, and overriding 
invoke
in the companion object, BUT this is cleaner, and allows for usage of 
inline class
, so the compiler can do it's thing with 
inline class
that it wouldn't be able to do with a 
data class
or 
class
. Keep up the great work on Arrow and Meta!
s
It can do more than that such as checks literals at compile time. For example for 
PositiveInt
I can make this not compile 
PositiveInt(-1)
And as you can see in the example you can also implicitly capture it like that. 
val i: PositiveInt? = -1
results in 
null
val i2: PositiveInt? = 3
results in 3 etc
j
also lets not forget that 
data class
+ 
invoke
can be bypassed by 
copy
^^ Thus this is also safer
m
Sorry, my 'BUT' was intended to say we can accomplish something similar now BUT the Meta approach is MASSIVELY SUPERIOR!!!! Sorry that wasn't clear.
👍 2
🙌 1
And yes, I also didn't state that Meta's approach is compile time, whereas the invoke is runtime.
s
I never really found a solution I’m happy with in Vanilla Kotlin, which is why I am so excited for this. Mostly because of 
copy
in data-classes, or additional required boilerplate if not using 
data
.
m
Agreed. The goal can be achieved with good code review, and caveats and extra work, but as you say, no one is likely to be pleased using it. Similar to coding in Java vs Kotlin. Can do the same things, but I think we both agree which is more pleasant to use ;)
m
This is amazing!
a
@raulraja - would you have this example in a GitHub repo? I'd like to try it locally, and getting undefined errors for 
Refined
. 😞
r
Hi @Attila Domokos it’s currently in the sv-test-proofs branch but there is an issue in the test DSL. Though the two simple tests are here:
still rough work in progress and not yet in Meta master
a
I see. This is helpful, thank you @raulraja!
r
No problem, if you have any questions or concerns feel free to ask around here
Some kind person just told me you can also make the inline class constructor private…
a
Will this be in Arrow 0.11 or 0.10.5?
r
This will be part of Arrow 1.4 or the first Arrow release depending on meta that follows the same release lifecycle as the compiler and language
We expect to have something around April we can test in the Arrow code base and make it official as a feature around the summer
👍 1
Also with type classes, union types and other features we are building on type proofs
😍 2
j
private inline class constructors? 🎉 That + refined types is perfect ^^
r
LOL yeah
j
Does typeclass resolution work on inline classes? Last I tried with the current kapt generated stuff it failed when the inline class got inlined^^ If that works we can have performant mtl o.O
➕ 1
s
Yes, but that’s 
kapt
which works on the JVM code. With Arrow Meta you work with the Kotlin code directly, so the 
inline class
should still be tehre
Yes, fast MTL!!! I already pitched this to Raul a while back haha
That’d be amazing
3 Views
Open in Slack
PreviousNext
Powered by