Type Refinements with Type Proofs in Kotlin

TwitterHandle.kt

/* 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")

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.