A proof of concept of a simple encoding of refinement types in Scala 3.
You can read about motivation behind and the main concepts in the blog post.
Include library in build.sbt
:
libraryDependencies += "pl.msitko" %% "mini-refined" % "0.2.0"
Common imports:
import pl.msitko.refined.auto._
import pl.msitko.refined.Refined
To use circe integration:
libraryDependencies += "pl.msitko" %% "mini-refined-circe" % "0.2.0"
val a: Int Refined GreaterThan[10] = 5
// fails compilation with: Validation failed: 5 > 10
val a: Int Refined LowerThan[10] = 15
// fails compilation with: Validation failed: 15 < 10
val s: String Refined StartsWith["xyz"] = "abc"
// fails compilation with: Validation failed: abc.startsWith(xyz)
val s: String Refined EndsWith["xyz"] = "abc"
// fails compilation with: Validation failed: abc.endsWith(xyz)
val as: List[String] Refined Size[GreaterThan[1]] = List("a")
// fails compilation with:
// Validation failed: list size doesn't hold predicate: 1 > 1
You can use any Int
predicates within Size
predicate.
You can compose predicates with boolean operators. For example:
val c: Int Refined And[GreaterThan[10], LowerThan[20]] = 25
// fails compilation with: Validation failed: (25 > 10 And 25 < 20), predicate failed: 25 < 20
Everything described so far works only for values known at a compile-time. However, values for most variables are coming
at runtime. For those you need to use Refined.refineV[T]
which returns Either[String, T]
. Example:
case class Example(a: Int, b: Int Refined GreaterThan[10])
def runtime(a: Int, b: Int): Either[String, Example] =
Refined.refineV[GreaterThan[10]](b).map(refined => Example(a, refined))
mini-refined
has some basic rules that enable using more specific types in places where more general types are required.
In other words, considering such function:
def intFun10(a: Int Refined GreaterThan[10]): Unit = ???
We can call it with a value of type Int Refined GreaterThan[20]
, as mini-refined
recognizes that being greater than 20 implies being greater than 10.