refined

Simple refinement types for Scala

⭐ 0

README

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 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[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
Community
Documentation
Provided predicates
Contributors and participation
Performance concerns
Related projects
License

More examples

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)

Using refined

The latest version of the library is 0.9.15, 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.9.15",
  "eu.timepit" %% "refined-cats"            % "0.9.15", // optional
  "eu.timepit" %% "refined-eval"            % "0.9.15", // optional, JVM-only
  "eu.timepit" %% "refined-jsonpath"        % "0.9.15", // optional, JVM-only
  "eu.timepit" %% "refined-pureconfig"      % "0.9.15", // optional, JVM-only
  "eu.timepit" %% "refined-scalacheck"      % "0.9.15", // optional
  "eu.timepit" %% "refined-scalaz"          % "0.9.15", // optional
  "eu.timepit" %% "refined-scodec"          % "0.9.15", // optional
  "eu.timepit" %% "refined-scopt"           % "0.9.15", // optional
  "eu.timepit" %% "refined-shapeless"       % "0.9.15"  // 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.9.15.markdown.

Community

Internal modules

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

External modules

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:

Projects using refined

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

Adopters

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

Documentation

API documentation of the latest release is available at:
https://static.javadoc.io/eu.timepit/refined_2.12/0.9.15/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.

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

Contributors and participation

The following people have helped making refined great:

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.

Performance concerns

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.

Related projects

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

License

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