Leibniz equivalence and Liskov substitutability library for Scala.
The Leibniz’ equality law states that if a
and b
are identical then they
must have identical properties. Leibniz’ original definition reads as follows:
a ≡ b = ∀ f .f a ⇔ f b
and can be proven to be equivalent to:
a ≡ b = ∀ f .f a → f b
This library provides an encoding of Leibniz' equality and other related concepts in Scala. See my impromptu LC 2018 presentation for an overview.
Is[A, B]
(with a type alias to A === B
) witnesses that types
A
and B
are exactly the same.IsK[A, B]
(with a type alias to A =~= B
) witnesses
that types A[_]
and B[_]
are exactly the same. Combinators exist that
allow you to prove that F[A] === F[B]
for any F[_[_]]
or that
A[X] === B[X]
for any X
.Leibniz[L, H, A, B]
witnesses that types A
and B
are the same
and that they both are in between types L
and H
.Is[F, A, B]
witnesses type-equality for F-Bounded types.As[A, B]
witnesses that A
is a subtype of B
.As1[A, B]
witnesses that A
is a subtype of B
using existential types.Liskov[L, H, A, B]
is a bounded counterpart to As[A, B]
.Constant[F]
witnesses that HKT F
is a constant type lambda.Injective[F]
witnesses that HKT F
is injective (not a constant type lambda :smiley:).Covariant[F]
witnesses that HKT F
is covariant (constant or strictly covariant).variance
package.resolvers += Resolver.bintrayRepo("alexknvl", "maven")
libraryDependencies += "com.alexknvl" %% "leibniz" % "0.10.0"
Code is provided under the MIT license available at https://opensource.org/licenses/MIT, as well as in the LICENSE file.