Skip to content

Latest commit

 

History

History
43 lines (38 loc) · 1.93 KB

README.md

File metadata and controls

43 lines (38 loc) · 1.93 KB
Raw

Leibniz Scala Library

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.

Witnesses

  • Is[A, B] (with a type alias to A === B) witnesses that types A and B are exactly the same.
  • Similarly, 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 😃).
  • Covariant[F] witnesses that HKT F is covariant (constant or strictly covariant).
  • Ditto other typeclasses / propositional types in variance package.
  • See my impromptu LC 2018 presentation for an overview.

Quick Start

resolvers += Resolver.bintrayRepo("alexknvl", "maven")
libraryDependencies += "com.alexknvl"  %%  "leibniz" % "0.10.0"

License

Code is provided under the MIT license available at https://opensource.org/licenses/MIT, as well as in the LICENSE file.