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

Sometimes, you want to refine a value that is not available at compile time. For example in the case of form validation.

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.string.*

val runtimeString: String = ???
val username: String :| Alphanumeric = runtimeString

This snippet would not compile because runtimeString is not evaluable at compile time. Fortunately, Iron supports explicit runtime checking using extension methods

Imperative

You can imperatively refine a value at runtime (much like an assertion) using the refine[C] method:

val runtimeString: String = ???
val username: String :| Alphanumeric = runtimeString.refineUnsafe //or more explicitly, refineUnsafe[LowerCase].

The refine extension method tests the constraint at runtime, throwing an IllegalArgumentException if the value does not pass the assertion.

Functional

Iron also provides methods similar to refine but returning an Option (refineOption) or an Either (refineEither), useful for data validation:

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.all.*

case class User(name: String :| Alphanumeric, age: Int :| Greater[0])

def createUser(name: String, age: Int): Either[String, User] =
  for
    n <- name.refineEither[Alphanumeric]
    a <- age.refineEither[Greater[0]]
  yield User(n, a)

createUser("Il_totore", 18) //Left("Should be alphanumeric")
createUser("Iltotore", 0) //Left("Should be greater than 0")
createUser("Iltotore", 18) //Right(User("Iltotore", 18))

Accumulative error

You can accumulate refinement errors using the Cats or ZIO module. Here is an example with the latter:

import zio.prelude.Validation

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.all.*
import io.github.iltotore.iron.zio.*


type Username = Alphanumeric DescribedAs "Username should be alphanumeric"

type Age = Positive DescribedAs "Age should be positive"

case class User(name: String :| Username, age: Int :| Age)

def createUser(name: String, age: Int): Validation[String, User] =
  Validation.validateWith(
    name.refineValidation[Username],
    age.refineValidation[Age]
  )(User.apply)

createUser("Iltotore", 18) //Success(Chunk(),User(Iltotore,18))
createUser("Il_totore", 18) //Failure(Chunk(),NonEmptyChunk(Username should be alphanumeric))
createUser("Il_totore", -18) //Failure(Chunk(),NonEmptyChunk(Username should be alphanumeric, Age should be positive))

This is useful for forms where you want to report all input errors to the user and not short-circuit like an Either.

Check the Cats module or ZIO module page for further information.

Refining further

Sometimes you want to refine the same value multiple times with different constraints. This is especially useful when you want fine-grained refinement errors. Let's take the last example but with passwords:

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.all.*

type Username = DescribedAs[Alphanumeric, "Username should be alphanumeric"]
type Password = DescribedAs[
  Alphanumeric & MinLength[5] & Exists[Letter] & Exists[Digit],
  "Password should have at least 5 characters, be alphanumeric and contain at least one letter and one digit"
]

case class User(name: String :| Username, password: String :| Password)

def createUser(name: String, password: String): Either[String, User] =
  for
    validName     <- name.refineEither[Username]
    validPassword <- password.refineEither[Password]
  yield
    User(validName, validPassword)

createUser("Iltotore", "abc123") //Right(User("Iltotore", "abc123"))
createUser("Iltotore", "abc") //Left("Password should have at least 5 characters, be alphanumeric and contain at least one letter and one digit")

At the last line, we get a Left saying that our password is invalid. However, it's not clear which constraint is not satisfied: is my password to short? Should I add a digit? etc...

Using refineFurther/refineFurtherEither/... enables more detailed messages:

type Username = DescribedAs[Alphanumeric, "Username should be alphanumeric"]
type Password = DescribedAs[
  Alphanumeric & MinLength[5] & Exists[Letter] & Exists[Digit],
  "Password should have at least 5 characters, be alphanumeric and contain at least one letter and one digit"
]

case class User(name: String :| Username, password: String :| Password)

def createUser(name: String, password: String): Either[String, User] =
  for
    validName     <- name.refineEither[Username]
    alphanumeric  <- password.refineEither[Alphanumeric]
    minLength     <- alphanumeric.refineFurtherEither[MinLength[5]]
    hasLetter     <- minLength.refineFurtherEither[Exists[Letter]]
    validPassword <- hasLetter.refineFurtherEither[Exists[Digit]]
  yield
    User(validName, validPassword)

createUser("Iltotore", "abc123") //Right(User("Iltotore", "abc123"))
createUser("Iltotore", "abc1") //Left("Should have a minimum length of 5")
createUser("Iltotore", "abcde") //Left("At least one element: (Should be a digit)")
createUser("Iltotore", "abc123  ") //Left("Should be alphanumeric")

Or with custom error messages:

type Username = DescribedAs[Alphanumeric, "Username should be alphanumeric"]
type Password = DescribedAs[
  Alphanumeric & MinLength[5] & Exists[Letter] & Exists[Digit],
  "Password should have at least 5 characters, be alphanumeric and contain at least one letter and one digit"
]

case class User(name: String :| Username, password: String :| Password)

def createUser(name: String, password: String): Either[String, User] =
  for
    validName     <- name.refineEither[Username]
    alphanumeric  <- password.refineEither[Alphanumeric].left.map(_ => "Your password should be alphanumeric")
    minLength     <- alphanumeric.refineFurtherEither[MinLength[5]].left.map(_ => "Your password should have a minimum length of 5")
    hasLetter     <- minLength.refineFurtherEither[Exists[Letter]].left.map(_ => "Your password should contain at least a letter")
    validPassword <- hasLetter.refineFurtherEither[Exists[Digit]].left.map(_ => "Your password should contain at least a digit")
  yield
    User(validName, validPassword)

createUser("Iltotore", "abc123") //Right(User("Iltotore", "abc123"))
createUser("Iltotore", "abc1") //Left("Your password should have a minimum length of 5")
createUser("Iltotore", "abcde") //Left("Your password should contain at least a digit")
createUser("Iltotore", "abc123  ") //Left("Your password should be alphanumeric")

Note: Accumulative versions exist for Cats and ZIO.

Refining first order types

Iron provides utility methods to easily refine first order types (e.g container types like List, Future, IO...).

List(1, 2, 3).refineAllUnsafe[Positive] //List(1, 2, 3): List[Int :| Positive]
List(1, 2, -3).refineAllUnsafe[Positive] //IllegalArgumentException

Variants exist for Option/Either, assume, ...Further as well as RefinedTypeOps constructors.

Assuming constraints

Sometimes, you know that your value always passes (possibly at runtime) a constraint. For example:

val random = scala.util.Random.nextInt(9)+1
val x: Int :| Positive = random

This code will not compile (see Runtime refinement). We could use refine but we don't actually need to apply the constraint to random. Instead, we can can use assume[C]. It simply acts like a safer cast.

val random = scala.util.Random.nextInt(9)+1
val x: Int :| Positive = random.assume

This code will compile to:

val random: Int = scala.util.Random.nextInt(9)+1
val x: Int = random

leaving no overhead.