-
-
Notifications
You must be signed in to change notification settings - Fork 1.2k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Browse files
Browse the repository at this point in the history
* Adds an As class which represents subtyping relationships This is a direct port of the Liskov class from scalaz. I named it `As` to be similar to our new `Is` class representing type equality, but there are aliases named `<~<` and `Liskov` * incorporate suggestions from Oscar (Thanksgit diff --cached)git * delete-trailing-whitespace * Minor changes to evidence/packages.scala remove explicit reference to package in Is type alias (for posco) add === type alias for `Is` (for sellout) * More enhancements for posco's feedback (thanks!) - change unsafeFromPredef to just use refl - add tests for some expected relationships such as Int <~< Any, and List[String] <~< List[Any] * ome more * add more tests, contravariant tests still pending * add contra tests and get rid fo the liftF like functions (they can be derrived from what we have, and I can't find anyone using them in the wild) * don't try to link the type in the scaladoc * fix test failure on 2.10.6 + scalajs Thank you very much @kailuowang for the solutiongit diff * added helper methods for converting Function1 * added category law tests
- Loading branch information
1 parent
219eecd
commit 2e01263
Showing
3 changed files
with
331 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,180 @@ | ||
package cats | ||
package evidence | ||
|
||
import arrow.Category | ||
|
||
/** | ||
* As substitutability: A better `<:<` | ||
* | ||
* This class exists to aid in the capture proof of subtyping | ||
* relationships, which can be applied in other context to widen other | ||
* type | ||
* | ||
* `A As B` holds whenever `A` could be used in any negative context | ||
* that expects a `B`. (e.g. if you could pass an `A` into any | ||
* function that expects a `B` as input.) | ||
* | ||
* This code was ported directly from scalaz to cats using this version from scalaz: | ||
* https://github.com/scalaz/scalaz/blob/a89b6d63/core/src/main/scala/scalaz/As.scala | ||
* | ||
* The original contribution to scalaz came from Jason Zaugg | ||
*/ | ||
sealed abstract class As[-A, +B] extends Serializable { | ||
/** | ||
* Use this subtyping relationship to replace B with a value of type | ||
* A in a contravariant context. This would commonly be the input | ||
* to a function, such as F in: `type F[-B] = B => String`. In this | ||
* case, we could use A As B to turn an F[B] Into F[A]. | ||
*/ | ||
def substitute[F[-_]](p: F[B]): F[A] | ||
|
||
@inline final def andThen[C](that: (B As C)): (A As C) = As.compose(that, this) | ||
|
||
@inline final def compose[C](that: (C As A)): (C As B) = As.compose(this, that) | ||
|
||
@inline final def coerce(a: A): B = As.witness(this)(a) | ||
} | ||
|
||
sealed abstract class AsInstances { | ||
import As._ | ||
|
||
/* | ||
* Subtyping forms a category | ||
*/ | ||
implicit val liskov: Category[As] = new Category[As] { | ||
def id[A]: (A As A) = refl[A] | ||
|
||
def compose[A, B, C](bc: B As C, ab: A As B): (A As C) = bc compose ab | ||
} | ||
} | ||
|
||
object As extends AsInstances { | ||
/** | ||
* In truth, "all values of `A Is B` are `refl`". `reflAny` is that | ||
* single value. | ||
*/ | ||
private[this] val reflAny = new (Any As Any) { | ||
def substitute[F[-_]](fa: F[Any]) = fa | ||
} | ||
/** | ||
* Subtyping is reflexive | ||
*/ | ||
implicit def refl[A]: (A As A) = | ||
reflAny.asInstanceOf[A As A] | ||
|
||
/** | ||
* We can witness the relationship by using it to make a substitution * | ||
*/ | ||
implicit def witness[A, B](lt: A As B): A => B = | ||
lt.substitute[-? => B](identity) | ||
|
||
/** | ||
* Subtyping is transitive | ||
*/ | ||
def compose[A, B, C](f: B As C, g: A As B): A As C = | ||
g.substitute[λ[`-α` => α As C]](f) | ||
|
||
/** | ||
* reify a subtype relationship as a Liskov relaationship | ||
*/ | ||
@inline def reify[A, B >: A]: (A As B) = refl | ||
|
||
/** | ||
* It can be convenient to convert a <:< value into a `<~<` value. | ||
* This is not strictly valid as while it is almost certainly true that | ||
* `A <:< B` implies `A <~< B` it is not the case that you can create | ||
* evidence of `A <~< B` except via a coercion. Use responsibly. | ||
*/ | ||
def fromPredef[A, B](eq: A <:< B): A As B = | ||
reflAny.asInstanceOf[A As B] | ||
|
||
/** | ||
* We can lift subtyping into any covariant type constructor | ||
*/ | ||
def co[T[+_], A, A2] (a: A As A2): (T[A] As T[A2]) = | ||
a.substitute[λ[`-α` => T[α] As T[A2]]](refl) | ||
|
||
// Similarly, we can do this any time we find a covariant type | ||
// parameter. Here we provide the proof for what we expect to be the | ||
// most common shapes. | ||
|
||
def co2[T[+_, _], Z, A, B](a: A As Z): T[A, B] As T[Z, B] = | ||
a.substitute[λ[`-α` => T[α, B] As T[Z, B]]](refl) | ||
|
||
/** | ||
* Widen a F[X,+A] to a F[X,B] if (A As B). This can be used to widen | ||
* the output of a Function1, for example. | ||
*/ | ||
def co2_2[T[_, +_], Z, A, B](a: B As Z): T[A, B] As T[A, Z] = | ||
a.substitute[λ[`-α` => T[A, α] As T[A, Z]]](refl) | ||
|
||
def co3[T[+_, _, _], Z, A, B, C](a: A As Z): T[A, B, C] As T[Z, B, C] = | ||
a.substitute[λ[`-α` => T[α, B, C] As T[Z, B, C]]](refl) | ||
|
||
def co3_2[T[_, +_, _], Z, A, B, C](a: B As Z): T[A, B, C] As T[A, Z, C] = | ||
a.substitute[λ[`-α` => T[A, α, C] As T[A, Z, C]]](refl) | ||
|
||
def co3_3[T[+_, _, +_], Z, A, B, C](a: C As Z): T[A, B, C] As T[A, B, Z] = | ||
a.substitute[λ[`-α` => T[A, B, α] As T[A, B, Z]]](refl) | ||
|
||
/** | ||
* Use this relationship to widen the output type of a Function1 | ||
*/ | ||
def onF[X, A, B](ev: A As B)(fa: X => A): X => B = co2_2[Function1, B, X, A](ev).coerce(fa) | ||
|
||
/** | ||
* widen two types for binary type constructors covariant in both | ||
* parameters | ||
* | ||
* lift2(a,b) = co1_2(a) compose co2_2(b) | ||
*/ | ||
def lift2[T[+_, +_], A, A2, B, B2]( | ||
a: A As A2, | ||
b: B As B2 | ||
): (T[A, B] As T[A2, B2]) = { | ||
type a[-X] = T[X, B2] As T[A2, B2] | ||
type b[-X] = T[A, X] As T[A2, B2] | ||
b.substitute[b](a.substitute[a](refl)) | ||
} | ||
|
||
/** | ||
* We can lift a subtyping relationship into a contravariant type | ||
* constructor. | ||
* | ||
* Given that F has the shape: F[-_], we show that: | ||
* (A As B) implies (F[B] As F[A]) | ||
*/ | ||
def contra[T[-_], A, B](a: A As B): (T[B] As T[A]) = | ||
a.substitute[λ[`-α` => T[B] As T[α]]](refl) | ||
|
||
// Similarly, we can do this any time we find a contravariant type | ||
// parameter. Here we provide the proof for what we expect to be the | ||
// most common shapes. | ||
|
||
def contra1_2[T[-_, _], Z, A, B](a: A As Z): (T[Z, B] As T[A, B]) = | ||
a.substitute[λ[`-α` => T[Z, B] As T[α, B]]](refl) | ||
|
||
def contra2_2[T[_, -_], Z, A, B](a: B As Z): (T[A, Z] As T[A, B]) = | ||
a.substitute[λ[`-α` => T[A, Z] As T[A, α]]](refl) | ||
|
||
def contra1_3[T[-_, _, _], Z, A, B, C](a: A As Z): (T[Z, B, C] As T[A, B, C]) = | ||
a.substitute[λ[`-α` => T[Z, B, C] As T[α, B, C]]](refl) | ||
|
||
def contra2_3[T[_, -_, _], Z, A, B, C](a: B As Z): (T[A, Z, C] As T[A, B, C]) = | ||
a.substitute[λ[`-α` => T[A, Z, C] As T[A, α, C]]](refl) | ||
|
||
def contra3_3[T[_, _, -_], Z, A, B, C](a: C As Z): (T[A, B, Z] As T[A, B, C]) = | ||
a.substitute[λ[`-α` => T[A, B, Z] As T[A, B, α]]](refl) | ||
|
||
/** | ||
* Use this relationship to narrow the input type of a Function1 | ||
*/ | ||
def conF[A, B, C](ev: B As A)(fa: A => C): B => C = | ||
contra1_2[Function1, A, B, C](ev).coerce(fa) | ||
|
||
/** | ||
* Use this relationship to widen the output type and narrow the input type of a Function1 | ||
*/ | ||
def invF[C, D, A, B](ev1: D As C, ev2: A As B)(fa: C => A): D => B = | ||
conF(ev1)(onF(ev2)(fa)) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,36 @@ | ||
package cats | ||
|
||
package object evidence { | ||
type Leibniz[A, B] = cats.evidence.Is[A, B] | ||
/** | ||
* A convenient type alias for Is, which declares that A is the same | ||
* type as B. | ||
*/ | ||
type ===[A, B] = A Is B | ||
|
||
/** | ||
* This type level equality represented by `Is` is referred to as | ||
* "Leibniz equality", and it had the name "Leibniz" in the scalaz | ||
* https://en.wikipedia.org/wiki/Gottfried_Wilhelm_Leibniz | ||
*/ | ||
type Leibniz[A, B] = A Is B | ||
|
||
/** | ||
* A convenient type alias for As, this declares that A is a | ||
* subtype of B, and should be able to be a B is | ||
* expected. | ||
*/ | ||
type <~<[-A, +B] = A As B | ||
|
||
/** | ||
* A flipped alias, for those used to their arrows running left to right | ||
*/ | ||
type >~>[+B, -A] = A As B | ||
|
||
/** | ||
* The property that a value of type A can be used in a context | ||
* expecting a B if A <~< B is refered to as the "Liskov | ||
* Substitution Principal", which is named for Barbara Liskov: | ||
* https://en.wikipedia.org/wiki/Barbara_Liskov | ||
*/ | ||
type Liskov[-A, +B] = A As B | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,119 @@ | ||
package cats | ||
package tests | ||
|
||
import cats.laws.discipline.{CategoryTests, SerializableTests} | ||
import org.scalacheck.{Arbitrary, Gen} | ||
import cats.arrow.Category | ||
class AsTests extends CatsSuite { | ||
import evidence._ | ||
|
||
def toMap[A, B, X](fa: List[X])(implicit ev: X <~< (A,B)): Map[A,B] = { | ||
type RequiredFunc = (Map[A, B], X) => Map[A, B] | ||
type GivenFunc = (Map[A, B], (A, B)) => Map[A, B] | ||
val subst: GivenFunc <~< RequiredFunc = As.contra2_3(ev) //introduced because inference failed on scalajs on 2.10.6 | ||
fa.foldLeft(Map.empty[A,B])(subst(_ + _)) | ||
} | ||
|
||
implicit def arbAs[A, B](implicit ev: A <~< B) = Arbitrary(Gen.const(ev)) | ||
implicit def eq[A, B]: Eq[As[A, B]] = Eq.fromUniversalEquals | ||
|
||
|
||
|
||
test("narrow an input of a function2") { | ||
// scala's GenTraversableOnce#toMap has a similar <:< constraint | ||
|
||
toMap(List("String" -> 1)) | ||
} | ||
|
||
test("lift <:") { | ||
// scala's GenTraversableOnce#toMap has a similar <:< constraint | ||
trait Bar | ||
case class Foo(x: Int) extends Bar | ||
|
||
val lifted: Foo <~< Bar = As.reify[Foo, Bar] | ||
toMap(List("String" -> Foo(1)))(As.co2_2(lifted)) | ||
} | ||
|
||
test("check expected relationships") { | ||
// scala's GenTraversableOnce#toMap has a similar <:< constraint | ||
implicitly[Int <~< Any] | ||
implicitly[String <~< Any] | ||
implicitly[String <~< AnyRef] | ||
implicitly[String <~< AnyRef] | ||
implicitly[(String,Int) <~< (AnyRef,Any)] | ||
implicitly[scala.collection.immutable.List[String] <~< scala.collection.Seq[Any]] | ||
} | ||
|
||
trait Top { | ||
def foo: String = this.getClass.getName | ||
} | ||
trait Middle extends Top | ||
case class Bottom() extends Middle | ||
|
||
checkAll("As[Bottom, Middle]", CategoryTests[As].category[Bottom, Middle, Top, Any]) | ||
checkAll("Category[As]", SerializableTests.serializable(Category[As])) | ||
|
||
test("subtyping relationships compose") { | ||
|
||
val cAsB: Bottom As Middle = As.reify[Bottom,Middle] | ||
val bAsA: Middle As Top = As.fromPredef(implicitly) | ||
|
||
val one: Bottom As Top = cAsB andThen bAsA | ||
val two: Bottom As Top = bAsA compose cAsB | ||
} | ||
|
||
test("we can use As to coerce a value") { | ||
val cAsA: Bottom As Top = implicitly | ||
|
||
val c: Bottom = Bottom() | ||
|
||
val a: Top = cAsA.coerce(c) | ||
a.foo | ||
} | ||
|
||
test("we can lift subtyping to covariant type constructors") { | ||
val cAsA: Bottom As Top = implicitly | ||
val co: List[Bottom] As List[Top] = As.co(cAsA) | ||
val co2: ((Bottom, String) As (Top, String)) = As.co2(cAsA) | ||
val co2_2: ((String, Bottom) As (String, Top)) = As.co2_2(cAsA) | ||
val co3: ((Bottom, Unit, Unit) As (Top, Unit, Unit)) = As.co3(cAsA) | ||
val co3_2: ((Unit, Bottom, Unit) As (Unit, Top, Unit)) = As.co3_2(cAsA) | ||
val co3_3: ((Unit, Unit, Bottom) As (Unit, Unit, Top)) = As.co3_3(cAsA) | ||
val lift2: ((Bottom, String) As (Top,Any)) = As.lift2(cAsA,implicitly) | ||
} | ||
|
||
test("we can lift subtyping to contravariant type constructors") { | ||
type Eat[-A] = A => Unit | ||
type EatF[-A, B] = A => B | ||
type Eatꟻ[B, -A] = A => B | ||
type EatF13[-A, B, C] = A => (B, C) | ||
type EatF23[B, -A, C] = A => (B, C) | ||
type EatF33[B, C, -A] = A => (B, C) | ||
|
||
val cAsA: (Bottom As Top) = implicitly | ||
val contra: Eat[Top] As Eat[Bottom] = As.contra(cAsA) | ||
val contra1_2: EatF[Top, Unit] As EatF[Bottom,Unit] = As.contra1_2(cAsA) | ||
val contra2_2: Eatꟻ[Unit, Top] As Eatꟻ[Unit,Bottom] = As.contra2_2(cAsA) | ||
val contra1_3: EatF13[Top, Unit,Unit] As EatF13[Bottom, Unit, Unit] = As.contra1_3(cAsA) | ||
val contra2_3: EatF23[Unit, Top, Unit] As EatF23[Unit, Bottom, Unit] = As.contra2_3(cAsA) | ||
val contra3_3: EatF33[Unit, Unit, Top] As EatF33[Unit, Unit, Bottom] = As.contra3_3(cAsA) | ||
} | ||
|
||
test("we can widen the output of a function1") { | ||
val f: Any => Bottom = _ => Bottom() | ||
val cAsA: Bottom As Top = implicitly | ||
val f2: Any => Top = As.onF(cAsA)(f) | ||
} | ||
|
||
test("we can narrow the input of a function1") { | ||
val f: Top => Any = (t: Top) => t | ||
val cAsA: Bottom As Top = implicitly | ||
val f2: Bottom => Any = As.conF(cAsA)(f) | ||
} | ||
|
||
test("we can simultaneously narrow the input and widen the ouptut of a Function1") { | ||
val f: Top => Bottom = _ => Bottom() | ||
val cAsA: Bottom As Top = implicitly | ||
val f2: Bottom => Top = As.invF(cAsA, cAsA)(f) | ||
} | ||
} |