Refinement Types: Design Notes

[InversionSpaces]

This is a discussion of Refinement Types for Kotlin.
Refinement Types allow narrowing types by specifying constraints on their values, thus enhancing type safety and reducing the number of bugs.

// Refinement Class
@Refinement
value class Pos(val value: Int) {
    init { require(value > 0) }
}
// Refinement Subtype
refinement Pos = Int satisfies { it > 0 }

Design notes could be found here.

Important: This is not a proposal, we did a research on the topic, but we don't intend to bring Refinement Types to Kotlin at the moment. However, we're sharing our work to be transparent, and we'd love to hear your thoughts, suggestions, or concerns.

[sam-coopercode]

I can definitely think of some scenarios where this would be a cool feature! For instance, having the type system know about non-empty collections would be great. Here are a few thoughts that jump to mind after reading the design notes. I haven't ever used a language that has refinement types like this (the closest I've gotten is TypeScript), so I'm no expert, and these might be things that have been solved (or rejected) by other languages 😁:

• I think I prefer the subtypes idea over the refinement classes. As you noted, it seems like a value (or value-like) class such as URL or UInt is already good enough for most practical uses. Dynamically refining existing types, though, seems much more interesting—let me elaborate:
• It'd be useful if these refinement types could be generated and inferred dynamically. For instance, if I know that x is between 0 and 10, and then I write val y = x + 1, then now I know that y is between 1 and 11. The compiler should be able to figure out and keep track of y's refined type without me having to create an explicit 1..11 type.
• Collection types become more powerful if we store not just the boolean condition of empty/non-empty, but rather a richer type that records the size of the collection, like List<T>[3] (or a range within which we know the size to be, like List<T>[1..10]). This is easier if you already have automatic number range types as described above. In certain single-threaded contexts I think this might even allow limited modification of "non-empty" or other refined-size collections?
• In some ways these refinements seem a lot like generics. I get the impression that, like generics, refinements could be checked at compile time and fully erased at runtime, which would be cool.
• If refinements can be erased, they could also be implemented at least experimentally via a compiler plugin, using Kotlin's existing @ annotations, so I tend to agree with the decision not to add new language features to support them, at least for now.

Anyway, that's the end of my rambling. Thanks for sharing the design notes! It's really interesting to see the thought process even for a feature that's not going to be implemented.

[kyay10]

I think what you're looking for is dependent typing, as in having a type depend on a value (like a list of specific size). It's very powerful, but might be too much for Kotlin (it is mentioned briefly in the notes)

[sam-coopercode]

Thanks! Now that I look again, it seems like a lot of the things I mentioned in my post above (including erasure, even) are actually touched on in the design notes 🤦. I think "dependent" was the clue I needed to find the right section of the document and spot the connections 🙇

[InversionSpaces]

Note that things that need computations on type level only are achievable without dependent typing.
For example, scala is somewhat capable of handling your example with numbers (I simplified it a little):

val y: Int :| Greater[5] = 6
val x: Int :| Greater[1] = 2

inline def add[la <: Int, lb <: Int](
    a: Int :| Greater[la],
    b: Int :| Greater[lb]
  ): Int :| Greater[la + lb] = refineUnsafe(a + b)

def test(v: Int :| Greater[6]) = println(v)

test(add(x, y))

scastie: link

In the same manner, it is possible to type append(List[T] :| Size[n], List[K] :| Size[k]) : List[T] :| Size[n + k].

You need dependent typing if you want to lift values to type level, e.g.

fun <T> List<T>.take(n: Int): List<T> satisfies { it.size <= n } // n is a value, mentioned in the type

[kyay10]

Edit: This got a little rambly, so apologies if it's difficult to read!

I think subtypes would be the way to go if this feature ever happens.
I want to suggest a simplification for subtypes: no magic compiler inference or solving. Just 2 options:

opaque typealias Foo = Bar
typealias Baz = Bar satisfies { it.foo() }

No magic compiler detection, instead all just contracts driven. opaque typealiases don't have is and as checks. satisfies typealiases do. An opaque typealias can thus only be created through contracts and an unsafe cast.
Subtyping of refinements works simply through contracts too.

But a more important issue would still persist: the necessity to repeat large API parts if they preserve the refinement

I really don't think that's as big of an issue as you think. This is already necessary with value classes. It's also library boilerplate that normal users likely won't face. It can be easily automated with IntelliJ too. It's ultimately as simple as writing a single declaration and some casts. I don't think there's a more elegant but Kotlin-y way to do that. You have highlighted that there's a limited amount of such refinement types that one needs to create anyway, and so they'd likely be covered by libraries rather fast.

I think having extensions take priority over members for refinement subtypes makes perfect sense, and helps address that typetag feature like you said.

I really don't like Implicit Refinement. It's too much implicit behaviour for Kotlin. Instead, I think type casts are reasonable in such a case.

w.r.t. refinements that refer to a member property, I think contracts and smart casts should be extended first to support that, and then it'll work naturally for refinements too.

what types should be allowed for T in fun f(v: T): T

This is just intersection types I think. Simply any type that happens to have T : Pos should be allowed. Just like if Pos was actually an interface. This'd also mean that T : String, which gives a warning right now, would actually have use.

Mutable underlying values can violate refinement predicates after initial validation, making the type system guarantees unreliable

Smartcasts already deal with this. Use the same system (and make them smarter as well by allowing a way to declare that a val is truly unchanging).

[InversionSpaces]

An opaque typealias can thus only be created through contracts and an unsafe cast.
Subtyping of refinements works simply through contracts too.

Sorry, I don't quite understand, could you possibly elaborate with code examples you have in mind?

w.r.t. refinements that refer to a member property, I think contracts and smart casts should be extended first to support that, and then it'll work naturally for refinements too.

This happens to be a challenging task deserving its own discussion, as tracking possible mutations for members is hard.

Simply any type that happens to have T : Pos should be allowed.

Well, sure, but the question is actually about which types do we consider as subtypes of Pos. Is it only the types which are defined as refinements of Pos or is it any refinement of Int which has a predicate at least as strict as Pos do?

Smartcasts already deal with this.

Unfortunately, they dont. Right now smartcasts work only work with checks that have the same result as long as identity is unchanged (v is I and v != null) and only with value that are stable (their identity can't change) (well, strictly speaking there is a limited support for vars). Tracking deep mutations inside an object, and whether they can invalidate some complicated predicate is much harder.

[kyay10]

opaque typealias MyInt = Int

fun myInt(x: Int): MyInt = (x * x) as MyInt

fun Int.isMyInt(): Boolean {
  contract {
    returns(true) implies (this@isMyInt is MyInt)
  }
  return math.sqrt(this) * math.sqrt(this) == this
}

For the subtyping situation, I meant that checker functions can imply that the parameter is of multiple refinement types. This might also motivate intersection types so that one may return a Positive & Even or something:

typealias Positive = Int satisfies { it > 0 }
typealias Even = Int satisfies { it % 2 == 0 }
typealias PositiveEven = Int satisfies { it % 2 == 0 && it > 0}

fun Int.isPositiveAndEven(): Boolean {
  contract {
    returns(true) implies (this@isPositiveAndEven is Positive && this@isPositiveAndEven is Even && this@isPositiveAndEven is PositiveEven)
  }
  return this is PositiveEven
}

Maybe we can have more complex contracts too:

fun Int.isEven(): Boolean {
  contract {
    returns(true) implies (this@isEven is Even)
    (returns(true) && this@isEven is Positive) implies (this@isEven is PositiveEven)
  }
  return this is Even
}

Is it only the types which are defined as refinements of Pos or is it any refinement of Int which has a predicate at least as strict as Pos do?

My solution is to ignore this entirely, and rely on people to use contracts and intersection types aptly to communicate that:

typealias BiggerThanOne = Int satisfies { it > 1 }
fun Int.isBiggerThanOne(): Boolean {
  contract {
    returns(true) satisfies (this@isBiggerThanOne is Positive && this@isBiggerThanOne is BiggerThanOne)
  }
  return this is BiggerThanOne
}

Unfortunately, they dont.

That's what I meant. Simply inherit the limitations of smart casts. If smart casts improve, this feature automatically improves.

[mikehearn]

It may be worth noting prior art here in the form of Java's validation libraries:

fun foo(@Email email: String) { ... }

Frameworks like Spring or Micronaut can enforce these constraints at runtime, but not always. It depends if the method is being invoked by the framework or not. I would prefer Kotlin continue its tradition of leaning into existing Java practice both for its familiarity and the practical benefits e.g. none of the refinement type proposals given above address reflection or database validation at all, whereas validation annotations do.

So one practical compromise might be to look at what it'd take to improve the validator libraries. For example, off the top of my head:

• Provide a way to integrate validation AOP advice with the compiler so validations work even on private methods that the Java frameworks can't / shouldn't override. The Java approach of exploiting virtual-by-default and overriding every method is a hack that wouldn't be needed if the language compiler knew about this stuff.
• Provide a more sophisticated ABI in which a method call can be dispatched via a 'back door' if the compiler knows constraints were already checked, i.e. the method above would compile to fun foo(email: String) { assertIsEmail(email); foo$validated(email) } and if the compiler can prove an argument comes from a field or value that's already annotated, it just directly invokes the $validated method. This would be a cheap'n'cheerful form of "optimization" that can avoid practical costs like regex invocations, and the compiler has freedom to decide whether to do the same validations at call sites or in the callees. The IDE can highlight places where pushing the validation upwards would be useful.
• Invoke the validation engine on variable assignment e.g. @Email val email: String = userInput would trigger the runtime check.
• Type aliases can then be used to "refine" String to Email without breaking existing APIs or introducing wrapper classes.

I guess you can think of many more. Data validation is useful but there's a lot of prior art here already that's deeply integrated with infrastructure like web servers and ORMs. Static analysis is great but there's no need to let perfect be the enemy of the good here. Even just more consistent and usable runtime validation would be an upgrade.