Daydreaming proofs as contracts

prelude.kt

package arrow.meta.ide.plugins.proofs.contracts

import kotlin.contracts.Effect
import kotlin.contracts.ExperimentalContracts

interface TypeLevelEffect : Effect

interface Declaration : Effect

fun declaration(): Declaration = TODO()

infix fun <A> Declaration.implies(proof: TypeLevelEffect): TypeLevelEffect = TODO()

fun extension(): TypeLevelEffect = TODO()

fun implicitConversion(): TypeLevelEffect = TODO()

infix fun <A> A.refinedBy(f: (A) -> Boolean): TypeLevelEffect = TODO()

typeclasses.kt

package arrow.meta.ide.plugins.proofs.contracts

import kotlin.contracts.ExperimentalContracts
import kotlin.contracts.contract

/** type class **/
interface Appendable<A> {
  fun append(other: A): A
}

/** extension instance **/
inline class StringAppendable(val value: String): Appendable<String> {
  override fun append(other: String): String = value + other
}

@ExperimentalContracts
fun String.appendable(): Appendable<String> {
  contract {
    // projects all members of Appendable<String> over String
    declaration() implies extension()
  }
  return StringAppendable(this)
}

typerefinements.kt

package arrow.meta.ide.plugins.proofs.contracts

import kotlin.contracts.contract

inline class PositiveInt(val value: Int)

fun Int.toPositiveInt(): PositiveInt? {
  contract {
    declaration() implies (this@toPositiveInt refinedBy { it > 0 })
  }
  // repeating the predicate here is not ideal
  return if (this > 0) PositiveInt(this) else null
}

fun PositiveInt.toInt(): Int =
  value

fun PositiveInt?.toInt(): Int? =
  this?.value

unions.kt

package arrow.meta.ide.plugins.proofs.contracts

import kotlin.contracts.ExperimentalContracts
import kotlin.contracts.contract

/** unions **/
interface Union22<out A, out B, out C, out D, out E, out F, out G, out H, out I, out J, out K, out L, out M, out N, out O, out P, out Q, out R, out S, out T, out U, out V>
inline class Union(val value: Any?) : Union22<`🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`, `🔥`>
typealias First<A> = Union22<A, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing>

@ExperimentalContracts
fun <A> A.first(): First<A> {
  contract {
    /** enables implicit conversion for cases like
     * fun f(): Union2<String, Int> = 0
     */
    declaration() implies implicitConversion()
  }
  return Union(this)
}