Refinement Types?

Language Design
1

Has the Kotlin team thought about introducing Refinement Types?

It’d be cool to be able to make certain assertions at compile time safely, i.e:

class User(
  val name: String,
  val age: Int :: { it >= 0 }
)

and to instantiate a User:

val name = readLine() ?: ""
val age = readLine()?.toIntOrNull() :: { it >= 0 } ?: 0

val user = User(name, age)

A type that is refined will turn into an optional, like the above, unless it can be smart casted:

val number = 3
val refinedNumber: Int :: { it > 0 } = number :: { it > 0 } // compiles
// and obviously the type definition is redundant

a less verbose syntax might be interesting to explore (although I don’t prefer it):

val refinedNumber: Int? :: { it > 0 } = number :: > 0

because it might be harder to follow without the {}, and the above would probably require a lot of work, I’d imagine it’d be hard for the lexer to decipher the difference between :: > 0 and :: 0 < or even

:: > 0 && < 15

Plus the above seems pretty hard to decipher for a human as well.

:: { it > 0 && it < 15 }

seems a lot more readable, plus you could write blocks to DRY up similar refinements.

2 Likes
2

And also to note, it would be ideal to be able to use typealias with the above.

typealias PositiveInt = Int :: { it > 0 }
3

I like the idea, I don’t like this syntax.
Maybe it’s possible to combine this with inline classes?
The only problem is that at the moment inline classes don’t allow constructor-blocks.
I think this is due to that the checks have to be copied inside every method that accepts an inline class, due to Interop with java, but I’m not entirely sure.

4

Utilizing inline-classes to achieve this type of functionality is interesting, and might be easier to do on the development side of things (I have no clue, never made a language).

The syntax probably does use the : symbol too frequently, I just came up with a syntax that’s unused, I’m sure there are better solutions.

I think the biggest thing for me is I want the refinement to happen by a block of type

(T) -> Boolean

so we can utilize things like the it keyword and allow the ability to simply dry up code by passing blocks around.

If we wanted to do this via inline classes with a different syntax, maybe something like the following would work?

inline class Age(val i: Int) {
    refined by { i >= 0 }
    // or
    refined { i >= 0 }
}

(although the block type here would actually be)

() -> Boolean

this solution would take a little more boilerplate for the functionality, but then we wouldn’t need to track refinements in the types. No Int :: { it > 0 } types, which might be ideal.

Inline classes would have to be able to return T? in the case that the refinement fails. No idea how easy that would be to do, hopefully easier than the system I proposed originally.

5

I like the idea of refining types. I’m curious to know whether there are other languages that do this?

I’m not sold on the idea of how you want to refine values. It feels too similar to the existing x.takeIf{it > 5}, just that your’s is less readable. Once refined types are available, the takeif function could maybe get a contract that refined its return type.

6

A couple other languages have refinement type implementations. Scala & Haskell namely (there are libraries that enable them).

In my OP, what I was describing was refinement types, which is different from x.takeIf { it > 5 } in that it actually defines a new type.

I suppose in our discussion we were kind of moving away from the idea, and I think that’s because I can be swayed away from refinement types if the following is true for whatever implementation replaces it:

  1. It’s just as safe
  2. You can somehow denote two variables have the same refinement by their type (either by refinement types or inline classes that are refined by a block, or by something I’m not thinking of).

Yeah I’d like takeIf to return a refined type, if we went with refinement types over refining inline classes.

Right now, the advantages for my OP refinement type suggestion is that it has less boilerplate than my inline class refinement type syntax. On the flip side, inline classes are already an (experimental?) feature in 1.3, so it may be easier to include refinements there.

7

The OP actually introduced 2 things, but both have the same syntax. The one thing is type refinements, which I find interesting and cool. The other thing is runtime type check against a refined type. This one I find a bit obsolete.

The followng line from the OP

readLine()?.toIntOrNull() :: { it >= 0 } ?: 0

could be replaced by

readLine()?.toIntOrNull()?.takeIf{ it >= 0 } ?: 0

When takeif’s contract is adjusted to return a refined type, this will have the same meaning.

8

Ah, good catch.

Definitely agree with your assessment there.

9

The scala refined type GitHub - fthomas/refined: Refinement types for Scala contains also rules like

typealias PositiveInt = Int :: { it > 0 }
typealias Age = Int :: { it > 0 && it < 130 }
val x: Age = 20
val posN:PositiveInt = x; // compilation OK
val age: Age = posN; // compilation KO

10

If I’m not mistaken you could probably do this with delegation and generics pretty easily in the language already.

The delegate class:

import kotlin.reflect.KProperty

class Refined<T>(initialValue: T, private val validator: (T) -> Boolean) {
    private var backingField: T = initialValue

    operator fun getValue(thisRef: Any?, property: KProperty<*>): T {
        return backingField
    }

    operator fun setValue(thisRef: Any?, property: KProperty<*>, value: T) {
        if (validator(value)) {
            this.backingField = value
        }
        else {
            // Throw some exception here?
            println("Validation failed!")
        }
    }
}

Sample usage:

var onlyPositive by Refined<Int>(defaultValue = 1) { it > 0 }
println("OnlyPositive initial value: $onlyPositive")
onlyPositive = 5
println("OnlyPositive value changed: $onlyPositive")
onlyPositive = -5
println("OnlyPositive did not accept negative value: $onlyPositive")

Output:

OnlyPositive initial value: 1
OnlyPositive value changed: 5
Validation failed!
OnlyPositive did not accept negative value: 5

1 Like
11

The objective is to have compilation warning

onlyPositive = -5
Should not compile with refinement type.

12

This was pretty awesome, thanks!

I modified the code a bit:

class Refined<T>(private var value: T?, private val validator: (T) -> Boolean) {
    operator fun getValue(thisRef: Any?, property: KProperty<*>) = value

    operator fun setValue(thisRef: Any?, property: KProperty<*>, value: T?) {
        this.value = if (value != null && validator(value)) value else null
    }
}

so now in the final case, onlyPositive becomes null, instead of retaining it’s value of 5.

13

The biggest problem this still faces though is my second point:

  1. You can somehow denote two variables have the same refinement by their type (either by refinement types or inline classes that are refined by a block, or by something I’m not thinking of).

There’s no way for this to happen if I’m not mistaken. If I want a method to require an Int of refinement { it > 5 }, I can’t find a way to do that.

Maybe typealises would work? I couldn’t find a way.

EDIT:
I think I found a way:

class PositiveNumber(value: Int) : Refined<Int>(value, { it > 0 })

open class Refined<T>(var value: T?, private val validator: (T) -> Boolean) {
    init { value = valueOrNull(value) }

    operator fun getValue(thisRef: Any?, property: KProperty<*>) = value

    operator fun setValue(thisRef: Any?, property: KProperty<*>, value: T?) {
        this.value = valueOrNull(value)
    }

    private fun valueOrNull(value: T?) =
        if (value != null && validator(value)) value else null
}

still not as concise as having refined syntax, but it should serve mostly the same purpose!

EDIT 2:
@emanguy I was playing around with this some more, and found out I can’t easily pass PositiveNumber into a method. If I require a PositiveNumber, I have to wrap any Int. It’d be cool if it automatically wrapped it, similarly to how it works locally.
LMK if you have any ideas

14

This would be ideal, but I don’t think there’s a way to enforce that without a literal change the language, which would still be great!

15

I haven’t tested this, but based on the documentation it looks like you can have parameters of PositiveNumber type and then pass your delegated variable via the following syntax:

var positiveOnly by PositiveNumber(5)
myMethodThatTakesPositiveNumbers(::positiveOnly)

But again, that’s a total guess based on the documentation here: https://kotlinlang.org/docs/reference/delegated-properties.html#translation-rules

16

How would we get the value supplied at the compile time ?

17

Same way as in scala

for examples :
typealias PositiveInt = Int :: { it > 0 }
var x : PositiveInt = 12 // constant affectation, checked at compile time.

typealias Age = Int :: { it > 0 && it < 130 }
fun foo( val a : Age) {
var x : PositiveInt = a; // compilation ok, because Set ‘PositiveInt’ contains Set ‘Age’.
var y : Age = x; // compilation ko.,
}

var y : Int = random();
var x : PositiveInt = PositiveInt::check(y); // runtime exception if y < 0.

That’s also means you could only have contraints on comparable type (number, date …) and on String (with regular expression).

18

This is adjacent in some ways to the proposal for contracts.

19

proposals for contracts is for controling function behavior, not for type.

it’s adjacent in that’s both proposals are for reliability by adding controls on compilation and prevents bugs.

20

At the moment, you’re correct.
I however like to see something like:

inline class NonEmptyString(val t: String){
    init {
        contract{ 
             (t == "") implies notReturning()
        }
        if(t == "") throw IllegalArgumentException()
    }
}

Of course I don’t know if this ever will happen, but thinking about what could be is fun :wink: