|
| 1 | +/* |
| 2 | +13.2 Indexed Codata |
| 3 | +The basic idea of indexed codata is to prevent methods being called unless certain conditions, |
| 4 | +encoded in types, are met. More precisely, methods are guarded by type equalities that callers |
| 5 | +must prove they satisfy to call a method. The contextual abstraction features, given instances |
| 6 | +and using clauses, are used to implement this in Scala. |
| 7 | + */ |
| 8 | +trait On |
| 9 | +trait Off |
| 10 | + |
| 11 | +trait Switch[A]: |
| 12 | + def on(using ev: A =:= Off): Switch[On] |
| 13 | + def off(using ev: A =:= On): Switch[Off] |
| 14 | + |
| 15 | +final case class SimpleSwitch[A]() extends Switch[A]: |
| 16 | + /* |
| 17 | + If a given instance A =:= B exists, then the type A is equal to the type B. |
| 18 | + We never create these instances ourselves. Instead the compiler creates them for us. |
| 19 | + In the on method, we are asking the compiler to construct an instance A =:= Off, |
| 20 | + which can only be done if A is Off. This in turn means we can only call the method |
| 21 | + when the Switch is Off. This is the core idea of indexed codata: we reflect states as types, |
| 22 | + and restrict method calls to a subset of states. |
| 23 | + */ |
| 24 | + def on(using ev: A =:= Off): Switch[On] = |
| 25 | + SimpleSwitch() |
| 26 | + def off(using ev: A =:= On): Switch[Off] = |
| 27 | + SimpleSwitch() |
| 28 | + |
| 29 | +object SimpleSwitch: |
| 30 | + val on: Switch[On] = SimpleSwitch() |
| 31 | + val off: Switch[Off] = SimpleSwitch() |
| 32 | + |
| 33 | +SimpleSwitch.on.off |
| 34 | +SimpleSwitch.off.on |
| 35 | + |
| 36 | +// Doesn't compile. |
| 37 | +// SimpleSwitch.on.on |
| 38 | + |
| 39 | +// Exercise: Torque |
| 40 | +// Below is the definition of Length we previously used. Your mission is to: |
| 41 | + |
| 42 | +// 1. implement a type Force, parameterized by a phantom type that represents the units of force; |
| 43 | +// 2. implement a type Torque, parameterized by a phantom type that represents the units of torque; |
| 44 | +// 3. define types Newtons and NewtonMetres to represent force in SI units; |
| 45 | +// 4. implement a method * on Force that accepts a Length and returns a Torque. It can only be |
| 46 | +// called if the Force is in Newtons and the Length is in Metres. In this case the Torque is in |
| 47 | +// NewtonMetres. (Torque is force times length.) |
| 48 | + |
| 49 | +trait Newtons |
| 50 | +trait Metres |
| 51 | +trait NewtonMetres |
| 52 | + |
| 53 | +final case class Length[Unit](value: Double): |
| 54 | + def +(that: Length[Unit]): Length[Unit] = |
| 55 | + Length[Unit](this.value + that.value) |
| 56 | + |
| 57 | +final case class Torque[Unit](value: Double) |
| 58 | + |
| 59 | +final case class Force[Unit](value: Double): |
| 60 | + def *[L](length: Length[L])(using Unit =:= Newtons, L =:= Metres): Torque[NewtonMetres] = |
| 61 | + Torque(this.value * length.value) |
| 62 | + |
| 63 | +ch13.Html.empty.head |
| 64 | + .link("stylesheet", "styles.css") |
| 65 | + .title("Our Amazing Webpage") |
| 66 | + .body |
| 67 | + .h1("Where Amazing Exists") |
| 68 | + .p("Right here") |
| 69 | + .toString |
| 70 | + |
| 71 | +// Doesn't compile. |
| 72 | +// Html.empty.head |
| 73 | +// .link("stylesheet", "styles.css") |
| 74 | +// .body |
| 75 | +// .h1("This Shouldn't Work") |
| 76 | + |
| 77 | +ch13.html2.Html.empty |
| 78 | + .head(_.title("Our Amazing Webpage")) |
| 79 | + .body(_.h1("Where Amazing Happens").p("Right here")) |
| 80 | + .toString() |
| 81 | + |
| 82 | +// 13.2.2 Beyond Equality Constraints |
| 83 | +/* |
| 84 | +We can use <:< for evidence of a subtyping relationship, |
| 85 | +and NotGiven for evidence that no given instance exists |
| 86 | +(with which we can test that types are not equal, for example). |
| 87 | +Beyond that, we can view any given instance as evidence. |
| 88 | + */ |
| 89 | +trait Feet |
| 90 | +trait Pounds |
| 91 | +trait PoundsFeet |
| 92 | + |
| 93 | +// An instance exists if A * B = C |
| 94 | +trait Multiply[A, B, C] |
| 95 | +object Multiply: |
| 96 | + given Multiply[Metres, Newtons, NewtonMetres] = new Multiply {} |
| 97 | + given Multiply[Feet, Pounds, PoundsFeet] = new Multiply {} |
| 98 | + |
| 99 | + // Exercise: Commutivitiy |
| 100 | + // A * B == B * A |
| 101 | + given commutative: [A, B, C] => Multiply[A, B, C] => Multiply[B, A, C] = |
| 102 | + new Multiply {} |
| 103 | + |
| 104 | +final case class Length2[L](value: Double): |
| 105 | + def *[F, T](that: Force2[F])(using Multiply[L, F, T]): Torque[T] = |
| 106 | + Torque(this.value * that.value) |
| 107 | + |
| 108 | +final case class Force2[F](value: Double): |
| 109 | + def *[L, T](that: Length2[L])(using Multiply[F, L, T]): Torque[T] = |
| 110 | + Torque(this.value * that.value) |
| 111 | + |
| 112 | +Length2[Metres](3) * Force2[Newtons](4) |
| 113 | +Length2[Feet](3) * Force2[Pounds](4) |
| 114 | +// Commutative |
| 115 | +Force[Newtons](3) * Length[Metres](4) |
0 commit comments