Skip to content
BranchesTags

Repository files navigation

refined: simple refinement types for Scala

Build Statuscodecov.ioGitterScaladexScaladoc

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:

importeu.timepit.refined._importeu.timepit.refined.api.Refinedimporteu.timepit.refined.auto._importeu.timepit.refined.numeric._// This refines Int with the Positive predicate and checks via an// implicit macro that the assigned value satisfies it:
scala>vali1:IntRefinedPositive=5
i1:IntRefinedPositive=5// If the value does not satisfy the predicate, we get a meaningful// compile error:
scala>vali2:IntRefinedPositive=-5
<console>:22:error: Predicatefailed: (-5>0).
vali2:IntRefinedPositive=-5^// There is also the explicit refineMV macro that can infer the base// type from its parameter:
scala> refineMV[Positive](5)
res0:IntRefinedPositive=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>valx=42// suppose the value of x is not known at compile-time
scala> refineV[Positive](x)
res1:Either[String, IntRefinedPositive] =Right(42)
scala> refineV[Positive](-x)
res2:Either[String, IntRefinedPositive] =Left(Predicatefailed: (-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>vala:IntRefinedGreater[W.`5`.T] =10
a:IntRefinedGreater[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>valb:IntRefinedGreater[W.`4`.T] = a
b:IntRefinedGreater[Int(4)] =10// An unsound ascription leads to a compile error:
scala>valc:IntRefinedGreater[W.`6`.T] = a
<console>:23:error: typemismatch (invalid inference):Greater[Int(5)] does not imply
Greater[Int(6)]
valc:IntRefinedGreater[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.

Table of contents

  1. More examples
  2. Using refined
  3. Community
  4. Documentation
  5. Provided predicates
  6. Contributors and participation
  7. Performance concerns
  8. Related projects
  9. License

More examples

importeu.timepit.refined.api.RefTypeimporteu.timepit.refined.boolean._importeu.timepit.refined.char._importeu.timepit.refined.collection._importeu.timepit.refined.generic._importeu.timepit.refined.string._importshapeless.{ ::, HNil }
scala> refineMV[NonEmpty]("Hello")
res2:StringRefinedNonEmpty=Hello
scala> refineMV[NonEmpty]("")
<console>:39:error: Predicate isEmpty() did not fail.
refineMV[NonEmpty]("")
^
scala>typeZeroToOne=Not[Less[W.`0.0`.T]] AndNot[Greater[W.`1.0`.T]]
defined typealiasZeroToOne
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:CharRefinedAnyOf[Digit::Letter::Whitespace::HNil] =F
scala> refineMV[MatchesRegex[W.`"[0-9]+"`.T]]("123.")
<console>:39:error: Predicatefailed: "123.".matches("[0-9]+").
refineMV[MatchesRegex[W.`"[0-9]+"`.T]]("123.")
^
scala>vald1:CharRefinedEqual[W.`'3'`.T] ='3'
d1:CharRefinedEqual[Char('3')] =3
scala>vald2:CharRefinedDigit= d1
d2:CharRefinedDigit=3
scala>vald3:CharRefinedLetter= d1
<console>:39:error: typemismatch (invalid inference):Equal[Char('3')] does not imply
Lettervald3:CharRefinedLetter= d1
^
scala>valr1:StringRefinedRegex="(a|b)"
r1:StringRefinedRegex= (a|b)
scala>valr2:StringRefinedRegex="(a|b"
<console>:38:error: Regex predicate failed: Unclosed group near index 4
(a|b
^valr2:StringRefinedRegex="(a|b"^
scala>valu1:StringRefinedUrl="htp://example.com"
<console>:38:error: Url predicate failed: unknown protocol: htp
valu1:StringRefinedUrl="htp://example.com"^// Here we define a refined type "Int with the predicate (7 <= value < 77)".
scala>typeAge=IntRefinedInterval.ClosedOpen[W.`7`.T, W.`77`.T]
scala>valuserInput=55// We can refine values with this refined type by either using `refineV`// with an explicit return type
scala>valageEither1:Either[String, Age] = refineV(userInput)
ageEither1:Either[String,Age] =Right(55)
// or by using `RefType.applyRef` with the refined type as type parameter.
scala>valageEither2=RefType.applyRef[Age](userInput)
ageEither2:Either[String,Age] =Right(55)

Using refined

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

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.14/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

License

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

About

Simple refinement types for Scala

Resources

Readme
MIT license
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

Packages

Contributors

Languages