Skip to content
master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
src
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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.