Refinement Methods
Iron provides multiple ways at compile time or runtime to refine a type depending on the use case.
Automatic refinement
Unconstrained values are automatically cast to their refined form if they satisfy the constraint at compile time:
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.*
val x: Int :| Greater[0] = 5
If they don't, a compile-time error is thrown:
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.*
val y: Int :| Greater[0] = -1
-- Constraint Error --------------------------------------------------------
Could not satisfy a constraint for type scala.Int.
Value: -1
Message: Should be strictly greater than 0
----------------------------------------------------------------------------
If the value (or the constraint itself) cannot be evaluated at compile time, then the compilation also fails:
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.*
val runtimeValue: Int = ???
val x: Int :| Greater[0] = runtimeValue
-- Constraint Error --------------------------------------------------------
Cannot refine non full inlined input at compile-time.
To test a constraint at runtime, use the `refine` extension method.
Note: Due to a Scala limitation, already-refined types cannot be tested at compile-time (unless proven by an `Implication`).
Inlined input: runtimeValue
----------------------------------------------------------------------------
Iron uses to determine if a value is evaluable at compile time the Scala typeclass FromExpr. By default, all fully inlined literals (including AnyVals, String, Option and Either) are evaluable at compile-time. Note that the constraint condition also needs to be fully inlined.
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.*
inline val value = 2
val x: Int :| Greater[0] = value //OK
Runtime refinement
In this article