Skip to content

note/mini-refined

main
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 

mini-refined

example workflow

A proof of concept of a simple encoding of refinement types in Scala 3.

You can read about motivation behind and the main concepts in the blog post.

Quick start

Include library in build.sbt:

libraryDependencies += "pl.msitko" %% "mini-refined" % "0.2.0"

Common imports:

import pl.msitko.refined.auto._
import pl.msitko.refined.Refined

Circe integration

To use circe integration:

libraryDependencies += "pl.msitko" %% "mini-refined-circe" % "0.2.0"

Int predicates

val a: Int Refined GreaterThan[10] = 5
// fails compilation with: Validation failed: 5 > 10
val a: Int Refined LowerThan[10] = 15
// fails compilation with: Validation failed: 15 < 10

String predicates

val s: String Refined StartsWith["xyz"] = "abc"
// fails compilation with: Validation failed: abc.startsWith(xyz)
val s: String Refined EndsWith["xyz"] = "abc"
// fails compilation with: Validation failed: abc.endsWith(xyz)

List predicates

val as: List[String] Refined Size[GreaterThan[1]] = List("a")
// fails compilation with: 
// Validation failed: list size doesn't hold predicate: 1 > 1

You can use any Int predicates within Size predicate.

Compose predicates with boolean operators

You can compose predicates with boolean operators. For example:

val c: Int Refined And[GreaterThan[10], LowerThan[20]] = 25
// fails compilation with: Validation failed: (25 > 10 And 25 < 20), predicate failed: 25 < 20

Runtime validation

Everything described so far works only for values known at a compile-time. However, values for most variables are coming at runtime. For those you need to use Refined.refineV[T] which returns Either[String, T]. Example:

case class Example(a: Int, b: Int Refined GreaterThan[10])

def runtime(a: Int, b: Int): Either[String, Example] =
  Refined.refineV[GreaterThan[10]](b).map(refined => Example(a, refined))

Inferring types compatibility

mini-refined has some basic rules that enable using more specific types in places where more general types are required.

In other words, considering such function:

def intFun10(a: Int Refined GreaterThan[10]): Unit = ???

We can call it with a value of type Int Refined GreaterThan[20], as mini-refined recognizes that being greater than 20 implies being greater than 10.

About

Simple encoding of refinement types in Scala 3

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages