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.numeric._
// refineMT decorates the type of its parameter if it satisfies the
// given type-level predicate:
scala> refineMT[Positive](5)
res0: Int @@ Positive = 5
// The type Int @@ Positive is the type of all Int values that are
// greater than zero.
// If the parameter does not satisfy the predicate, we get a meaningful
// compile error:
scala> refineMT[Positive](-5)
<console>:34: error: Predicate failed: (-5 > 0).
refineMT[Positive](-5)
^
// refineMT is a macro and only works with literals. To validate
// arbitrary (runtime) values we can use the refineT function:
scala> refineT[Positive](5)
res1: Either[String, Int @@ Positive] = Right(5)
scala> refineT[Positive](-5)
res2: Either[String, Int @@ Positive] = Left(Predicate failed: (-5 > 0).)Note that @@ is shapeless' type for tagging types.
refined also contains inference rules for converting between different
refined types. For example, Int @@ Greater[_10] can be safely converted
to Int @@ 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:
import eu.timepit.refined.implicits._
import shapeless.nat._
import shapeless.tag.@@
scala> val a: Int @@ Greater[_5] = refineMT(10)
a: Int @@ Greater[_5] = 10
// Since every value greater than 5 is also greater than 4, a can be ascribed
// the type Int @@ Greater[_4]:
scala> val b: Int @@ Greater[_4] = a
b: Int @@ Greater[_4] = 10
// An unsound ascription leads to a compile error:
scala> val c: Int @@ Greater[_6] = a
<console>:34: error: invalid inference: Greater[_5] ==> Greater[_6]
val b: Int @@ Greater[_6] = a
^This mechanism allows to pass values of more specific types (e.g. Int @@ Greater[_10])
to functions that take a more general type (e.g. Int @@ Positive) without manual
intervention.
import shapeless.{ ::, HNil }
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._
scala> refineMT[NonEmpty]("Hello")
res2: String @@ NonEmpty = Hello
scala> refineMT[NonEmpty]("")
<console>:27: error: Predicate isEmpty() did not fail.
refineMT[NonEmpty]("")
^
scala> type ZeroToOne = Not[Less[_0]] And Not[Greater[_1]]
defined type alias ZeroToOne
scala> refineMT[ZeroToOne](1.8)
<console>:27: error: Right predicate of (!(1.8 < 0) && !(1.8 > 1)) failed: Predicate (1.8 > 1) did not fail.
refineMT[ZeroToOne](1.8)
^
scala> refineMT[AnyOf[Digit :: Letter :: Whitespace :: HNil]]('F')
res3: Char @@ AnyOf[Digit :: Letter :: Whitespace :: HNil] = F
scala> refineMT[MatchesRegex[W.`"[0-9]+"`.T]]("123.")
<console>:34: error: Predicate failed: "123.".matches("[0-9]+").
refineMT[MatchesRegex[W.`"[0-9]+"`.T]]("123.")
^
// The implicits object contains an implicit version of refineMT which is
// used here to validate that the right-hand side is equal to '3' (obviously
// there is only one value satisfying this predicate):
scala> val d1: Char @@ Equal[W.`'3'`.T] = '3'
d1: Char @@ Equal[Char('3')] = 3
scala> val d2: Char @@ Digit = d1
d2: Char @@ Digit = 3
scala> val d3: Char @@ Letter = d1
<console>:34: error: invalid inference: Equal[Char('3')] ==> Letter
val d3: Char @@ Letter = d1
^
scala> val r1: String @@ Regex = "(a|b)"
r1: String @@ Regex = (a|b)
scala> val r2: String @@ Regex = "(a|b"
<console>:40: error: Regex predicate failed: Unclosed group near index 4
(a|b
^
val r2: String @@ Regex = "(a|b"
^
scala> val u1: String @@ Url = "htp://example.com"
<console>:40: error: Url predicate failed: unknown protocol: htp
val u1: String @@ Url = "htp://example.com"
^Note that W is a shortcut for shapeless.Witness which
provides syntax for singleton types.
The latest version of the library is 0.2.0, which is available for Scala and Scala.js version 2.11.
If you're using SBT, add the following to your build:
libraryDependencies += "eu.timepit" %% "refined" % "0.2.0"
Or for Scala.js:
libraryDependencies += "eu.timepit" %%% "refined" % "0.2.0"
Instructions for Maven and other build tools are available at search.maven.org.
Release notes for the latest version are available in 0.2.0.markdown.
API documentation of the latest release is available at: http://fthomas.github.io/refined/latest/api/
There are also further (type-checked) examples in the docs
directory including one for defining custom predicates.
refined basically consists of two parts, one for refining types with type-level predicates and the other for converting between different refined types.
The refinement machinery is built of:
-
Type-level predicates for refining other types, like
UpperCase,Positive, orLessEqual[_2]. There are also higher order predicates for combining proper predicates likeAnd[_, _],Or[_, _],Not[_],Forall[_], orSize[_]. -
A
Predicatetype class for validating a value of an unrefined type (likeDouble) against a type-level predicate (likePositive). -
A function
refineTand a macrorefineMTthat take a predicatePand some value of typeT, validate this value with aPredicate[P, T]and return the value with typeT @@ Pif validation was successful or an error otherwise. The return type ofrefineTisEither[String, T @@ P]while therefineMTreturns aT @@ Por compilation fails. SincerefineMTis a macro it only works with literal values or constant predicates.
The type-conversions are built of:
-
An
InferenceRuletype class that is indexed by two type-level predicates which states whether the second predicate can be logically derived from the first.InferenceRule[Greater[_5], Positive]would be an instance of a valid inference rule whileInferenceRule[Greater[_5], Negative]would be an invalid inference rule. -
An implicit conversion defined as macro that casts a value of type
T @@ Ato typeT @@ Bif a validInferenceRule[A, B]is in scope.
The library comes with these predefined predicates:
True: constant predicate that is alwaystrueFalse: constant predicate that is alwaysfalseNot[P]: negation of the predicatePAnd[A, B]: conjunction of the predicatesAandBOr[A, B]: disjunction of the predicatesAandBXor[A, B]: exclusive disjunction of the predicatesAandBAllOf[PS]: conjunction of all predicates inPSAnyOf[PS]: disjunction of all predicates inPSOneOf[PS]: exclusive disjunction of all predicates inPS
Digit: checks if aCharis a digitLetter: checks if aCharis a letterLetterOrDigit: checks if aCharis a letter or digitLowerCase: checks if aCharis a lower case characterUpperCase: checks if aCharis an upper case characterWhitespace: checks if aCharis white space
Contains[U]: checks if aTraversableOncecontains a value equal toUCount[PA, PC]: counts the number of elements in aTraversableOncewhich satisfy the predicatePAand passes the result to the predicatePCEmpty: checks if aTraversableOnceis emptyNonEmpty: checks if aTraversableOnceis not emptyForall[P]: checks if the predicatePholds for all elements of aTraversableOnceExists[P]: checks if the predicatePholds for some elements of aTraversableOnceHead[P]: checks if the predicatePholds for the first element of aTraversableIndex[N, P]: checks if the predicatePholds for the element at indexNof a sequenceLast[P]: checks if the predicatePholds for the last element of aTraversableSize[P]: checks if the size of aTraversableOncesatisfies the predicatePMinSize[N]: checks if the size of aTraversableOnceis greater than or equal toNMaxSize[N]: checks if the size of aTraversableOnceis less than or equal toN
Equal[U]: checks if a value is equal toUConstructorNames[P]: checks if the constructor names of a sum type satisfyPFieldNames[P]: checks if the field names of a product type satisfyPSubtype[U]: witnesses that the type of a value is a subtype ofUSupertype[U]: witnesses that the type of a value is a supertype ofU
Less[N]: checks if a numeric value is less thanNLessEqual[N]: checks if a numeric value is less than or equal toNGreater[N]: checks if a numeric value is greater thanNGreaterEqual[N]: checks if a numeric value is greater than or equal toNPositive: 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[L, H]: checks if a numeric value is in the interval [L,H]
EndsWith[S]: checks if aStringends with the suffixSMatchesRegex[R]: checks if aStringmatches the regular expressionRRegex: checks if aStringis a valid regular expressionStartsWith[S]: checks if aStringstarts with the prefixSUri: checks if aStringis a valid URIUrl: checks if aStringis a valid URLUuid: checks if aStringis a valid UUIDXml: checks if aStringis valid XMLXPath: checks if aStringis a valid XPath expression
- Your name here :-)
If you have a project that uses the library to enforce more static guarantees and you'd like to include in this list, please open a pull request or mention it in the Gitter channel and we'll add a link to it here.
- Your project here :-)
This library is inspired by the refined library for Haskell. It even stole its name! Another Scala library that provides type-level validations is bond.
refined is licensed under the MIT license, available at http://opensource.org/licenses/MIT and also in the LICENSE file.