Skip to content

Commit

Permalink
dev: Add snippet checking to reference pages
Browse files Browse the repository at this point in the history
  • Loading branch information
Iltotore committed Sep 13, 2023
1 parent 00683a0 commit afb875f
Show file tree
Hide file tree
Showing 5 changed files with 232 additions and 17 deletions.
2 changes: 2 additions & 0 deletions docs/_docs/reference/constraint.md
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,7 @@ Here is how it looks:
```scala sc:nocompile sc-name:PositiveAndConstraint.scala sc-compile-with:Positive.scala
//{
import io.github.iltotore.iron.*

//}
given Constraint[Int, Positive] with

Expand All @@ -80,6 +81,7 @@ you can use a trait to reduce boilerplate:
```scala sc:nocompile sc-compile-with:Positive.scala
//{
import io.github.iltotore.iron.*

//}
trait PositiveConstraint[A] extends Constraint[A, Positive]:
override inline def message: String = "Should be strictly positive"
Expand Down
49 changes: 47 additions & 2 deletions docs/_docs/reference/implication.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@ For example, the following code compiles due to [transitivity](https://en.wikipe
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Greater
//}

//}
val x: Int :| Greater[5] = ???
val y: Int :| Greater[0] = x
```
Expand All @@ -36,12 +36,25 @@ Note: implications are a purely compile-time mechanism.
For example, the following implication:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.any.Not

//}
given [C1]: (C1 ==> Not[Not[C1]]) = Implication()
```

allows us (if imported) to compile this code:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.any.Not
import io.github.iltotore.iron.constraint.numeric.Greater

given [C1]: (C1 ==> Not[Not[C1]]) = Implication()

//}
val x: Int :| Greater[0] = ???
val y: Int :| Not[Not[Greater[0]]] = x //C1 implies Not[Not[C1]]: `x` can be safely casted.
```
Expand All @@ -51,7 +64,13 @@ val y: Int :| Not[Not[Greater[0]]] = x //C1 implies Not[Not[C1]]: `x` can be saf
Almost every implication has a dependency. For example, our previous "double negation" implication doesn't work in the
following case:

```scala
```scala sc:nocompile
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.any.Not
import io.github.iltotore.iron.constraint.numeric.Greater

//}
val x: Int :| Greater[1] = ???

//Assuming that Greater[1] ==> Greater[0]
Expand All @@ -61,6 +80,11 @@ val y: Int :| Not[Not[Greater[0]]] = x
But it should. This can be fixed by using two different constraints linked by an implication:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.any.Not

//}
given [C1, C2](using C1 ==> C2): (C1 ==> Not[Not[C2]]) = Implication()
```

Expand All @@ -69,6 +93,14 @@ given [C1, C2](using C1 ==> C2): (C1 ==> Not[Not[C2]]) = Implication()
Our implication now depends on another implication: `C1 ==> C2`. With this implementation, our code now compiles:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.any.Not
import io.github.iltotore.iron.constraint.numeric.Greater

given [C1, C2](using C1 ==> C2): (C1 ==> Not[Not[C2]]) = Implication()

//}
val x: Int :| Greater[1] = ???

//Assuming that Greater[1] ==> Greater[0]
Expand All @@ -86,6 +118,11 @@ This can be combined with [[iron.ops|io.github.iltotore.iron.ops]] to create log
For example, we can implement the [transitive relation](https://en.wikipedia.org/wiki/Transitive_relation):

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Greater

//}
import io.github.iltotore.iron.compileTime.*

given [V1, V2](using V1 > V2 =:= true): (Greater[V1] ==> Greater[V2]) = Implication()
Expand All @@ -96,6 +133,14 @@ given [V1, V2](using V1 > V2 =:= true): (Greater[V1] ==> Greater[V2]) = Implicat
Now, the following code compiles:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.compileTime.*
import io.github.iltotore.iron.constraint.numeric.Greater

given [V1, V2](using V1 > V2 =:= true): (Greater[V1] ==> Greater[V2]) = Implication()

//}
val x: Int :| Greater[1] = ???
val y: Int :| Greater[0] = x //x > 1 and 1 > 0, so x > 0.
```
10 changes: 10 additions & 0 deletions docs/_docs/reference/iron-type.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,11 @@ used in set builders.
Refined types are subtypes of their unrefined form. For instance, `Int :| Greater[0]` is a subtype of `Int`.

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Greater

//}
val x: Int :| Greater[0] = ???
val y: Int = x //Compiles
```
Expand All @@ -28,6 +33,11 @@ val y: Int = x //Compiles
types overheadless.

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Greater

//}
val x: Int :| Greater[0] = ???
```

Expand Down
133 changes: 129 additions & 4 deletions docs/_docs/reference/newtypes.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,28 @@ You can create no-overhead new types like [scala-newtype](https://github.com/est
Iron provides a convenient trait called `RefinedTypeOps` to easily add smart constructors to your type:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

//}
type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]
```

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]

//}
val temperature = Temperature(15) //Compiles
println(temperature) //15

val positive: Int :| Positive = 15
val positive: Double :| Positive = 15
val tempFromIron = Temperature(positive) //Compiles too
```

Expand All @@ -28,6 +41,14 @@ val tempFromIron = Temperature(positive) //Compiles too
`RefinedTypeOps` supports [all refinement methods](refinement.md) provided by Iron:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]

//}
val unsafeRuntime: Temperature = Temperature.applyUnsafe(15)
val option: Option[Temperature] = Temperature.option(15)
val either: Either[String, Temperature] = Temperature.either(15)
Expand All @@ -36,20 +57,43 @@ val either: Either[String, Temperature] = Temperature.either(15)
Constructors for other modules exist:

```scala
val zioValidation: Temperature = Temperature.validation(15)
//{
import zio.prelude.Validation

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive
import io.github.iltotore.iron.zio.*

type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]

//}
val zioValidation: Validation[String, Temperature] = Temperature.validation(15)
```

Note: all these constructors are inline. They don't bring any overhead:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]

//}
val temperature: Temperature = Temperature(15)

val runtimeValue: Double = ???
val unsafeRuntime: Temperature = Temperature.applyUnsafe(runtimeValue)
```

compiles to

```scala
val temperature: Double = 15

val runtimeValue: Double = ???
val unsafeRuntime: Double =
if runtimeValue > 0 then runtimeValue
else throw new IllegalArgumentException("...")
Expand All @@ -62,10 +106,23 @@ constraint. [[Pure|io.github.iltotore.iron.constraint.any.Pure]] is an alias for
[[True|io.github.iltotore.iron.constraint.any.True]], a constraint that is always satisfied.

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.any.Pure

//}
type FirstName = String :| Pure
object FirstName extends RefinedTypeOps[FirstName]
```
```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.any.Pure

type FirstName = String :| Pure
object FirstName extends RefinedTypeOps[FirstName]

//}
val firstName = FirstName("whatever")
```

Expand All @@ -74,22 +131,47 @@ val firstName = FirstName("whatever")
The aliased type of an [opaque type](https://docs.scala-lang.org/scala3/book/types-opaque-types.html) is only known in its definition file. It is not considered like a type alias outside of it:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

//}
opaque type Temperature = Double :| Positive
```

```scala
```scala sc:nocompile
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

opaque type Temperature = Double :| Positive

//}
val x: Double :| Positive = 5
val temperature: Temperature = x //Error: Temperature expected, got Double :| Positive
```

Such encapsulation is especially useful to avoid mixing different domain types with the same refinement:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

//}
opaque type Temperature = Double :| Positive
opaque type Moisture = Double :| Positive
```

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

opaque type Temperature = Double :| Positive
opaque type Moisture = Double :| Positive

//}
case class Info(temperature: Temperature, moisture: Moisture)

val temperature: Temperature = ???
Expand All @@ -102,11 +184,24 @@ Therefore, it also forces the user to convert the value explicitly, for example
`RefinedTypeOps`:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

//}
opaque type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]
```

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

opaque type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]

//}
val value: Double :| Positive = ???

val a: Temperature = value //Compile-time error
Expand Down Expand Up @@ -141,17 +236,37 @@ object Foo:
def apply(value: String): Foo = value
```
```scala
//{
opaque type Foo <: String = String
object Foo:
def apply(value: String): Foo = value

//}
val x = Foo("abcd")
x.toUpperCase //"ABCD"
```

Therefore, you can combine it with `RefinedTypeOps`:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.all.*

//}
opaque type FirstName <: String :| ForAll[Letter] = String :| ForAll[Letter]
object FirstName extends RefinedTypeOps[FirstName]
```
```scala

```scala sc:nocompile
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.all.*

opaque type FirstName <: String :| ForAll[Letter] = String :| ForAll[Letter]
object FirstName extends RefinedTypeOps[FirstName]

//}
val x = FirstName("Raphael")
x.toUpperCase //"RAPHAEL"
```
Expand All @@ -162,6 +277,11 @@ Usually, transparent type aliases do not need a special handling for typeclass d
instances for `IronType`. However, this is not the case for opaque type aliases, for instance:

```scala
//{
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.Positive

//}
opaque type Temperature = Double :| Positive
object Temperature extends RefinedTypeOps[Temperature]
```
Expand All @@ -172,6 +292,11 @@ each `RefinedTypeOps`. It works the same as
from the [ZIO JSON module](https://iltotore.github.io/iron/docs/modules/zio-json.html):

```scala
//{
import zio.json.*
import io.github.iltotore.iron.*

//}
inline given[T](using mirror: RefinedTypeOps.Mirror[T], ev: JsonDecoder[mirror.IronType]): JsonDecoder[T] =
ev.asInstanceOf[JsonDecoder[T]]
```
Expand Down
Loading

0 comments on commit afb875f

Please sign in to comment.