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.4, 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.4",
"eu.timepit" %% "refined-cats" % "0.11.4", // optional
"eu.timepit" %% "refined-eval" % "0.11.4", // optional, JVM-only
"eu.timepit" %% "refined-jsonpath" % "0.11.4", // optional, JVM-only
"eu.timepit" %% "refined-pureconfig" % "0.11.4", // optional, JVM-only
"eu.timepit" %% "refined-scalacheck" % "0.11.4", // optional
"eu.timepit" %% "refined-scalaz" % "0.11.4", // optional
"eu.timepit" %% "refined-scodec" % "0.11.4", // optional
"eu.timepit" %% "refined-scopt" % "0.11.4", // optional
"eu.timepit" %% "refined-shapeless" % "0.11.4" // 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 Cats
type class instances for refined typesrefined-eval provides the Eval[S] predicate that checks if a value
applied to the predicate S yields truerefined-jsonpath provides the JSONPath predicate that checks if a
String is a valid JSONPathrefined-pureconfig allows to read configuration with refined types
using PureConfigrefined-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.13refined-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.ByteVectorrefined-scopt allows to read command line options with refined types
using scoptrefined-shapelessBelow 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.4/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 trueFalse: constant predicate that is always falseNot[P]: negation of the predicate PAnd[A, B]: conjunction of the predicates A and BOr[A, B]: disjunction of the predicates A and BXor[A, B]: exclusive disjunction of the predicates A and BNand[A, B]: negated conjunction of the predicates A and BNor[A, B]: negated disjunction of the predicates A and BAllOf[PS]: conjunction of all predicates in PSAnyOf[PS]: disjunction of all predicates in PSOneOf[PS]: exclusive disjunction of all predicates in PSDigit: 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 UCount[PA, PC]: counts the number of elements in an Iterable which satisfy the
predicate PA and passes the result to the predicate PCEmpty: 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 IterableExists[P]: checks if the predicate P holds for some elements of an IterableHead[P]: checks if the predicate P holds for the first element of an IterableIndex[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 IterableLast[P]: checks if the predicate P holds for the last element of an IterableTail[P]: checks if the predicate P holds for all but the first element of an IterableSize[P]: checks if the size of an Iterable satisfies the predicate PMinSize[N]: checks if the size of an Iterable is greater than or equal to NMaxSize[N]: checks if the size of an Iterable is less than or equal to NEqual[U]: checks if a value is equal to ULess[N]: checks if a numeric value is less than NLessEqual[N]: checks if a numeric value is less than or equal to NGreater[N]: checks if a numeric value is greater than NGreaterEqual[N]: checks if a numeric value is greater than or equal to NPositive: 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 ODivisible[N]: checks if an integral value is evenly divisible by NNonDivisible[N]: checks if an integral value is not evenly divisible by NEven: 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 SIPv4: 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 SRegex: checks if a String is a valid regular expressionStartsWith[S]: checks if a String starts with the prefix SUri: 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 ByteValidShort: checks if a String is a parsable ShortValidInt: checks if a String is a parsable IntValidLong: checks if a String is a parsable LongValidFloat: checks if a String is a parsable FloatValidDouble: checks if a String is a parsable DoubleValidBigInt: checks if a String is a parsable BigIntValidBigDecimal: checks if a String is a parsable BigDecimalXml: 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.
(top 24 of 36)
1,608 followers · starred Aug 2020
1,001 followers · starred Oct 2016
671 followers · starred May 2015
207 followers · starred Jul 2015
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.4, 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.4",
"eu.timepit" %% "refined-cats" % "0.11.4", // optional
"eu.timepit" %% "refined-eval" % "0.11.4", // optional, JVM-only
"eu.timepit" %% "refined-jsonpath" % "0.11.4", // optional, JVM-only
"eu.timepit" %% "refined-pureconfig" % "0.11.4", // optional, JVM-only
"eu.timepit" %% "refined-scalacheck" % "0.11.4", // optional
"eu.timepit" %% "refined-scalaz" % "0.11.4", // optional
"eu.timepit" %% "refined-scodec" % "0.11.4", // optional
"eu.timepit" %% "refined-scopt" % "0.11.4", // optional
"eu.timepit" %% "refined-shapeless" % "0.11.4" // 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 Cats
type class instances for refined typesrefined-eval provides the Eval[S] predicate that checks if a value
applied to the predicate S yields truerefined-jsonpath provides the JSONPath predicate that checks if a
String is a valid JSONPathrefined-pureconfig allows to read configuration with refined types
using PureConfigrefined-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.13refined-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.ByteVectorrefined-scopt allows to read command line options with refined types
using scoptrefined-shapelessBelow 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.4/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 trueFalse: constant predicate that is always falseNot[P]: negation of the predicate PAnd[A, B]: conjunction of the predicates A and BOr[A, B]: disjunction of the predicates A and BXor[A, B]: exclusive disjunction of the predicates A and BNand[A, B]: negated conjunction of the predicates A and BNor[A, B]: negated disjunction of the predicates A and BAllOf[PS]: conjunction of all predicates in PSAnyOf[PS]: disjunction of all predicates in PSOneOf[PS]: exclusive disjunction of all predicates in PSDigit: 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 UCount[PA, PC]: counts the number of elements in an Iterable which satisfy the
predicate PA and passes the result to the predicate PCEmpty: 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 IterableExists[P]: checks if the predicate P holds for some elements of an IterableHead[P]: checks if the predicate P holds for the first element of an IterableIndex[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 IterableLast[P]: checks if the predicate P holds for the last element of an IterableTail[P]: checks if the predicate P holds for all but the first element of an IterableSize[P]: checks if the size of an Iterable satisfies the predicate PMinSize[N]: checks if the size of an Iterable is greater than or equal to NMaxSize[N]: checks if the size of an Iterable is less than or equal to NEqual[U]: checks if a value is equal to ULess[N]: checks if a numeric value is less than NLessEqual[N]: checks if a numeric value is less than or equal to NGreater[N]: checks if a numeric value is greater than NGreaterEqual[N]: checks if a numeric value is greater than or equal to NPositive: 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 ODivisible[N]: checks if an integral value is evenly divisible by NNonDivisible[N]: checks if an integral value is not evenly divisible by NEven: 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 SIPv4: 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 SRegex: checks if a String is a valid regular expressionStartsWith[S]: checks if a String starts with the prefix SUri: 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 ByteValidShort: checks if a String is a parsable ShortValidInt: checks if a String is a parsable IntValidLong: checks if a String is a parsable LongValidFloat: checks if a String is a parsable FloatValidDouble: checks if a String is a parsable DoubleValidBigInt: checks if a String is a parsable BigIntValidBigDecimal: checks if a String is a parsable BigDecimalXml: 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.
(top 24 of 36)
1,608 followers · starred Aug 2020
1,001 followers · starred Oct 2016
671 followers · starred May 2015
207 followers · starred Jul 2015