Refinement Types in Practice

class: center, middle
background-image: url(background.jpg)

# Refinement Types In Practice
## Peter Mortier
## April 2018

GitHub: [@kwark](https://github.com/kwark) /
 Twitter: [@kwarkk](https://twitter.com/kwarkk)

---

#About me .image-200[![Vlaanderen is wegen en verkeer](https://docs.wegenenverkeer.be/Huisstijl%20AWV/Vol%20logo/Vlaanderen_is_wegenenverkeer_vol.png)]

Freelance Scala developer @ [Agentschap Wegen en Verkeer](http://wegenenverkeer.be/)

Twenty years of JVM experience: wrote my first applet in 1996

Did Javascript on the server (SSJS) before it was cool: Netscape Enterprise Server

Used [Pizza language](https://en.wikipedia.org/wiki/Pizza_%28programming_language%29): a superset of Java with support for generics

Interested in Scala through [Functional Programming Principles in Scala](https://www.coursera.org/learn/progfun1) course on Coursera

???

I started programming in this crazy old time, where we did things in reverse

We used java on the client and javascript on the server.

Pizza was invented by Martin Odersky and he later worked on the java compiler to support generics

---

# Agenda

* Stringly typed

* Smart constructors

* Taking it to the type level

* Introducing Refined

* Slick integration

* Play integration

* Extension methods

* Newtyping, tagging

---

# [Stringly typed](http://wiki.c2.com/?StringlyTyped)

> *"A riff on strongly typed. Used to describe an implementation that needlessly relies on strings."*

## What's the problem when using Strings?

* A `String` can *represent* anything
* A `String` can *contain* anything

???
A pun on strongly typed

represent: URL, a first name, an authorization token, ...

contain: nothing (empty string), entire contents of the bible

Not only strings, but also APIs that rely on Int or Long

Why do we keep on using them:

baked into the language (every API supports them)

types like String come with a bunch of useful methods: concat, toUppercase, ...

```scala
final case class Developer(name: String, twitterHandle: String)

Developer("Peter", "@kwarkk") // ok

Developer("@kwarkk", "Peter") // Oops, we've got a bug!
```
???
Let's see an example in code of a stringly typed API

Here we have a case class representing a Developer in our domain

And our developer has a name and a twitterhandle (which is his or hers twitter username)

I can now simply construct a developer

But if I accidently switch the arguments, I have introduced a bug

---
# Type aliases to the rescue ?

```scala
type Name = String
type TwitterHandle = String

final case class Developer(name: Name, twitterHandle: TwitterHandle)

val name: Name = "Peter"
val twitterHandle: TwitterHandle = "@kwarkk"

Developer(name, twitterHandle) // ok

Developer(twitterHandle, name) // Again, we've got a bug
```
???
Let's see if we can do better.

First we'll try a solution using type aliases

type aliases don't work for this

type aliases are great

if you have a complicated type and want to avoid retyping it over and over again, or clear up your method signatures

we'll see a great use of them later on

---
# Value classes to the rescue ?

```scala
final class Name(val value: String) extends AnyVal

final class TwitterHandle (val value: String) extends AnyVal

final case class Developer(name: Name, twitterHandle: TwitterHandle)
```
And now we can't switch arguments anymore !

```scala
scala> Developer(new TwitterHandle("@kwarkk"), new Name("Peter"))
<console>:19: error: type mismatch;
 found : TwitterHandle
 required: Name
 Developer(new TwitterHandle("@kwarkk"), new Name("Peter"))
 ^
<console>:19: error: type mismatch;
 found : Name
 required: TwitterHandle
 Developer(new TwitterHandle("@kwarkk"), new Name("Peter"))
 ^
```
???
value class: class with single parameter, which extends AnyVal

advantage is that compiler will try to avoid to allocating them at runtime

at runtime a Name will still be a string

most of the time

https://stackoverflow.com/questions/34561614/should-i-use-the-final-modifier-when-declaring-case-classes

---
# Value classes to the rescue ?

But these value classes can still contain any `String`:

```scala
// Sigh, yet another bug!
Developer(new Name("@kwarkk"), new TwitterHandle("Peter"))
```

---
# Add validation with smart constructors

```scala
object smart {

final class TwitterHandle private(val value: String) extends AnyVal

object TwitterHandle {
    def fromString(s: String): Option[TwitterHandle] = {
      if (s.startsWith("@")) Some(new TwitterHandle(s))
      else None
    }
  }

final class Name private(val value: String) extends AnyVal

object Name {
    def fromString(s: String): Option[Name] = {
       if (s.nonEmpty) Some(new Name(s)) else None
    }
  }

final case class Developer(name: Name, twitterHandle: TwitterHandle)

}
```
???
make constructor of value class private

create a companion object with a factory method

that validates the input string

and either returns None if input is invalid

or Some if it is valid

---
# Smart constructors

```scala
import smart._

val maybeName: Option[Name]              = Name.fromString("Peter Mortier")
val maybeHandle: Option[TwitterHandle]   = TwitterHandle.fromString("@kwarkk")
val invalidHandle: Option[TwitterHandle] = TwitterHandle.fromString("foo")

Developer(
    maybeName.get, // Ugh! .get
    maybeHandle.get
)
```
???
So, we can't switch the arguments anymore

And we also can't create invalid instances of our value classes

But creating a developer has become slightly more cumbersome

```scala
(maybeName, maybeHandle) match {
  case (Some(name), Some(handle)) => Some(Developer(name, handle))
  case _                          => None
}
```
--

```scala
import cats.Apply
import cats.implicits._

Apply[Option].map2(maybeName, maybeHandle)(Developer.apply _)

(maybeName, invalidHandle).mapN(Developer.apply _)

```
???

smart constructors are great, but I do have a couple of concerns:

---
# Smart constructors concerns

* Our values are always wrapped in an Option

* Even though sometimes we statically know these are valid values

???
I have got a literal "@kwarkk" value in my scala source code.

I can see that it is a valid TwitterHandle, so surely the compiler, which is usually way smarter than me

should also be able to figure this out

* Boilerplate validation logic

---
#Idea: encode validations at the typelevel .image-200[![Idea](https://encrypted-tbn0.gstatic.com/images?q=tbn:ANd9GcRRFVNLa-nEYwfufPyCpabTcrcChYY9q0aVuBLWtCMU5IMyE7ZF0g)]

* This is the basic idea behind [refinement types](https://en.wikipedia.org/wiki/Refinement_%28computing#29#Refinement_types):

> *"In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type."*

???
So, what if we could take the idea of smart constructors

and encode our validations at the typelevel

A refinement type is just some basic type with a predicate (or a validation rule) which should be true for all valid values.

---
#Refinement type  basics

* refinement type =
 **base type** +
 **predicate**

* values of a refinement type = all values of the base type that
 **satisfy the predicate**

Examples:

* `TwitterHandle = String + (∀ s => s.startsWith("@"))`

* `Name          = String + (∀ s => s.nonEmpty)`

---
# Refined

There already exists a Scala [refined](https://github.com/fthomas/refined) library by Frank Thomas.

```
libraryDependencies += "eu.timepit" %% "refined" % "0.9.0"
```
--

```scala
import eu.timepit.refined.api.Refined
import eu.timepit.refined.collection.NonEmpty
import eu.timepit.refined.string.StartsWith
import eu.timepit.refined.W

object refinements {

type Name = Refined[String, NonEmpty]

type TwitterHandle = String Refined StartsWith[W.`"@"`.T]

final case class Developer(name: Name, twitterHandle: TwitterHandle)

}
```
???

Refined library provides us with a type constructor

Type that takes two type parameters and constructs a new type

point out base type and predicate

infix notation for readability

make good use of a type alias: avoids repeated typing and makes are code more readable

predicate with a value as a type parameters

--
Some predicates require encoding literals at the type-level

We use [Shapeless Witness macro](https://github.com/milessabin/shapeless/wiki/Feature-overview:-shapeless-2.0.0#singleton-typed-literals) to achieve this

---
# Sidebar: Literal based singleton types .image-200[![Pop quiz](./iStock_71171629_SMALL.jpg)]

Pop quiz: How many types does the value: `"foo"` belong to?

1, 2, 3, 4, more ?

Answer is 4:
--
  `String`
--
  `Any`
--
  `AnyRef`
--
  `"foo"`

???

Any (top type), AnyRef (because String is also a reference type)

String and the actual value is also a type

singleton type is a type inhabited by a single value

There is a [SIP](http://docs.scala-lang.org/sips/pending/42.type.html) to expose these literal based singleton types

```scala
type TwitterHandle = String Refined StartsWith["@"]
```

This is already available in:
* [Dotty](http://dotty.epfl.ch/docs/reference/singleton-types.html)
* [Typelevel scala (-Yliteral-types)](https://typelevel.org/scala/)
* [2.13.0-M3](https://github.com/scala/scala/pull/5310)

---
## Try it out by yourself

```scala
curl -s https://raw.githubusercontent.com/typelevel/scala/typelevel-readme/try-typelevel-scala.sh | bash
Loading...
Welcome to the Ammonite Repl 1.0.3
(Scala 2.12.4-bin-typelevel-4 Java 1.8.0_152)
If you like Ammonite, please support our development at www.patreon.com/lihaoyi
@ repl.compiler.settings.YliteralTypes.value = true

@ val x = "foo"
x: String = "foo"

@ x.isInstanceOf[String]
res2: Boolean = true

@ x.isInstanceOf[Any]
res3: Boolean = true

@ x.isInstanceOf[AnyRef]
res4: Boolean = true

@ x.isInstanceOf["foo"]
res5: Boolean = true

@ x.isInstanceOf["bar"]
res6: Boolean = false
```

???
You can launch an Ammonite instant repl with the Typelevel compiler and try this out yourself

---
# Refining literal values at compile time

Using a magic macro: `import eu.timepit.refined.auto._`

```scala
scala>"Peter Mortier": refinements.Name
res0: refinements.Name = Peter Mortier
```
???
Let's see if Refinement types can address our concerns

validation logic is declarative (we didn't write any actual validation code)

literal values can be automatically converted to refined type

Invalid literal => compilation error

```scala
scala> "foo": refinements.TwitterHandle
<console>:15: error: Predicate failed: "foo".startsWith("@").
 "foo": refinements.TwitterHandle
```

---
#Creating a Developer from literal values is now easier than ever!

```scala
import eu.timepit.refined._
import eu.timepit.refined.auto._

refinements.Developer("Peter Mortier", "@kwarkk") // Hell yeah
```
--
And swapping arguments fails to compile

```scala
refinements.Developer("@kwarkk", "Peter Mortier") // Does not compile, sweet
```

---
# Manually refine if this is too much magic

```scala
import eu.timepit.refined.api.RefType
```

```scala
scala> RefType.applyRefM[refinements.Name]("Peter Mortier")
res4: refinements.Name = Peter Mortier
```

```scala
scala> RefType.applyRefM[refinements.TwitterHandle]("wrong")
<console>:29: error: Predicate failed: "wrong".startsWith("@").
 RefType.applyRefM[refinements.TwitterHandle]("wrong")
 ^
```
---
# Refining runtime values

Most of the time however we don't have literals available

```scala
scala> val name: String = "Peter Mortier"
name: String = Peter Mortier

scala> RefType.applyRef[refinements.Name](name)
res6: Either[String,refinements.Name] = Right(Peter Mortier)
```

```scala
scala> val handle: String = "wrong"
handle: String = wrong

scala> RefType.applyRef[refinements.TwitterHandle](handle)
res7: Either[String,refinements.TwitterHandle] = Left(Predicate failed: "wrong".startsWith("@").)
```

---
# Refining with RefinedTypeOps

* new since refined `0.8.5`

```scala
import eu.timepit.refined.numeric.Positive
import eu.timepit.refined.api.RefinedTypeOps

type PosInt = Int Refined Positive
object PosInt extends RefinedTypeOps[PosInt, Int]

val five: PosInt = PosInt(5)
val result: Either[String, PosInt] = PosInt.from(4)
```

* `def apply(t: T): RT` => compile time refinement
* `def from(t: T): Either[String, RT]` => runtime refinement
* `def unapply(t: T): Option[RT]` => pattern matching

???
single line of boilerplate required

---
# Refinement recap

* Using ** eu.timepit.refined.api.RefType **

|                |                                  |
| -------------  | ---------------                  |
| compile time   | `RefType.applyRefM[RT](t: T): RT` |
| runtime        | `RefType.applyRef[RT](t: T): Either[String, RT]`  |

--
 
* Using ** refined type's companion **

|                |                                  |
| -------------  | ---------------                  |
| compile time   | `RT.apply(t: T): RT` |
| runtime        | `RT.from(t: T): Either[String, RT]`  |

---
class: center, middle
# Predicates in refined

---
# Char predicates

In package `eu.timepit.refined.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 |
???
Refined comes with a built-in set of predicates
Won't go over these in detail, but I'll just point out a couple of them
---
# Numeric predicates

In package `eu.timepit.refined.numeric`

|                             |                                                 |
| -------------               | ---------------                                 |
| `Less[N]`                   | checks if number is less than `N`                |
| `LessEqual[N]`              | checks if number is less than or equal to `N`    |
| `Greater[N]`                | checks if number is greater than `N`             |
| `GreaterEqual[N]`           | checks if number is greater than or equal to `N` |
| `Positive`                  | checks if number is greater than zero            |
| `NonPositive`               | checks if number is zero or negative             |
| `Negative`                  | checks if number is less than zero               |
| `NonNegative`               | checks if number is zero or positive             |
| `Odd`                       | checks if number is odd                          |
| `Even`                      | checks if number is even                         |
| `Modulo[N, O]`              | checks if number modulo `N` is `O`               |
| `Divisible[N]`              | checks if number is divisible by `N`             |
| `NonDivisible[N]`           | checks if number is NOT divisible by `N`         |

---
# Numeric interval predicates

In package `eu.timepit.refined.numeric`

|                             |                                                 |
| -------------               | ---------------                                 |
| `Interval.Open[L, H]`       | checks if number is in the interval (`L`, `H`)   |
| `Interval.OpenClosed[L, H]` | checks if number is in the interval (`L`, `H`]   |
| `Interval.ClosedOpen[L, H]` | checks if number is in the interval [`L`, `H`)   |
| `Interval.Closed[L, H]`     | checks if number is in the interval [`L`, `H`]   |
???
Difference between intervals is inclusive/exclusive
---
# String predicates
In package `eu.timepit.refined.string`

|                     |                                                         |
| -------------       | ---------------                                         |
| `StartsWith[S]`     | checks if string starts with the prefix `S`         |
| `EndsWith[S]`       | checks if string ends with the suffix `S`           |
| `MatchesRegex[S]`   | checks if string matches the regular expression `S` |
| `Regex`             | checks if string is a valid regular expression      |
| `Uri`               | checks if string is a valid URI                     |
| `Url`               | checks if string is a valid URL                     |
| `Uuid`              | checks if string is a valid UUID                    |
| `Xml`               | checks if string is valid XML                       |
| `XPath`             | checks if string is a valid XPath expression        |
???
StartsWith[S]
MatchesRegex[S]
---
# Collection predicates
In package `eu.timepit.refined.collection`

|                     |                                                         |
| -------------       | ---------------                                         |
| `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` |

---
# More Collection predicates
In package `eu.timepit.refined.collection`

|                     |                                                         |
| -------------       | ---------------                                         |
| `Size[P]`           | checks if the size of a `Traversable` satisfies the predicate `P`                  |
| `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`                                               |
| `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`                 |

---
# Logical (Boolean) predicates
In package `eu.timepit.refined.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`         |

---
exclude: true
# Predefined Refined types

* `eu.timepit.refined.types.char`: `LowerCaseChar`, `UpperCaseChar`

* `eu.timepit.refined.types.string`: `NonEmptyString`, `FiniteString[N]`

* `eu.timepit.refined.types.numeric`: `PosInt`, `NonNegInt`, `NegInt`, ...

* `eu.timepit.refined.types.net`: `PortNumber`, `SystemPortNumber`, ...

* `eu.timepit.refined.types.time`: `Month`, `Day`, `Hour`, `Minute`, `Second`, `Millis`

---
# Combining predicates

Simple predicates can be combined using the boolean predicates into a more complex predicate.

Our predicate for `TwitterHandle` is not precise enough.

According to [Twitter's support page](https://support.twitter.com/articles/101299#error):

* Usernames containing the words 'Twitter' or 'Admin' cannot be claimed.
* Your username cannot be longer than 15 characters. (not including '@')
* A username can only contain alphanumeric characters (letters A-Z, numbers 0-9) with the exception of underscores

---
# Improved `TwitterHandle`

```scala
import eu.timepit.refined.api.Refined
import eu.timepit.refined.boolean.{AllOf, Not, Or, And}
import eu.timepit.refined.string.{MatchesRegex, StartsWith}
import eu.timepit.refined.W
import eu.timepit.refined.char.LetterOrDigit
import eu.timepit.refined.collection.{NonEmpty, MaxSize, Tail}
import eu.timepit.refined.generic.Equal
import shapeless.::
import shapeless.HNil

object improved {

type TwitterHandle = String Refined AllOf[
    StartsWith[W.`"@"`.T] ::
    MaxSize[W.`16`.T] ::
    Not[MatchesRegex[W.`"(?i:.*twitter.*)"`.T]] ::
    Not[MatchesRegex[W.`"(?i:.*admin.*)"`.T]] ::
    Tail[Or[LetterOrDigit, Equal[W.`'_'`.T]]] ::
    HNil
  ]

type Name = String Refined And[NonEmpty, MaxSize[W.`256`.T]]

}
```

???
uses Shapeless HList to encode a list at the typelevel
declarative way to specify my validations
---
# Storing/Retrieving refined values

* We'll use Slick to retrieve/store Developers from an SQL database

* We need to map our Developer case class from/to a DB table using Slick's DSL

```scala
object Schema {

import slick.jdbc.H2Profile.api._

class Developers(tag: Tag) extends Table[Developer](tag, "developers") {
    def twitter = column[TwitterHandle]("twitter", O.PrimaryKey)
    def name    = column[Name]("name")

def * = (twitter, name).mapTo[Developer]
  }

val developers = TableQuery[Developers]

}
```

???

for this we create a Schema object

first we'll import the slick profile

Even though slick uses JDBC underneath, there are still difference in SQL dialect and the way different databases encode data types,
so slick needs to know which database you are using

Next, we do the actually mapping by creating a class which extends the Table

We also need to map our case class members to database columns

star projection is used to tell Slick which column maps to which case class member

finally we'll create a TableQuery, which will allow us to interact with actual database

http://slick.lightbend.com/doc/3.2.1/concepts.html#profiles:
Even when using a standard interface for database drivers like JDBC
there are many differences between databases in the SQL dialect they understand,
the way they encode data types, or other idiosyncracies.
Slick abstracts over these differences with profiles.

https://stackoverflow.com/questions/31849946/scala-slick-table-tag

only difference with non-refined types: is column[XXX]

---
# Standard mappings don't work

```scala
could not find implicit value for parameter tt:
    slick.ast.TypedType[improved.TwitterHandle]
    def twitter = column[TwitterHandle]("twitter", O.PrimaryKey)
                                       ^
could not find implicit value for parameter tt:
    slick.ast.TypedType[improved.Name]
    def name    = column[Name]("name")
                              ^
two errors found
(core/compile:compile) Compilation failed
```

It looks like Slick does not know how to map our refined types from/to SQL types.
---
# Custom Slick mappings

Let's fix that by writing some custom mappings

```scala
import eu.timepit.refined.api.Refined
import improved.TwitterHandle

implicit val twitterMapping = MappedColumnType.base[TwitterHandle, String](
  _.value, Refined.unsafeApply
)
```

`Refined.unsafeApply` is an escape hatch!
???

Let's fix that with a custom Slick mapping

That is a way to tell slick how to convert between a Refined type and its base type and vice versa

We call the base method on MappedColumnType with two type parameters

and we need to provide two functions

```scala
implicit val twitterMapping = MappedColumnType.base[TwitterHandle, String](
  _.value, v => RefType.applyRef[Name](v) match { 
    case Right(rt) => rt
    case Left(e)   => throw new SQLException(s"can not refine '$v'", e)
  }
)
```

This will protect you from reading DB rows, which don't pass the predicate
???

Refined.unsafeApply lifts your base type to a refined type without running any validations

Use with extreme caution

---
# Custom Slick mappings

Now we can store refined values!

```scala
val jdbcUrl = "jdbc:h2:mem:test-refined;DB_CLOSE_DELAY=-1"
val db = Database.forURL(jdbcUrl, driver = "org.h2.Driver")

db.run(developers.insert(developer))
```
???
A Database object encapsulates the resources that are required to connect to a specific database.

This can be just a number of connection parameters but in most cases it includes a connection pool and a thread pool.

--
However slick queries are still a problem!

`SELECT * FROM developers WHERE twitter like '%k%';`

```scala
db.run(developers.filter(_.twitter.like("%k%")).result)

[error] value like is not a member of slick.lifted.Rep[improved.TwitterHandle]
[error]     db.run(developers.filter(_.twitter.like("%kwa%")).result)
```
???

We want to find all developers with a twitter username containing the letter k

We use slick's collection like DSL

Unfortunately this does not compile out of the box

Convince the compiler that `twitter` is actually a `Rep[String]`

```scala
db.run(developers.filter(_.twitter.asInstanceOf[Rep[String]].like("%k%")).result)
```

---
# Integration library for Refined and Slick

```scala
libraryDependencies += "be.venneborg" %% "slick-refined" % "0.2.0"
```

[slick-refined](https://github.com/kwark/slick-refined) provides:

* boilerplate-free mapping support for Refined types

* extension methods to enable SQL operations on lifted `Rep[RefinedType]`

* support for mapping results from plain SQL queries

---
#Refined Slick Profile

```scala
import slick.jdbc.H2Profile
import be.venneborg.refined.{RefinedMapping, RefinedSupport}

trait MyRefinedSlickProfile extends H2Profile
  with RefinedMapping
  with RefinedSupport {

override val api = new API with RefinedImplicits

}

object MyRefinedSlickProfile extends MyRefinedSlickProfile
```
???
We need to extend the default H2Profile

If you ever worked with slick-pg, extension library for Slick and postgres

https://github.com/scala/bug/issues/10477

---
# Refined Schema
```scala
object RefinedSchema {

import MyRefinedSlickProfile.api._
  import MyRefinedSlickProfile.mapping._

class Developers(tag: Tag) extends Table[Developer](tag, "developers") {
    def twitter = column[TwitterHandle]("twitter", O.PrimaryKey)
    def name    = column[Name]("name")

def * = (name, twitter).mapTo[Developer]
  }

val developers = TableQuery[Developers]

}
```
---
# Storing and querying for refined types works out of the box

Storing a developer in the DB
```scala
db.run(developers += developer)
```

Retrieving a developer from the DB using a slick query
```scala
db.run(developers.filter(_.twitter.like("%kwa%")).result)
```
---
# Plain SQL query support

> *As an alternative to Scala queries you can write queries and other database statements in SQL. This is done with string interpolators.*

```scala
import be.venneborg.refined.RefinedPlainSql._

db.run(sql"""SELECT NAME FROM DEVELOPERS
    WHERE TWITTER LIKE '%rk'""".as[Name])

db.run(sqlu"""UPDATE DEVELOPERS SET NAME = 'Peter DM Mortier'
    WHERE TWITTER = '@kwarkk'""")
```
---
# Json serialization

### Let's use Play Json

```scala
import play.api.libs.json.Json

implicit val developerFormat = Json.format[Developer]

Json.toJson(Developer("Peter Mortier", "@kwarkk"))
```

???
We are going to ask Play to automatically derive a Json formatter for our Developer class

Play uses a macro to inspect the Developer case class

and for every member of case class will try find a JSON formatter

--
```scala
No instance of play.api.libs.json.Format is available
    for eu.timepit.refined.api.Refined[java.lang.String,
            eu.timepit.refined.boolean.And[eu.timepit.refined.boolean.Not[eu.timepit.refined.collection.Empty], eu.timepit.refined.collection.Size[eu.timepit.refined.boolean.Not[eu.timepit.refined.numeric.Greater[scala.Int]]]]],
        eu.timepit.refined.api.Refined[java.lang.String,
            eu.timepit.refined.boolean.AllOf[shapeless.$colon$colon[eu.timepit.refined.string.StartsWith[java.lang.String], shapeless.$colon$colon[eu.timepit.refined.collection.Size[eu.timepit.refined.boolean.Not[eu.timepit.refined.numeric.Greater[scala.Int]]], shapeless.$colon$colon[eu.timepit.refined.boolean.Not[eu.timepit.refined.string.MatchesRegex[java.lang.String]], shapeless.$colon$colon[eu.timepit.refined.boolean.Not[eu.timepit.refined.string.MatchesRegex[java.lang.String]], shapeless.$colon$colon[eu.timepit.refined.collection.Tail[eu.timepit.refined.boolean.Or[eu.timepit.refined.boolean.Or[eu.timepit.refined.char.Letter, eu.timepit.refined.char.Digit], eu.timepit.refined.generic.Equal[scala.Char]]], shapeless.HNil]]]]]]]
in the implicit scope (Hint: if declared in the same file, make sure it's declared before)
```
---
# Manual Json Format

```scala
import play.api.libs.json._
import improved_refinements._

implicit val twitterHandleFormat = new Format[TwitterHandle] {

override def reads(json: JsValue) = json.validate[String] flatMap { s =>
    RefType.applyRef[TwitterHandle](s) match {
      case Right(v)   => JsSuccess(v)
      case Left(err)  => JsError(err)
    }
  }

override def writes(handle: TwitterHandle) = JsString(handle.value)

}
```
???
create a new Format and implement two methods

--
* Reasonably easy code to understand/write

* But lots of boilerplate if we need to write this for every refined type

---
# Manual Form binding

```scala
import improved_refinements._
import eu.timepit.refined.api.RefType
import play.api.data.FormError
import play.api.data.format.Formatter

implicit val twitterHandleFormatter = new Formatter[TwitterHandle] {

override def bind(key: String, data: Map[String, String]):
    Either[Seq[FormError], TwitterHandle] = {
    data.get(key) match {
      case None    => Left(Seq(FormError(key, "error.required")))
      case Some(v) => RefType.applyRef[TwitterHandle](v) match {
        case Right(v)     => Right(v)
        case Left(error)  => Left(Seq(FormError(key, error)))
      }
    }

}

override def unbind(key: String, value: TwitterHandle) =
    Map[String, String](key -> value.value)

}
```
---
# Play-refined integration library

```scala
libraryDependencies += "be.venneborg" %% "play26-refined" % "0.2.0"
```
--

[play-refined](https://github.com/kwark/play-refined) provides:

* boilerplate-free JSON serialization/deserialization support for refined types

* boilerplate-free form binding/unbinding for refined types

* Path/Query binding for refined types in `routes`: 
 `/developers/:handle => controller.lookup(handle)`

* Translation of Refined error messages to standard Play error codes
---
# No more boilerplate

```scala
import improved_refinements._
import be.venneborg.refined.play.RefinedJsonFormats._
import play.api.libs.json._

implicit val developerFormat = Json.format[Developer]

Json.
  parse("""{ "name": "Peter Mortier", "twitterHandle": "@kwarkk" }""").
  as[Developer]
```

--
```
import improved_refinements._
import be.venneborg.refined.play.RefinedForms._

val developerForm = Form(
  mapping(
    "name"   -> Forms.of[Name],
    "handle" -> Formsof[TwitterHandle]
  )(Developer.apply)(Developer.unapply)
)

developerForm.
    bind(Map("name" -> "Peter Mortier", "handle" -> "@kwarkk"))

```
???
Uniform validation across json/forms
---
# Extension methods

* What if you need to perform operations on Refined types?

???

Lot's of the time the above is enough

You can simply take values from a REST api, refine them at runtime and store them in your database

But sometimes you need to do more with them, like call actual operations on them

* Use Typeclass pattern

---
# RefinedStringOps

```scala
import eu.timepit.refined.types.string._

trait RefinedStringOps[T] {
  def concat(x: T, y: T): T
}

implicit val refinedNonEmptyStringOps = new RefinedStringOps[NonEmptyString] {

override def concat(x: NonEmptyString, y: NonEmptyString): NonEmptyString =
    NonEmptyString.unsafeFrom(x.value + y.value)

}
```
---
# RefinedIntOps

```scala
import eu.timepit.refined.types.numeric._

trait RefinedIntOps[T] {
  def unsafeAdd(t1: T, t2: T): T
  def add(t1: T, t2: T): Option[T]
}

implicit val refinedPosIntOps = new RefinedIntOps[PosInt] {

override def unsafeAdd(x: PosInt, y: PosInt): PosInt =
    PosInt.unsafeFrom(x.value + y.value)

override def add(x: PosInt, y: PosInt): Option[PosInt] =
    PosInt.unapply(x.value + y.value)

}
```
???

use property-based testing with scalacheck to check your assumptions: show RefinedOpsTest

---
# Discriminating refined types

```scala
scala> val firstName: Name = "Peter"
firstName: improved_refinements.Name = Peter

scala> val lastName: Name = "Mortier"
lastName: improved_refinements.Name = Mortier
```
--
How can I prevent swapping bugs?

Using type aliases?
--
 no

Using a value class?

```scala
class FirstName(val name: Name) extends AnyVal
```

```scala
error: value class may not wrap another user-defined value class
       class FirstName(val name: Name) extends AnyVal
```

---
# Newtype

In Haskell:

> *A common programming practice is to define a type whose representation is identical to an existing one but which has a separate identity in the type system.
In Haskell, the newtype declaration creates a new type from an existing one.*

In scala use tagging:

> *Tag instances with arbitrary types. Useful if you'd like to differentiate between instances on the type level without runtime overhead.
  Tags are only used at compile-time to provide additional type safety.*

Different tagging libraries:

* [SoftwareMill](https://github.com/softwaremill/scala-common#tagging): lastest version `2.2.1` works
  * [Supertagged](https://github.com/rudogma/scala-supertagged)
  * [Shapeless](https://github.com/milessabin/shapeless/blob/4bf0263d402f852c4786111796cdcf869fe3bd65/core/src/main/scala/shapeless/typeoperators.scala#L25): unfortunately current version can NOT tag value classes

---
# Let's take supertagged for a spin

```scala
libraryDependencies += "org.rudogma" %% "supertagged" % "1.4",
```

```scala
import supertagged._
import improved_refinements._
import eu.timepit.refined.types.numeric.PosLong

trait DeveloperIdTag
type DeveloperId = PosLong @@ DeveloperIdTag

trait FirstNameTag
type FirstName = Name @@ FirstNameTag

val firstName: Name @@ FirstNameTag = tag[FirstNameTag](Name("Peter"))

val anotherFirstName: FirstName =
  tag[FirstNameTag](Name("Bart")).asInstanceOf[FirstName]
```

---
# Getting rid of asInstanceOf

```scala
class TaggedTypeOps[TT, T, U](implicit ev: @@[T, U] =:= TT) {
  def apply(t: T): TT = tag[U](t).asInstanceOf[TT]
}

trait DeveloperIdTag
type DeveloperId = PosLong @@ DeveloperIdTag
object DeveloperId extends TaggedTypeOps[DeveloperId, PosLong, DeveloperIdTag]

val myId: DeveloperId = DeveloperId(PosLong(5))
```

---
# supertagged Developer

```scala
import supertagging._

case class Developer(id: Option[DeveloperId],
                     twitterHandle: TwitterHandle,
                     firstName: FirstName,
                     lastName: LastName)
```
---
# supertagged schema

```scala
object SupertaggedSchema {

import MyRefinedSlickProfile.api._
  import MyRefinedSlickProfile.mapping._

// some necessary boilerplate. I haven't found a way (yet) to get rid of this
  implicit val developerIdIso =
    new Isomorphism[DeveloperId, PosLong](identity, DeveloperId(_))
  implicit val firstNameIso =
    new Isomorphism[FirstName, Name](identity, FirstName(_))
  implicit val lastNameIso =
    new Isomorphism[LastName, Name](identity, LastName(_))

class Developers(tag: Tag) extends Table[Developer](tag, "DEVELOPERS") {
    def id = column[DeveloperId]("ID", O.PrimaryKey, O.AutoInc)
    def twitter = column[TwitterHandle]("TWITTER")
    def firstName    = column[FirstName]("FIRSTNAME")
    def lastName    = column[LastName]("LASTNAME")

def * = (id.?, twitter, firstName, lastName).mapTo[Developer]
  }

val developers = TableQuery[Developers]

}
```
---
# Storing/querying supertagged Developer

```scala
val developer = Developer(
  None,
  TwitterHandle("@kwarkk"),
  FirstName(Name("Peter")),
  LastName(Name("Mortier"))
)
```

```scala
db.run(developers.insert(developer))

db.run(developers
  .filter(_.firstName.asInstanceOf[Rep[Name]].ilike("%ete%"))
  .result
)
```
---
# Json serialization of supertagged Developer

```scala
implicit def taggedReads[T, U](implicit reads: Reads[T]): Reads[T @@ U] =
    reads.map(tag[U].apply(_))

implicit val developerFormat = Json.format[Developer]

Json.toJson(developer)
```

---
# Refined gotcha's

--
* Intellij squiggly lines

.image-half[![Witness](./witness_macro_intellj.png)]
.image-half[![Macro](refined_auto_macro_intellij.png)]

squigglies are gone in latest releases `2018.1.x` !!!

--
* Watch-out when using infix type notation!

<del>`String Refined XXX And YYY`</del> 
`String Refined And[XXX, YYY]` 
`String Refined (XXX And YYY)`

* Refined primitives are always boxed

* Validation error messages are not always clear: `Empty did not fail`

* Watch your compile times!

???

implicit search is involved + inductive proofs are involved

https://scastie.scala-lang.org/kwark/0v3U5OtSSlCypBxeCJoLrA

https://github.com/fthomas/refined/blob/master/modules/scalaz/jvm/src/test/scala-2.12/eu/timepit/refined/scalaz/RefineJavapSpec.scala

opaque types SIP

---
# Refined advantages

* Typesafety++ (catch bugs at compile time)

* Uniform, declarative validation

* compile time refinement of literal values

---
# Alternatives

* [Bond](https://github.com/fwbrasil/bond)

* [scalactic](http://www.scalactic.org/): `PosInt, PozInt`

---
# Refined integrations

### Configuration
* [PureConfig](https://github.com/fthomas/refined)
* [Validated Typesafe Configuration](https://github.com/carlpulley/validated-config)
* [Ciris](https://github.com/vlovgr/ciris)

### Testing
* [scalacheck](https://github.com/fthomas/refined)

### Database access
* [Slick](https://github.com/kwark/slick-refined)
* [Doobie](https://github.com/tpolecat/doobie)
* [Anorm](https://github.com/derekmorr/refined-anorm)

---
# More refined integrations

### Json
* [Circe](https://github.com/circe/circe)
* [Argonaut Shapeless](https://github.com/alexarchambault/argonaut-shapeless)
* [Play Json](https://github.com/lunaryorn/play-json-refined)
* [Play](https://github.com/kwark/play-refined)

### Other
* [Monocle](https://github.com/julien-truffaut/Monocle) -- lens library
* [Decline](https://github.com/bkirwi/decline) -- command line parsing
* [Scopt](https://github.com/fthomas/refined)  -- command line parsing
* [Quasar](https://github.com/quasar-analytics/quasar) -- NoSql analytics engine
* [kantan.codecs](https://github.com/nrinaudo/kantan.codecs) -- Codecs f.e. for CSV parsing
---
# Refined presentations

* [Decorate your types with refined - Frank Thomas](https://www.youtube.com/watch?v=zExb9x3fzKs&t=1501s)

* [Refined types for validated configurations = Viktor Lövgren](https://www.youtube.com/watch?v=C3ciegxMAqA)

* [Leif Wickland, Defusing the configuration time bomb with PureConfig and Refined](https://www.youtube.com/watch?v=NjqRi-cF3-g)

* Links to even more resources in [Refined wiki](https://github.com/fthomas/refined/wiki/Resources)

---
class: center, middle

.image-half[![Static typing](./degoes_tweet.png)]

---
class: center, middle

# Thanks!
Code and slides at `kwark/refined-in-practice-bescala` on GitHub

Presentation available at https://kwark.github.io/refined-in-practice-bescala

???

Static typing debate is actually pretty silly

I think the more you can prove about your program before you run it, the better of you are

And refinement types help you achieve this

But they do come with a cost

cost of integrating them with other frameworks

cost of typelevel programming

Thanks to:

Frank for creating refined

Miles Sabin for his incredible work on the scala/typelevel compiler:

driving the literal based singleton types SIP

improving the implicit search algo in the compiler

And all other developers that created these awesome integration libraries

And finally I want to thank you for coming to my talk

## Questions?

You can always find me later in the refined gitter room: https://gitter.im/fthomas/refined