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.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"
^
The latest version of the library is 0.6.2, 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.6.2",
"eu.timepit" %% "refined-pureconfig" % "0.6.2" // optional, JVM-only
"eu.timepit" %% "refined-scalacheck" % "0.6.2", // optional
"eu.timepit" %% "refined-scalaz" % "0.6.2", // optional
"eu.timepit" %% "refined-scodec" % "0.6.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 available in 0.6.2.markdown.
The optional dependencies are add-on libraries that provide support for other tag types or integration of refined types in other libraries:
refined-pureconfig
for PureConfig integrationrefined-scalacheck
for ScalaCheck type class instances of refined typesrefined-scalaz
for support of Scalaz' tag type (scalaz.@@
)refined-scodec
for scodec integration
See also the list of projects that use refined for libraries that directly provide support for refined.
API documentation of the latest release is available at: http://fthomas.github.io/refined/latest/api/
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
Eval[S]
: checks if a value applied to the predicateS
yieldstrue
ConstructorNames[P]
: checks if the constructor names of a sum type satisfyP
FieldNames[P]
: checks if the field names of a product type satisfyP
Subtype[U]
: witnesses that the type of a value is a subtype ofU
Supertype[U]
: witnesses that the type of a value is a supertype ofU
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
]
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 UUIDXml
: checks if aString
is well-formed XMLXPath
: checks if aString
is a valid XPath expression
- Alexandre Archambault (@alxarchambault)
- Dale Wijnand (@dwijnand)
- Frank S. Thomas (@fst9000)
- Jean-Rémi Desjardins (@jrdesjardins)
- John-Michael Reed
- Shohei Shimomura (@sm0kym0nkey)
- Viktor Lövgren (@vlovgr)
- Vladimir Koshelev (@vlad_koshelev)
- 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.
Please see the wiki for an incomplete list of projects and companies which use refined. If you are using the library and your project isn't listed yet, please add it.
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
- 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.