Iron Refined Types for Scala 3

Iron is a lightweight library for Scala 3 that enables attaching constraints or assertions to types. This allows you to enforce specific properties and forbid invalid values at both compile-time and runtime.

Key features:

• Catch bugs: Use specific types to avoid invalid values via static typing.
• Compile-time and runtime: Evaluate constraints during compilation or explicitly check them at runtime (e.g., for user input).
• Seamless integration: Iron types are subtypes of their unrefined versions, allowing for easy conversion.
• Extendable: Create custom constraints using standard typeclasses.
• No black magic: Built using Scala 3's inline, types, and restricted macros for predictable behavior.

Implication is a compile-time mechanism that allows casting from one refined type to another. It is analogous to logical implication and is represented by Implication[C1, C2] or its type alias C1 ==> C2 (read as "C1 implies C2").

This mechanism allows you to treat a value with a stricter constraint as a value with a weaker constraint. For example, if a value is known to be Greater[5], it can be safely cast to Greater[0] because Greater[5] implies Greater[0] via transitivity.

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Greater

val x: Int :| Greater[5] = ???
val y: Int :| Greater[0] = x // Compiles because Greater[5] ==> Greater[0]

You can compose existing constraints using type-level operators that act as boolean logic.

• Union (|): Acts as a boolean OR. A value is valid if it satisfies either constraint.
• Intersection (&): Acts as a boolean AND. A value must satisfy both constraints.

Example: Creating a GreaterEqual[V] constraint by unioning Greater[V] and StrictEqual[V].

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

type GreaterEqual[V] = Greater[V] | StrictEqual[V]

type Between[Min, Max] = GreaterEqual[Min] & LessEqual[Max]

The iron-scodec module implements integration via two primary mechanisms:

1. Newtypes: It utilizes RefinedType.Mirror to provide codecs for newtype definitions.
2. Refined Types: It leverages the codec of the underlying base type and applies the refinement constraint validation during the decoding phase.

This integration is designed to work seamlessly with Scodec's native derivation mechanisms for case classes and sealed traits.

Iron is built around three fundamental concepts used to define and enforce type safety:

• Iron Type: A type that is constrained by one or more rules.
• Constraint: A specific rule or condition that a value must satisfy to be considered a valid Iron Type.
• Implication: A logical relationship where one constraint implies another (e.g., if a value satisfies constraint A, it must also satisfy constraint B).

Iron is a type constraints (or "refined types") library for Scala. It allows you to bind specific constraints to a type, a process called "type refinement".

While standard Scala static typing prevents passing the wrong type (e.g., passing a String where an Int is expected), it cannot prevent logically invalid values (e.g., passing a negative number for an age). Refined types solve this by ensuring constraints are checked at compile time or explicitly at runtime, preventing invalid data from propagating through your application.

If a value and its constraint are both fully inlined and evaluable at compile time, Iron automatically casts the unconstrained value to its refined form. If the constraint is not satisfied, a compile-time error is thrown. Note that if the value or constraint cannot be evaluated at compile time (e.g., a runtime variable), compilation will fail with a Constraint Error stating that you must use runtime refinement methods instead.

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

// OK: 5 satisfies Greater[0] at compile time
val x: Int :| Greater[0] = 5

// Compile Error: -1 does not satisfy Greater[0]
// val y: Int :| Greater[0] = -1

// Compile Error: runtimeValue is not evaluable at compile time
// val runtimeValue: Int = ???
// val x: Int :| Greater[0] = runtimeValue

Iron new types are opaque. This means they are only known as their specific type within the file where they are defined. Outside that file, they are treated as their underlying IronType (the base type plus the constraint), not as the new type itself.

Benefits

1. Prevents accidental mixing: You cannot pass a Moisture type into a function expecting a Temperature type, even if both are Double :| Positive.
2. Forces explicit conversion: You cannot assign a raw Double :| Positive to a Temperature type directly; you must use a smart constructor like Temperature(value).

Limitations

Because of opacity, you cannot treat the new type as a simple type alias in other modules. You must interact with it via its defined interface.

Once the iron-scalacheck dependency is added, all Iron refined types are compatible with ScalaCheck via Arbitrary instances.

• Fallback instances: Every refined type has a default Arbitrary instance provided by the module.
• Custom instances: Certain constraints include optimized custom Arbitrary instances. These are designed to be faster and more efficient at generating valid values, helping to prevent test exhaustion (where the generator struggles to find values that satisfy the refinement).

While Constraint is used for compile-time refinement, RuntimeConstraint is a proxy designed for runtime usage.

When to use RuntimeConstraint:

• When the calling method does not need to be inline.
• To reduce generated bytecode size and improve performance.
• When deriving typeclasses (e.g., FromString) to avoid warnings about large generated code from inline given aliases.
• When you need to reuse the same constraint instance at runtime.

RuntimeConstraint provides the same test and message interface as Constraint.

// Example of using RuntimeConstraint in a refinement function
def refineOption[A, C](value: A)(using constraint: RuntimeConstraint[A, C]): Option[A :| C] =
  Option.when(constraint.test(value))(value.asInstanceOf[A :| C])

refineOption[Int, Positive](5) // Some(5)
refineOption[Int, Positive](-5) // None