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 (which also provides an excellent motivation why this kind of library is useful).
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[W.`10`.T]
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[W.`5`.T] = 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[W.`4`.T]:
scala> val b: Int Refined Greater[W.`4`.T] = a
b: Int Refined Greater[Int(4)] = 10
// An unsound ascription leads to a compile error:
scala> val c: Int Refined Greater[W.`6`.T] = a
<console>:23: error: type mismatch (invalid inference):
Greater[Int(5)] does not imply
Greater[Int(6)]
val c: Int Refined Greater[W.`6`.T] = a
^
This mechanism allows to pass values of more specific types (e.g.
Int Refined Greater[W.`10`.T]
) to functions that take a more general
type (e.g. Int Refined Positive
) without manual intervention.
Note that W
is a shortcut for shapeless.Witness
which provides
syntax for literal-based singleton types.
- More examples
- Using refined
- Documentation
- Provided predicates
- Contributors and participation
- Projects using refined
- Performance concerns
- Related projects
- License
import eu.timepit.refined.api.RefType
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[W.`0.0`.T]] And Not[Greater[W.`1.0`.T]]
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[W.`"[0-9]+"`.T]]("123.")
<console>:39: error: Predicate failed: "123.".matches("[0-9]+").
refineMV[MatchesRegex[W.`"[0-9]+"`.T]]("123.")
^
scala> val d1: Char Refined Equal[W.`'3'`.T] = '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[W.`7`.T, W.`77`.T]
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.8.7, which is available for Scala and Scala.js version 2.10, 2.11, and 2.12.
If you're using sbt, add the following to your build:
libraryDependencies ++= Seq(
"eu.timepit" %% "refined" % "0.8.7",
"eu.timepit" %% "refined-cats" % "0.8.7", // optional
"eu.timepit" %% "refined-eval" % "0.8.7", // optional, JVM-only
"eu.timepit" %% "refined-jsonpath" % "0.8.7", // optional, JVM-only
"eu.timepit" %% "refined-pureconfig" % "0.8.7", // optional, JVM-only
"eu.timepit" %% "refined-scalacheck" % "0.8.7", // optional
"eu.timepit" %% "refined-scalaz" % "0.8.7", // optional
"eu.timepit" %% "refined-scodec" % "0.8.7" // 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 available in 0.8.7.markdown.
The project provides these optional extensions and library integrations:
refined-cats
provides Cats type class instances for refined typesrefined-eval
provides theEval[S]
predicate that checks if a value applied to the predicateS
yieldstrue
refined-jsonpath
provides theJSONPath
predicate that checks if aString
is a valid JSONPathrefined-pureconfig
allows to read configuration with refined types using PureConfigrefined-scalacheck
allows to generate arbitrary values of refined types with ScalaCheckrefined-scalaz
provides Scalaz type class instances for refined types and support forscalaz.@@
refined-scodec
allows binary decoding and encoding of refined types with scodec and allows refiningscodec.bits.ByteVector
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:
- argonaut-refined
- circe-refined
- ciris-refined
- decline-refined
- doobie-refined
- exercises-refined
- extruder-refined
- formulation-refined
- kantan.csv-refined
- kantan.regex-refined
- kantan.xpath-refined
- monocle-refined
- play-refined
- play-json-refined
- play-json-refined
- refined-anorm
- refined-guava
- seals-refined
- slick-refined
- strictify-refined
- validated-config
- xml-names-core
If your open source project is using refined, please consider opening a pull request to list it here:
- 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:
API documentation of the latest release is available at: https://static.javadoc.io/eu.timepit/refined_2.12/0.8.7/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 alwaystrue
False
: constant predicate that is alwaysfalse
Not[P]
: negation of the predicateP
And[A, B]
: conjunction of the predicatesA
andB
Or[A, B]
: disjunction of the predicatesA
andB
Xor[A, B]
: exclusive disjunction of the predicatesA
andB
Nand[A, B]
: negated conjunction of the predicatesA
andB
Nor[A, B]
: negated disjunction of the predicatesA
andB
AllOf[PS]
: conjunction of all predicates inPS
AnyOf[PS]
: disjunction of all predicates inPS
OneOf[PS]
: exclusive disjunction of all predicates inPS
Digit
: checks if aChar
is a digitLetter
: checks if aChar
is a letterLetterOrDigit
: checks if aChar
is a letter or digitLowerCase
: checks if aChar
is a lower case characterUpperCase
: checks if aChar
is an upper case characterWhitespace
: checks if aChar
is white space
Contains[U]
: checks if aTraversable
contains a value equal toU
Count[PA, PC]
: counts the number of elements in aTraversable
which satisfy the predicatePA
and passes the result to the predicatePC
Empty
: checks if aTraversable
is emptyNonEmpty
: checks if aTraversable
is not emptyForall[P]
: checks if the predicateP
holds for all elements of aTraversable
Exists[P]
: checks if the predicateP
holds for some elements of aTraversable
Head[P]
: checks if the predicateP
holds for the first element of aTraversable
Index[N, P]
: checks if the predicateP
holds for the element at indexN
of a sequenceInit[P]
: checks if the predicateP
holds for all but the last element of aTraversable
Last[P]
: checks if the predicateP
holds for the last element of aTraversable
Tail[P]
: checks if the predicateP
holds for all but the first element of aTraversable
Size[P]
: checks if the size of aTraversable
satisfies the predicateP
MinSize[N]
: checks if the size of aTraversable
is greater than or equal toN
MaxSize[N]
: checks if the size of aTraversable
is less than or equal toN
Equal[U]
: checks if a value is equal toU
Less[N]
: checks if a numeric value is less thanN
LessEqual[N]
: checks if a numeric value is less than or equal toN
Greater[N]
: checks if a numeric value is greater thanN
GreaterEqual[N]
: checks if a numeric value is greater than or equal toN
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 moduloN
isO
Divisible[N]
: checks if an integral value is evenly divisible byN
NonDivisible[N]
: checks if an integral value is not evenly divisible byN
Even
: checks if an integral value is evenly divisible by 2Odd
: checks if an integral value is not evenly divisible by 2
EndsWith[S]
: checks if aString
ends with the suffixS
MatchesRegex[S]
: checks if aString
matches the regular expressionS
Regex
: checks if aString
is a valid regular expressionStartsWith[S]
: checks if aString
starts with the prefixS
Uri
: checks if aString
is a valid URIUrl
: checks if aString
is a valid URLUuid
: checks if aString
is a valid UUIDValidInt
: checks if aString
is a parsableInt
ValidLong
: checks if aString
is a parsableLong
ValidDouble
: checks if aString
is a parsableDouble
ValidBigInt
: checks if aString
is a parsableBigInt
ValidBigDecimal
: checks if aString
is a parsableBigDecimal
Xml
: checks if aString
is well-formed XMLXPath
: checks if aString
is a valid XPath expression
- Alexandre Archambault (@alxarchambault)
- Chris Hodapp (@clhodapp)
- Dale Wijnand (@dwijnand)
- Derek Morr (@derekmorr)
- Didac
- Frank S. Thomas (@fst9000)
- Howard Perrin
- Iurii Susuk (@IuriiSusuk)
- Jean-Rémi Desjardins (@jrdesjardins)
- Joe Greene
- John-Michael Reed
- kusamakura
- Leif Wickland
- Naoki Aoyama (@AoiroAoino)
- Nicolas Rinaudo (@NicolasRinaudo)
- Olli Helenius
- Richard Gomes
- ronanM
- Sam Halliday
- Shohei Shimomura (@sm0kym0nkey)
- Tim Steinbach (@Tim_Steinbach)
- Torsten Scholak (@tscholak)
- Viktor Lövgren (@vlovgr)
- Vladimir Koshelev (@vlad_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 Typelevel code of conduct.
Using refined's macros for compile-time refinement has zero runtime overhead for reference types and only causes boxing for value types. Refer to RefineJavapSpec and InferJavapSpec for a detailed analysis of the runtime component of refinement types on the JVM.
- 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 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 http://opensource.org/licenses/MIT and also in the LICENSE file.