Constraint Creation

This page details all steps to create a type constraint.

Overview

A type constraint consists of two parts:

• Dummy: the shallow/API part of your constraint
• Behaviour: the internal behaviour of your constraint

Basic constraint creation

Dummy

A dummy can be anything passable as a generic type. Iron's defaults use traits for dummies.

The dummy can contain information like values through singleton types.

Example:

import io.github.iltotore.numeric.Number

trait Greater[V <: Number] //A V singleton type is required

Note: Number is an alias for the union of all numerical primitives.

Behaviour

We need to attach a behaviour to our dummy. A constraint behaviour is a given instance of Constraint[A, B] where A is the input type and B the dummy.

Without parameter

For constraints without parameters, we can just use create an anonymous given:

import io.github.iltotore.numeric.Number
import scala.compiletime.constValue

trait Dummy

inline given Constraint[Boolean, Dummy] with {
  override inline def assert(value: Boolean): Boolean = value
}

With parameters

If our constraint is runtime-only, you can use the same method as above.

Due to Dotty's nested inlines limitation, we need to create a class for compile-time constraints with parameters:

import io.github.iltotore.numeric.Number
import scala.compiletime.constValue

trait Greater[V <: Number]

class GreaterConstraint[A <: Number, V <: A] extends Constraint[A, Greater[V]] {
  override inline
  
  def assert(value: A): Boolean = NumberOrdering.gt(value, constValue[V])
}

Note: NumberOrdering is an instance of InlineOrdering for Number. It offers the same features as a normal Ordering but inline.

Now, we need to create a given method returning an instance of our constraint:

inline given[A <: Number, V <: A]: GreaterConstraint[A, V] = new GreaterConstraint

You can now use your constraint:

inline def log(x: Double / Greater[0d]): Refined[Double] = x.map(Math.log)

Note: here, the log method is inline to reduce overhead (log(x) will desugar to Right(x).map(Math.log)).

Constraint aliases

You can use Scala's type aliases to alias constraints. This can be useful for special cases or readability.

Example using the Greater constraint:

type >[A, V] = A / Greater[V]

Usage:

inline def log(x: Double > 0d): Refined[Double] = x.map(Math.log)

//Desugars to
inline def log(x: Double / Greater[0d]): Refined[Double] = x.map(Math.log)

Custom description

You can attach a description to a custom constraint alias using the DescribedAs[B, V] type:

type Email = String / (Match["^[\\w-\\.]+@([\\w-]+\\.)+[\\w-]{2,4}$"] DescribedAs "Value should be an email")

Note: you can only use string literals in DescribedAs message.

Advanced features

Algebraic constraints

You can create constraints that belong to a special algebra to allow creation of complex constraint equations.

To avoid conflict, algebraic constraints have a special algebra type, for example the trait MathAlgebra.

Entry point

An algebraic entry point is a starting point of an algebraic equation. Its right value is always the input value of the equation (= the input of this Constrained).

def foo(x: Double / (-1d < ?? < 1d)): Unit = ???

In this example, -1d < ?? is an entry point.

You can create an algebraic entry point by making its dummy extending AlgebraEntryPoint[T]:

trait Less[V] extends AlgebraEntryPoint[MathAlgebra]

Example taken from the numeric module.

Middle part

An algebra part is part of the algebraic equation containing an algebra type (to avoid conflict with other algebras) and a right value.

Here is an example taken from the core of Iron:

trait Placehold[B, Alg, V] extends AlgebraPart[Alg, V]

Binary operators

An algebraic binary operator allows chaining with other binary operators of the same algebra. Iron provides a type alias to ease their creation:

type <[A, B] = BiOperator[A, B, MathAlgebra, Number, Less, Greater]

The parameters details are available on the Scaladoc.

Further information about algebraic constraints usage here