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.

1. More examples
2. Using refined
3. Community
4. Documentation
5. Provided predicates
6. Contributors and participation
7. Related projects
8. License

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:https://example.com"
<console>:38: error: Url predicate failed: unknown protocol: htp
       val u1: String Refined Url = "htp:https://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 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

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
• argonaut-refined
• atto-refined
• case-app-refined
• circe-refined
• ciris-refined
• cormorant-refined
• coulomb-refined
• decline-refined
• doobie-refined
• exercises-refined
• extruder-refined
• finch-refined
• formulation-refined
• kantan.csv-refined
• kantan.regex-refined
• kantan.xpath-refined
• monocle-refined
• neotypes-refined
• play-refined
• play-json-refined
• play-json-refined
• refined-anorm
• refined-guava
• scanamo-refined
• seals-refined
• slick-refined
• spray-json-refined
• strictify-refined
• validated-config
• vulcan-refined
• xml-names-core

If your open source project is using refined, please consider opening a pull request to list it here:

• calypso: BSON library for Scala
• Quasar: An open source NoSQL analytics engine which uses refined for natural and positive integer types
• rvi_sota_server: The SOTA Server Reference Implementation uses refined for domain specific types. like the vehicle identification number (VIN).

Are you using refined in your organization or company? Please consider opening a pull request to list it here:

• PITS Global Data Recovery Services
• AutoScout24
• Besedo
• Chatroulette
• Colisweb
• FOLIO
• HolidayCheck
• Zalando
• ContentSquare
• Dassault Systèmes
• Hypefactors

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:

boolean

• 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

char

• Digit: checks if a Char is a digit
• Letter: checks if a Char is a letter
• LetterOrDigit: checks if a Char is a letter or digit
• LowerCase: checks if a Char is a lower case character
• UpperCase: checks if a Char is an upper case character
• Whitespace: checks if a Char is white space

collection

• Contains[U]: checks if an Iterable contains a value equal to U
• Count[PA, PC]: counts the number of elements in an Iterable which satisfy the predicate PA and passes the result to the predicate PC
• Empty: checks if an Iterable is empty
• NonEmpty: checks if an Iterable is not empty
• Forall[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 sequence
• Init[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

generic

• Equal[U]: checks if a value is equal to U

numeric

• 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 zero
• NonPositive: checks if a numeric value is zero or negative
• Negative: checks if a numeric value is less than zero
• NonNegative: checks if a numeric value is zero or positive
• Interval.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 2
• Odd: checks if an integral value is not evenly divisible by 2
• NonNaN: checks if a floating-point number is not NaN

string

• EndsWith[S]: checks if a String ends with the suffix S
• IPv4: checks if a String is a valid IPv4
• IPv6: checks if a String is a valid IPv6
• MatchesRegex[S]: checks if a String matches the regular expression S
• Regex: checks if a String is a valid regular expression
• StartsWith[S]: checks if a String starts with the prefix S
• Uri: checks if a String is a valid URI
• Url: checks if a String is a valid URL
• Uuid: checks if a String is a valid UUID
• ValidByte: 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 XML
• XPath: checks if a String is a valid XPath expression
• Trimmed: checks if a String has no leading or trailing whitespace
• HexStringSpec: checks if a String represents a hexadecimal number

The following people have helped making refined great:

• Alex
• Alexandre Archambault
• Arman Bilge
• Brian P. Holt
• Chris Birchall
• Chris Hodapp
• Cody Allen
• Dale Wijnand
• Denys Shabalin
• Derek Morr
• Didac
• Diogo Castro
• dm-tran
• Ender Tunç
• Frank S. Thomas
• Frederick Roth
• Howard Perrin
• Iurii Susuk
• Ivan Klass
• Jean-Rémi Desjardins
• Jente Hidskes
• Joe Greene
• John-Michael Reed
• Julien BENOIT
• kalejami
• kenji yoshida
• kusamakura
• 急須
• Leif Wickland
• Luis Miguel Mejía Suárez
• Mateusz Wójcik
• Matt Pickering
• Matthieu Jacquot
• Michael Thomas
• Michal Sitko
• Naoki Aoyama
• Nicolas Rinaudo
• Olli Helenius
• Richard Gomes
• ronanM
• Sam Guymer
• Sam Halliday
• Shawn Garner
• Shohei Shimomura
• Shunsuke Otani
• Tim Steinbach
• Torsten Scholak
• Viktor Lövgren
• Vladimir Koshelev
• Yuki Ishikawa
• Zainab Ali
• Your name here :-)

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.

• SMT-Based Checking of Predicate-Qualified Types for Scala
• bond: Type-level validation for Scala
• F7: Refinement Types for F#
• LiquidHaskell: Refinement Types via SMT and Predicate Abstraction
• Refinement Types in Typed Racket
• refined: Refinement types with static and runtime checking for Haskell. refined was inspired by this library and even stole its name!
• refscript: Refinement Types for TypeScript
• Subtypes in Perl 6

refined is licensed under the MIT license, available at https://opensource.org/licenses/MIT and also in the LICENSE file.