refined: simple refinement types for Scala

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.auto._
import eu.timepit.refined.numeric._
import shapeless.tag.@@

// This refines Int with the Positive predicate and checks via an
// implicit macro that the assigned value satisfies it:
val i1: Int @@ Positive = 5
i1: Int @@ Positive = 5

// If the value does not satisfy the predicate, we get a meaningful
// compile error:
val i2: Int @@ Positive = -5
<console>:21: error: Predicate failed: (-5 > 0).
       val i2: Int @@ Positive = -5
                                  ^

// There is also the explicit refineMT macro that can infer the base
// type from its parameter:
scala> refineMT[Positive](5)
res0: Int @@ Positive = 5

// Macros can only validate literals because their values are known at
// compile-time. 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).)

@@ is shapeless' type for tagging types which has the nice property of being a subtype of its first type parameter (i.e. (T @@ P) <: T).

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 shapeless.nat._

scala> val a: Int @@ Greater[_5] = 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.

More examples
Using refined
Documentation
Provided predicates
Contributors and participation
Projects using refined
Performance concerns
Related projects
License

More examples

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.")
                                                    ^

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.

Using refined

The latest version of the library is 0.3.2, which is available for Scala and Scala.js version 2.10 and 2.11.

If you're using sbt, add the following to your build:

libraryDependencies ++= Seq(
  "eu.timepit" %% "refined"            % "0.3.2",
  "eu.timepit" %% "refined-scalaz"     % "0.3.2",         // optional, JVM only
  "eu.timepit" %% "refined-scodec"     % "0.3.2",         // optional
  "eu.timepit" %% "refined-scalacheck" % "0.3.2" % "test" // 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.3.2.markdown.

Documentation

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.

Provided predicates

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
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 a TraversableOnce contains a value equal to U
Count[PA, PC]: counts the number of elements in a TraversableOnce which satisfy the predicate PA and passes the result to the predicate PC
Empty: checks if a TraversableOnce is empty
NonEmpty: checks if a TraversableOnce is not empty
Forall[P]: checks if the predicate P holds for all elements of a TraversableOnce
Exists[P]: checks if the predicate P holds for some elements of a TraversableOnce
Head[P]: checks if the predicate P holds for the first element of a Traversable
Index[N, P]: checks if the predicate P holds for the element at index N of a sequence
Last[P]: checks if the predicate P holds for the last element of a Traversable
Size[P]: checks if the size of a TraversableOnce satisfies the predicate P
MinSize[N]: checks if the size of a TraversableOnce is greater than or equal to N
MaxSize[N]: checks if the size of a TraversableOnce is less than or equal to N

generic

Equal[U]: checks if a value is equal to U
Eval[S]: checks if a value applied to the predicate S yields true
ConstructorNames[P]: checks if the constructor names of a sum type satisfy P
FieldNames[P]: checks if the field names of a product type satisfy P
Subtype[U]: witnesses that the type of a value is a subtype of U
Supertype[U]: witnesses that the type of a value is a supertype of 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]

string

EndsWith[S]: checks if a String ends with the suffix S
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
Xml: checks if a String is valid XML
XPath: checks if a String is a valid XPath expression

Contributors and participation

The refined project supports the Typelevel code of conduct and wants all of its channels (Gitter, GitHub, etc.) to be welcoming environments for everyone.

Projects using refined

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.

argonaut-shapeless - provides the argonaut-refined subproject for (de)serialization of refined types from and to JSON
circe - provides the circe-refined subproject for (de)serialization of refined types from and to JSON
Monocle - provides the monocle-refined subproject which contains lenses for safe bit indexing into primitive types
Your project here :-)

Performance concerns

Using refined's macros for compile-time refinement bears zero runtime overhead for reference types and only causes boxing for value types. PostErasureAnyRef and PostErasureAnyVal show the differences of unrefined and refined types during the posterasure compiler phase.

Related projects

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!

License

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

jedesah/refined