refined: simple refinement types for Scala

refined is a Scala library for refining types with type-level predicates which constrain the set of values described by the refined type. It started as a port of the [refined][refined.hs] Haskell library by Nikita Volkov (which also provides an excellent motivation why this kind of library is useful). The idea of expressing constraints at the type-level as Scala library was first explored by Flavio W. Brasil in [bond][bond].

A quick example:

import eu.timepit.refined._
import eu.timepit.refined.api.Refined
import eu.timepit.refined.auto._
import eu.timepit.refined.numeric._

// This refines Int with the Positive predicate and checks via an
// implicit macro that the assigned value satisfies it:
scala> val i1: Int Refined Positive = 5
i1: Int Refined Positive = 5

// If the value does not satisfy the predicate, we get a meaningful
// compile error:
scala> val i2: Int Refined Positive = -5
<console>:22: error: Predicate failed: (-5 > 0).
       val i2: Int Refined Positive = -5
                                       ^

// There is also the explicit refineMV macro that can infer the base
// type from its parameter:
scala> refineMV[Positive](5)
res0: Int Refined Positive = 5

// Macros can only validate literals because their values are known at
// compile-time. To validate arbitrary (runtime) values we can use the
// refineV function:

scala> val x = 42 // suppose the value of x is not known at compile-time

scala> refineV[Positive](x)
res1: Either[String, Int Refined Positive] = Right(42)

scala> refineV[Positive](-x)
res2: Either[String, Int Refined Positive] = Left(Predicate failed: (-42 > 0).)

refined also contains inference rules for converting between different refined types. For example, Int Refined Greater[10] can be safely converted to Int Refined Positive because all integers greater than ten are also positive. The type conversion of refined types is a compile-time operation that is provided by the library:

scala> val a: Int Refined Greater[5] = 10
a: Int Refined Greater[Int(5)] = 10

// Since every value greater than 5 is also greater than 4, `a` can be
// ascribed the type Int Refined Greater[4]:
scala> val b: Int Refined Greater[4] = a
b: Int Refined Greater[Int(4)] = 10

// An unsound ascription leads to a compile error:
scala> val c: Int Refined Greater[6] = a
                                       ^
       error: type mismatch (invalid inference):
               eu.timepit.refined.numeric.Greater[5] does not imply
               eu.timepit.refined.numeric.Greater[6]

This mechanism allows to pass values of more specific types (e.g. Int Refined Greater[10]) to functions that take a more general type (e.g. Int Refined Positive) without manual intervention.

prior Scala 2.13 without literal types

Since there are no literal types prior to Scala 2.13 the literals must be created with shapeless:

scala> val a: Int Refined Greater[W.`5`.T] = 10
a: Int Refined Greater[Int(5)] = 10
scala> val b: Int Refined Greater[W.`4`.T] = a
b: Int Refined Greater[Int(4)] = 10

Note that W is a shortcut for [shapeless.Witness][singleton-types] which provides syntax for [literal-based singleton types][sip-23].

More examples
Using refined
Community
Documentation
Provided predicates
Contributors and participation
Related projects
License

More examples

import eu.timepit.refined._
import eu.timepit.refined.auto._
import eu.timepit.refined.numeric._
import eu.timepit.refined.api.{RefType, Refined}
import eu.timepit.refined.boolean._
import eu.timepit.refined.char._
import eu.timepit.refined.collection._
import eu.timepit.refined.generic._
import eu.timepit.refined.string._
import shapeless.{ ::, HNil }

scala> refineMV[NonEmpty]("Hello")
res2: String Refined NonEmpty = Hello

scala> refineMV[NonEmpty]("")
<console>:39: error: Predicate isEmpty() did not fail.
            refineMV[NonEmpty]("")
                              ^

scala> type ZeroToOne = Not[Less[0.0]] And Not[Greater[1.0]]
defined type alias ZeroToOne

scala> refineMV[ZeroToOne](1.8)
<console>:40: error: Right predicate of (!(1.8 < 0.0) && !(1.8 > 1.0)) failed: Predicate (1.8 > 1.0) did not fail.
       refineMV[ZeroToOne](1.8)
                          ^

scala> refineMV[AnyOf[Digit :: Letter :: Whitespace :: HNil]]('F')
res3: Char Refined AnyOf[Digit :: Letter :: Whitespace :: HNil] = F

scala> refineMV[MatchesRegex["[0-9]+"]]("123.")
<console>:39: error: Predicate failed: "123.".matches("[0-9]+").
              refineMV[MatchesRegex[W.`"[0-9]+"`.T]]("123.")
                                                    ^

scala> val d1: Char Refined Equal['3'] = '3'
d1: Char Refined Equal[Char('3')] = 3

scala> val d2: Char Refined Digit = d1
d2: Char Refined Digit = 3

scala> val d3: Char Refined Letter = d1
<console>:39: error: type mismatch (invalid inference):
 Equal[Char('3')] does not imply
 Letter
       val d3: Char Refined Letter = d1
                                     ^

scala> val r1: String Refined Regex = "(a|b)"
r1: String Refined Regex = (a|b)

scala> val r2: String Refined Regex = "(a|b"
<console>:38: error: Regex predicate failed: Unclosed group near index 4
(a|b
    ^
       val r2: String Refined Regex = "(a|b"
                                      ^

scala> val u1: String Refined Url = "htp://example.com"
<console>:38: error: Url predicate failed: unknown protocol: htp
       val u1: String Refined Url = "htp://example.com"
                                    ^

// Here we define a refined type "Int with the predicate (7 <= value < 77)".
scala> type Age = Int Refined Interval.ClosedOpen[7, 77]

scala> val userInput = 55

// We can refine values with this refined type by either using `refineV`
// with an explicit return type
scala> val ageEither1: Either[String, Age] = refineV(userInput)
ageEither1: Either[String,Age] = Right(55)

// or by using `RefType.applyRef` with the refined type as type parameter.
scala> val ageEither2 = RefType.applyRef[Age](userInput)
ageEither2: Either[String,Age] = Right(55)

Using refined

The latest version of the library is 0.11.3, which is available for Scala and [Scala.js][scala.js] version 2.12 and 2.13.

If you're using sbt, add the following to your build:

libraryDependencies ++= Seq(
  "eu.timepit" %% "refined"                 % "0.11.3",
  "eu.timepit" %% "refined-cats"            % "0.11.3", // optional
  "eu.timepit" %% "refined-eval"            % "0.11.3", // optional, JVM-only
  "eu.timepit" %% "refined-jsonpath"        % "0.11.3", // optional, JVM-only
  "eu.timepit" %% "refined-pureconfig"      % "0.11.3", // optional, JVM-only
  "eu.timepit" %% "refined-scalacheck"      % "0.11.3", // optional
  "eu.timepit" %% "refined-scalaz"          % "0.11.3", // optional
  "eu.timepit" %% "refined-scodec"          % "0.11.3", // optional
  "eu.timepit" %% "refined-scopt"           % "0.11.3", // optional
  "eu.timepit" %% "refined-shapeless"       % "0.11.3"  // optional
)

For Scala.js just replace %% with %%% above.

Instructions for Maven and other build tools are available at [search.maven.org][search.maven].

Release notes for the latest version are here.

Community

Internal modules

The project provides these optional extensions and library integrations:

refined-cats provides Cats type class instances for refined types
refined-eval provides the Eval[S] predicate that checks if a value applied to the predicate S yields true
refined-jsonpath provides the JSONPath predicate that checks if a String is a valid JSONPath
refined-pureconfig allows to read configuration with refined types using PureConfig
refined-scalacheck allows to generate arbitrary values of refined types with ScalaCheck. Use refined-scalacheck_1.13 instead if your other dependencies use scalacheck version 1.13
refined-scalaz provides Scalaz type class instances for refined types and support for scalaz.@@
refined-scodec allows binary decoding and encoding of refined types with scodec and allows refining scodec.bits.ByteVector
refined-scopt allows to read command line options with refined types using scopt
refined-shapeless

External modules

Below is an incomplete list of third-party extensions and library integrations for refined. If your library is missing, please open a pull request to list it here:

[api-refiner](https://github.com/dgouyette/play-api-refi

Refined

Install / Use

README