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 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.
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.
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
which provides
syntax for literal-based singleton types.
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)
The latest version of the library is 0.11.2, which is available for Scala and 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.2",
"eu.timepit" %% "refined-cats" % "0.11.2", // optional
"eu.timepit" %% "refined-eval" % "0.11.2", // optional, JVM-only
"eu.timepit" %% "refined-jsonpath" % "0.11.2", // optional, JVM-only
"eu.timepit" %% "refined-pureconfig" % "0.11.2", // optional, JVM-only
"eu.timepit" %% "refined-scalacheck" % "0.11.2", // optional
"eu.timepit" %% "refined-scalaz" % "0.11.2", // optional
"eu.timepit" %% "refined-scodec" % "0.11.2", // optional
"eu.timepit" %% "refined-scopt" % "0.11.2", // optional
"eu.timepit" %% "refined-shapeless" % "0.11.2" // optional
)
For Scala.js just replace %%
with %%%
above.
Instructions for Maven and other build tools are available at search.maven.org.
Release notes for the latest version are here.
The project provides these optional extensions and library integrations:
refined-cats
provides Catsrefined-eval
provides the Eval[S]
predicate that checks if a valueS
yields true
refined-jsonpath
provides the JSONPath
predicate that checks if aString
is a valid JSONPath
refined-pureconfig
allows to read configuration with refined typesrefined-scalacheck
allows to generate arbitrary values of refined typesrefined-scalacheck_1.13
instead if your other dependenciesrefined-scalaz
provides Scalazscalaz.@@
refined-scodec
allows binary decoding and encoding of refined types withscodec.bits.ByteVector
refined-scopt
allows to read command line options with refined typesrefined-shapeless
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:
If your open source project is using refined, please consider opening a pull request to list it here:
Are you using refined in your organization or company? Please consider opening a pull request to list it here:
API documentation of the latest release is available at: https://static.javadoc.io/eu.timepit/refined_2.12/0.11.2/eu/timepit/refined/index.html
There are further (type-checked) examples in the docs
directory including ones for defining custom predicates
and working with type aliases. It also contains a
description of refined's design and internals.
Talks and other external resources are listed on the Resources page in the wiki.
The library comes with these predefined predicates:
True
: constant predicate that is always true
False
: constant predicate that is always false
Not[P]
: negation of the predicate P
And[A, B]
: conjunction of the predicates A
and B
Or[A, B]
: disjunction of the predicates A
and B
Xor[A, B]
: exclusive disjunction of the predicates A
and B
Nand[A, B]
: negated conjunction of the predicates A
and B
Nor[A, B]
: negated disjunction of the predicates A
and B
AllOf[PS]
: conjunction of all predicates in PS
AnyOf[PS]
: disjunction of all predicates in PS
OneOf[PS]
: exclusive disjunction of all predicates in PS
Digit
: checks if a Char
is a digitLetter
: checks if a Char
is a letterLetterOrDigit
: checks if a Char
is a letter or digitLowerCase
: checks if a Char
is a lower case characterUpperCase
: checks if a Char
is an upper case characterWhitespace
: checks if a Char
is white spaceContains[U]
: checks if an Iterable
contains a value equal to U
Count[PA, PC]
: counts the number of elements in an Iterable
which satisfy thePA
and passes the result to the predicate PC
Empty
: checks if an Iterable
is emptyNonEmpty
: checks if an Iterable
is not emptyForall[P]
: checks if the predicate P
holds for all elements of an Iterable
Exists[P]
: checks if the predicate P
holds for some elements of an Iterable
Head[P]
: checks if the predicate P
holds for the first element of an Iterable
Index[N, P]
: checks if the predicate P
holds for the element at index N
of a sequenceInit[P]
: checks if the predicate P
holds for all but the last element of an Iterable
Last[P]
: checks if the predicate P
holds for the last element of an Iterable
Tail[P]
: checks if the predicate P
holds for all but the first element of an Iterable
Size[P]
: checks if the size of an Iterable
satisfies the predicate P
MinSize[N]
: checks if the size of an Iterable
is greater than or equal to N
MaxSize[N]
: checks if the size of an Iterable
is less than or equal to N
Equal[U]
: checks if a value is equal to U
Less[N]
: checks if a numeric value is less than N
LessEqual[N]
: checks if a numeric value is less than or equal to N
Greater[N]
: checks if a numeric value is greater than N
GreaterEqual[N]
: checks if a numeric value is greater than or equal to N
Positive
: checks if a numeric value is greater than zeroNonPositive
: checks if a numeric value is zero or negativeNegative
: checks if a numeric value is less than zeroNonNegative
: checks if a numeric value is zero or positiveInterval.Open[L, H]
: checks if a numeric value is in the interval (L
, H
)Interval.OpenClosed[L, H]
: checks if a numeric value is in the interval (L
, H
]Interval.ClosedOpen[L, H]
: checks if a numeric value is in the interval [L
, H
)Interval.Closed[L, H]
: checks if a numeric value is in the interval [L
, H
]Modulo[N, O]
: checks if an integral value modulo N
is O
Divisible[N]
: checks if an integral value is evenly divisible by N
NonDivisible[N]
: checks if an integral value is not evenly divisible by N
Even
: checks if an integral value is evenly divisible by 2Odd
: checks if an integral value is not evenly divisible by 2NonNaN
: checks if a floating-point number is not NaNEndsWith[S]
: checks if a String
ends with the suffix S
IPv4
: checks if a String
is a valid IPv4IPv6
: checks if a String
is a valid IPv6MatchesRegex[S]
: checks if a String
matches the regular expression S
Regex
: checks if a String
is a valid regular expressionStartsWith[S]
: checks if a String
starts with the prefix S
Uri
: checks if a String
is a valid URIUrl
: checks if a String
is a valid URLUuid
: checks if a String
is a valid UUIDValidByte
: checks if a String
is a parsable Byte
ValidShort
: checks if a String
is a parsable Short
ValidInt
: checks if a String
is a parsable Int
ValidLong
: checks if a String
is a parsable Long
ValidFloat
: checks if a String
is a parsable Float
ValidDouble
: checks if a String
is a parsable Double
ValidBigInt
: checks if a String
is a parsable BigInt
ValidBigDecimal
: checks if a String
is a parsable BigDecimal
Xml
: checks if a String
is well-formed XMLXPath
: checks if a String
is a valid XPath expressionTrimmed
: checks if a String
has no leading or trailing whitespaceHexStringSpec
: checks if a String
represents a hexadecimal numberThe following people have helped making refined great:
refined is a Typelevel project. This means we embrace pure, typeful, functional programming, and provide a safe and friendly environment for teaching, learning, and contributing as described in the Scala Code of Conduct.
refined is licensed under the MIT license, available at http://opensource.org/licenses/MIT and also in the LICENSE file.