Kotlin proposal

hybrid_refinement_types_proposal.md

Proposal: "Hybrid Refinement Types"

(Compile-time validation where possible, runtime checks where necessary)

Concept:

Introduce refinement types that:

1. Enforce constraints at compile time for literals and compile-time-known values.
2. Generate runtime checks for dynamic values (e.g., variables computed at runtime).
3. Integrate with Kotlin’s contracts and smart-casting to minimize boilerplate.

---

Syntax & Mechanics:

// Define a refinement type with a predicate  
typealias PositiveInt = Int where this > 0  

// Compile-time validation (for literals)  
val a: PositiveInt = 5   // ✅ Compiles  
val b: PositiveInt = -2  // ❌ Compile-time error  

// Runtime validation (for dynamic values)  
fun calculate(x: Int): PositiveInt {  
    val result = x * 2  
    return result.asRefined<PositiveInt>() // ✅ Compiles, checks at runtime  
}  

val dynamicValue: PositiveInt = calculate(3) // ✅ Runtime check: 6 > 0  
val invalidValue = calculate(-5)             // ❌ Runtime exception: -10 !> 0  

---

Key Features:

1. Compile-Time Checks for Constants:

   • Validate literals and const val values during compilation.
   • Example: const val MAX: PositiveInt = 100 (validated once at compile time).

2. Runtime Checks for Dynamic Values:

   • Automatically insert runtime assertions when converting to refinement types.
   • Example: val x: PositiveInt = userInput.toInt().refine() (checks x > 0 at runtime).

3. Smart-Casting Integration:

   • Use Kotlin’s smart-casting to avoid redundant checks:

   fun process(value: Int) {  
       if (value is PositiveInt) { // Compiler inserts a runtime check here  
           println("Valid: $value") // `value` is now smart-casted to PositiveInt  
       }  
   }  

4. Seamless Interop with Existing Code:

   • Refinement types are erased to their base types at runtime (like typealiases).
   • Works with Java code (no runtime overhead for interop).

5. IDE Support:

   • IntelliJ highlights compile-time violations and suggests runtime checks.

---

Handling Runtime-Dependent Cases:

For values computed at runtime, refinement types would:

1. Insert runtime checks when assigning to a refined type.

2. Propagate constraints through functions using contracts:

   fun square(x: Int): PositiveInt {  
       contract { returns().implies(x != 0) } // Hypothetical contract  
       return (x * x).asRefined()  
   }  

3. Allow opt-out for performance-critical code:

   val unsafe: PositiveInt = compute().uncheckedRefined() // 🔥 No runtime check  

---

Comparison to Value Classes:

Value Classes (Current Kotlin)	Hybrid Refinement Types
Wrap values with validation in init blocks	No wrapper—directly use Int with constraints:
Requires manual wrapping/unwrapping	Automatic coercion: val x: PositiveInt = 5
Runtime overhead for wrapping	Zero overhead (typealias erasure)

Use Cases:

1. APIs with Domain Constraints:

   fun transfer(amount: PositiveDouble, from: NonEmptyAccountId) { ... }  

2. Secure Input Handling:

   val userInput: SanitizedString = rawInput.refined() // Runtime check for XSS  

3. Mathematical Guarantees:

   typealias Probability = Double where this in 0.0..1.0  
   fun validate(p: Probability) { ... }  

4. Stateful Systems:

   typealias ConnectedSocket = Socket where this.isConnected()  
   fun sendData(socket: ConnectedSocket) { ... } // Compiler ensures valid state  

---

Why This Works:

• Pragmatic: Balances compile-time safety with runtime checks.
• Backward-Compatible: Works with existing code and Java interop.
• Reduces Boilerplate: No need for manual require() or wrapper classes.

---

Implementation Strategy:

1. Compiler Plugin:

   • Insert runtime checks during IR generation for assignments to refinement types.
   • Track compile-time constants for static validation.

2. Contracts API Extension:

   • Extend Kotlin’s contracts to support refinement predicates.

3. Reflection for Debugging:

   • Add reflection APIs to inspect refinement constraints at runtime.

---

Conclusion:

While not a full dependent type system, Hybrid Refinement Types would make Kotlin a leader in practical type safety. They address 80% of common validation use cases with minimal overhead, leaving complex proofs to specialized languages like Idris or Lean. This aligns with Kotlin’s philosophy of pragmatic innovation—leveraging the compiler where possible and failing gracefully to runtime checks when necessary. 🚀