I’m messing around with trying to implemented a `C...

# arrow

[tavish pegram]

I’m messing around with trying to implemented a Constrained<T> as a DSL for domain modeling (inspired by this and other similar talks

https://www.youtube.com/watch?v=PLFl95c-IiU▾

). What I would really love is to make it a one liner to create constrained types with private constructors so that it becomes effortless to use in domain modeling. Currently in Kotlin the way to implement something like this is

data class Natural private constructor(val value: Int) {
    companion object {
        fun fromInt(v: Int): Either<NaturalFromIntFailure, Natural> =
            when (v < 0) {
                true -> NaturalFromIntFailure.IntMustBeGTEZero.left()
                false -> Natural(v).right()
            }
    }
}
sealed class NaturalFromIntFailure {
    object IntMustBeGTEZero: NaturalFromIntFailure()
}

which is fine I guess, but if people want to get in the habit of using constrained domain types for every type in a domain (as is recommended), this starts to become tedious and starts to lead toward cutting corners on these types.

From reading about dependent types, it would be awesome to do something like

typealias Natural = Constrained<Int><{ 
    when (it < 0) {
        true -> NaturalFromIntFailure.IntMustBeGTEZero.left()
        false -> Natural(it).right()
    }
}>
val x = Natural(-1) // Doesnt compile
val y = Natural.new(-1) // Left(NaturalFromIntFailure.IntMustBeGTEZero)

Alas messing around hasn’t gotten me close to this at all. This is the best I’ve gotten so far which is still a little too verbose , doesn’t have a consistent interface for constrained types, and has some public “private” methods :(

/*
----------------------------------------------------------------------------------------------------
Generic bits
 */
data class Constrained<A> private constructor(val a: A) {
    companion object {
        fun <A, E>validateNew(a: A, validator: (A) -> Either<E, A>): Either<E, Constrained<A>> =
            validator(a).fold(
                { it.left() },
                { Constrained(a).right() }
            )
    }
}

/*
----------------------------------------------------------------------------------------------------
Consumer Implementation
 */
typealias Natural = Constrained<Int>
sealed class NaturalFromIntFailure {
    object IntMustBeGTEZero: NaturalFromIntFailure()
}

fun natural(a: Int) = Natural.validateNew<Int, NaturalFromIntFailure>(a) {
    when (it < 0) {
        true -> NaturalFromIntFailure.IntMustBeGTEZero.left()
        false -> it.right()
    }
}
/*
----------------------------------------------------------------------------------------------------
Examples
 */

val a = Natural(-1) // Doesn't compile
val b = natural(1)  // Result: Right(Natural(1))
val c = natural(-1) // Result: Left(NaturalFromIntFailure.IntMustBeGTEZero)

Does anyone have any suggestions on if there are any tools available in arrow that could move this closer to the ideal state?

[raulraja]

Arrow is solving this issue with meta after 1.4 with Refined types

[raulraja]

https://www.youtube.com/watch?v=ETn_6LmMjho▾

[raulraja]

https://github.com/arrow-kt/arrow-meta/blob/master/compiler-plugin/src/test/kotlin/arrow/meta/plugins/refinement/RefinementTests.kt

[tavish pegram]

very cool, thank you!

[raulraja]

Also after refined types will come liquid expressions which essentially allow you to constrain without the type encapsulation since all expressions in Kotlin are typed after analysis

[raulraja]

Then you will be able to do this:

[raulraja]

inline fun Int.portNumber(): Int =
  +(0..65535)..this

[raulraja]

which the compiler can refine and ensure symbolically this had to been prechecked by a logical precondition in the scope data flow before it’s safe to call otherwise a nullable, Either or Validated runtime api like yours is provided

[raulraja]

automatically

[raulraja]

This is more powerful than Scala or Haskell dependent type refinements since it can be arbitrary lifted to expressions that can be evaluated symbolically

[raulraja]

and there is no type carrying burden on type signatures which would not play nice in a lang like Kotlin without path dependent types

[raulraja]

I encoded scala refined entirely in Kotlin and the lack of path dependent types forces you to carry them as type arguments at all call sites which makes the DSL unusable

[raulraja]

https://github.com/fthomas/refined

[raulraja]

Hope this gives an update on where we are at in terms of ensuring safe domains and expressions

[tavish pegram]

very excited for this stuff!

[raulraja]

I believe in Kotlin smart casting and dataflow are more relevant than typelevel nats and similar to offer an api people can use with compile time guarantees because type level programming in kotlin is not possible without path dependent types or singleton nats.