refined
refined copied to clipboard
Refinement types for Scala
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[10]
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[5] = 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[4]:
scala> val b: Int Refined Greater[4] = a
b: Int Refined Greater[Int(4)] = 10
// An unsound ascription leads to a compile error:
scala> val c: Int Refined Greater[6] = a
^
error: type mismatch (invalid inference):
eu.timepit.refined.numeric.Greater[5] does not imply
eu.timepit.refined.numeric.Greater[6]
This mechanism allows to pass values of more specific types (e.g.
Int Refined Greater[10]
) to functions that take a more general
type (e.g. Int Refined Positive
) without manual intervention.
prior Scala 2.13 without literal types
Since there are no literal types prior to Scala 2.13 the literals must be created with shapeless:
scala> val a: Int Refined Greater[W.`5`.T] = 10
a: Int Refined Greater[Int(5)] = 10
scala> val b: Int Refined Greater[W.`4`.T] = a
b: Int Refined Greater[Int(4)] = 10
Note that W
is a shortcut for shapeless.Witness
which provides
syntax for literal-based singleton types.
Table of contents
- More examples
- Using refined
- Community
- Documentation
- Provided predicates
- Contributors and participation
- Related projects
- License
More examples
import eu.timepit.refined._
import eu.timepit.refined.auto._
import eu.timepit.refined.numeric._
import eu.timepit.refined.api.{RefType, Refined}
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[0.0]] And Not[Greater[1.0]]
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["[0-9]+"]]("123.")
<console>:39: error: Predicate failed: "123.".matches("[0-9]+").
refineMV[MatchesRegex[W.`"[0-9]+"`.T]]("123.")
^
scala> val d1: Char Refined Equal['3'] = '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[7, 77]
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.10.1, 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.10.1",
"eu.timepit" %% "refined-cats" % "0.10.1", // optional
"eu.timepit" %% "refined-eval" % "0.10.1", // optional, JVM-only
"eu.timepit" %% "refined-jsonpath" % "0.10.1", // optional, JVM-only
"eu.timepit" %% "refined-pureconfig" % "0.10.1", // optional, JVM-only
"eu.timepit" %% "refined-scalacheck" % "0.10.1", // optional
"eu.timepit" %% "refined-scalaz" % "0.10.1", // optional
"eu.timepit" %% "refined-scodec" % "0.10.1", // optional
"eu.timepit" %% "refined-scopt" % "0.10.1", // optional
"eu.timepit" %% "refined-shapeless" % "0.10.1" // 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 here.
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 theEval[S]
predicate that checks if a value applied to the predicateS
yieldstrue
-
refined-jsonpath
provides theJSONPath
predicate that checks if aString
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. Userefined-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 forscalaz.@@
-
refined-scodec
allows binary decoding and encoding of refined types with scodec and allows refiningscodec.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:
- api-refiner
- argonaut-refined
- atto-refined
- case-app-refined
- circe-refined
- ciris-refined
- cormorant-refined
- coulomb-refined
- decline-refined
- doobie-refined
- exercises-refined
- extruder-refined
- finch-refined
- formulation-refined
- kantan.csv-refined
- kantan.regex-refined
- kantan.xpath-refined
- monocle-refined
- neotypes-refined
- play-refined
- play-json-refined
- play-json-refined
- refined-anorm
- refined-guava
- scanamo-refined
- seals-refined
- slick-refined
- spray-json-refined
- strictify-refined
- validated-config
- vulcan-refined
- xml-names-core
Projects using refined
If your open source project is using refined, please consider opening a pull request to list it here:
- calypso: BSON library for Scala
- 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.10.1/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:
-
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 digit -
Letter
: checks if aChar
is a letter -
LetterOrDigit
: checks if aChar
is a letter or digit -
LowerCase
: checks if aChar
is a lower case character -
UpperCase
: checks if aChar
is an upper case character -
Whitespace
: checks if aChar
is white space
-
Contains[U]
: checks if anIterable
contains a value equal toU
-
Count[PA, PC]
: counts the number of elements in anIterable
which satisfy the predicatePA
and passes the result to the predicatePC
-
Empty
: checks if anIterable
is empty -
NonEmpty
: checks if anIterable
is not empty -
Forall[P]
: checks if the predicateP
holds for all elements of anIterable
-
Exists[P]
: checks if the predicateP
holds for some elements of anIterable
-
Head[P]
: checks if the predicateP
holds for the first element of anIterable
-
Index[N, P]
: checks if the predicateP
holds for the element at indexN
of a sequence -
Init[P]
: checks if the predicateP
holds for all but the last element of anIterable
-
Last[P]
: checks if the predicateP
holds for the last element of anIterable
-
Tail[P]
: checks if the predicateP
holds for all but the first element of anIterable
-
Size[P]
: checks if the size of anIterable
satisfies the predicateP
-
MinSize[N]
: checks if the size of anIterable
is greater than or equal toN
-
MaxSize[N]
: checks if the size of anIterable
is less than or equal toN
-
Equal[U]
: checks if a value is equal toU
-
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 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 moduloN
isO
-
Divisible[N]
: checks if an integral value is evenly divisible byN
-
NonDivisible[N]
: checks if an integral value is not evenly divisible byN
-
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
-
EndsWith[S]
: checks if aString
ends with the suffixS
-
IPv4
: checks if aString
is a valid IPv4 -
IPv6
: checks if aString
is a valid IPv6 -
MatchesRegex[S]
: checks if aString
matches the regular expressionS
-
Regex
: checks if aString
is a valid regular expression -
StartsWith[S]
: checks if aString
starts with the prefixS
-
Uri
: checks if aString
is a valid URI -
Url
: checks if aString
is a valid URL -
Uuid
: checks if aString
is a valid UUID -
ValidByte
: checks if aString
is a parsableByte
-
ValidShort
: checks if aString
is a parsableShort
-
ValidInt
: checks if aString
is a parsableInt
-
ValidLong
: checks if aString
is a parsableLong
-
ValidFloat
: checks if aString
is a parsableFloat
-
ValidDouble
: checks if aString
is a parsableDouble
-
ValidBigInt
: checks if aString
is a parsableBigInt
-
ValidBigDecimal
: checks if aString
is a parsableBigDecimal
-
Xml
: checks if aString
is well-formed XML -
XPath
: checks if aString
is a valid XPath expression -
Trimmed
: checks if aString
has no leading or trailing whitespace -
HexStringSpec
: checks if aString
represents a hexadecimal number
Contributors and participation
The following people have helped making refined great:
- Alex
- Alexandre Archambault
- Arman Bilge
- Brian P. Holt
- Chris Birchall
- Chris Hodapp
- Cody Allen
- Dale Wijnand
- Denys Shabalin
- Derek Morr
- Didac
- Diogo Castro
- dm-tran
- Ender Tunç
- Frank S. Thomas
- Frederick Roth
- Howard Perrin
- Iurii Susuk
- Jean-Rémi Desjardins
- Jente Hidskes
- Joe Greene
- John-Michael Reed
- Julien BENOIT
- kalejami
- kenji yoshida
- kusamakura
- 急須
- Leif Wickland
- Luis Miguel Mejía Suárez
- Mateusz Wójcik
- Matt Pickering
- Michael Thomas
- Michal Sitko
- Naoki Aoyama
- Nicolas Rinaudo
- Olli Helenius
- Richard Gomes
- ronanM
- Sam Guymer
- Sam Halliday
- Shawn Garner
- Shohei Shimomura
- Shunsuke Otani
- Tim Steinbach
- Torsten Scholak
- Viktor Lövgren
- Vladimir Koshelev
- Yuki Ishikawa
- Zainab Ali
- 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 Scala Code of Conduct.
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 by 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.