Skip to content

Instantly share code, notes, and snippets.

@raulraja
Created February 20, 2020 12:16
Show Gist options
  • Save raulraja/a40b9a9fb3c381ec3281afac77f326d3 to your computer and use it in GitHub Desktop.
Save raulraja/a40b9a9fb3c381ec3281afac77f326d3 to your computer and use it in GitHub Desktop.
Type Refinements with Type Proofs in Kotlin
/* Coming up ~ April 2020 */
package test
import arrow.*
inline class TwitterHandle(val handle: String) {
companion object : Refined<String> {
override val validate: String.() -> Map<String, Boolean> = {
mapOf(
"Should start with '@'" to startsWith("@"),
"Should have length <= 16" to (length <= 16),
"Should not contain the word 'twitter'" to !contains("twitter"),
"Should not contain the word 'admin'" to !contains("admin")
)
}
}
}
/**
* Similar extensions can target Validation and Either not just nullable types
* Proofs `String` can be coerced safely into a TwitterHandle
*/
@Proof(TypeProof.Extension, coerce = true)
fun String.twitterHandle(): TwitterHandle? =
if (TwitterHandle.isValid(this)) TwitterHandle(this)
else null
val admin = "@admin"
val whatever = "@whatever"
/* Fails to Compile:
* "@adminxxxxxxxxxxxxxxxxxxxxxxxx" is not a valid TwitterHandle because:
* e: Should not contain the word 'admin'
* e: Should have length <= 16
*/
TwitterHandle("@adminxxxxxxxxxxxxxxxxxxxxxxxx")
TwitterHandle("@whatever")
//TwitterHandle("@whatever")
val ok: TwitterHandle = "@whatever"
//TwitterHandle("@whatever") //ok
val nullableOk: TwitterHandle? = "@whatever"
//TwitterHandle("@whatever")
val runtimeAdminWillBeNull: TwitterHandle? = admin
//null
val runtimeWhateverIsValidated: TwitterHandle? = whatever
//TwitterHandle("@whatever")
@raulraja
Copy link
Author

raulraja commented Feb 20, 2020

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment