Leibniz

Type Members

type ===[A, B] = Leibniz[⊥, ⊤, A, B]

(A === B) is a supertype of Leibniz[L,H,A,B]

Value Members

final def !=(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def !=(arg0: Any): Boolean

Definition Classes
Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def ==(arg0: Any): Boolean

Definition Classes
Any
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
def force[L, H >: L, A >: L <: H, B >: L <: H]: Leibniz[L, H, A, B]

Unsafe coercion between types.
Unsafe coercion between types. force abuses asInstanceOf to explicitly coerce types. It is unsafe, but needed where Leibnizian equality isn't sufficient

Definition Classes
LeibnizFunctions
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
def hashCode(): Int

Definition Classes
AnyRef → Any
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
implicit def leibniz: Category[===]

Definition Classes
LeibnizInstances
def lift[LA, LT, HA >: LA, HT >: LT, T[_ >: LA <: HA] >: LT <: HT, A >: LA <: HA, A2 >: LA <: HA](a: Leibniz[LA, HA, A, A2]): Leibniz[LT, HT, T[A], T[A2]]

We can lift equality into any type constructor
We can lift equality into any type constructor

Definition Classes
LeibnizFunctions
def lift2[LA, LB, LT, HA >: LA, HB >: LB, HT >: LT, T[_ >: LA <: HA, _ >: LB <: HB] >: LT <: HT, A >: LA <: HA, A2 >: LA <: HA, B >: LB <: HB, B2 >: LB <: HB](a: Leibniz[LA, HA, A, A2], b: Leibniz[LB, HB, B, B2]): Leibniz[LT, HT, T[A, B], T[A2, B2]]

We can lift equality into any type constructor
We can lift equality into any type constructor

Definition Classes
LeibnizFunctions
def lift3[LA, LB, LC, LT, HA >: LA, HB >: LB, HC >: LC, HT >: LT, T[_ >: LA <: HA, _ >: LB <: HB, _ >: LC <: HC] >: LT <: HT, A >: LA <: HA, A2 >: LA <: HA, B >: LB <: HB, B2 >: LB <: HB, C >: LC <: HC, C2 >: LC <: HC](a: Leibniz[LA, HA, A, A2], b: Leibniz[LB, HB, B, B2], c: Leibniz[LC, HC, C, C2]): Leibniz[LT, HT, T[A, B, C], T[A2, B2, C2]]

We can lift equality into any type constructor
We can lift equality into any type constructor

Definition Classes
LeibnizFunctions
def lower[LA, HA >: LA, T[_ >: LA <: HA], A >: LA <: HA, A2 >: LA <: HA](t: ===[T[A], T[A2]]): Leibniz[LA, HA, A, A2]

Emir Pasalic's PhD thesis mentions that it is unknown whether or not ((A,B) === (C,D)) => (A === C) is inhabited.
Emir Pasalic's PhD thesis mentions that it is unknown whether or not ((A,B) === (C,D)) => (A === C) is inhabited.
Haskell can work around this issue by abusing type families as noted in Leibniz equality can be injective (Oleg Kiselyov, Haskell Cafe Mailing List 2010) but we instead turn to force.

Definition Classes
LeibnizFunctions
def lower2[LA, HA >: LA, LB, HB >: LB, T[_ >: LA <: HA, _ >: LB <: HB], A >: LA <: HA, A2 >: LA <: HA, B >: LB <: HB, B2 >: LB <: HB](t: ===[T[A, B], T[A2, B2]]): (Leibniz[LA, HA, A, A2], Leibniz[LB, HB, B, B2])

Definition Classes
LeibnizFunctions
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
final def notifyAll(): Unit

Definition Classes
AnyRef
implicit def refl[A]: Leibniz[A, A, A, A]

Equality is reflexive -- we rely on subtyping to expand this type
Equality is reflexive -- we rely on subtyping to expand this type

Definition Classes
LeibnizFunctions
implicit def subst[A, B](a: A)(implicit f: ===[A, B]): B

Definition Classes
LeibnizFunctions
def symm[L, H >: L, A >: L <: H, B >: L <: H](f: Leibniz[L, H, A, B]): Leibniz[L, H, B, A]

Equality is symmetric
Equality is symmetric

Definition Classes
LeibnizFunctions
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def toString(): String

Definition Classes
AnyRef → Any
def trans[L, H >: L, A >: L <: H, B >: L <: H, C >: L <: H](f: Leibniz[L, H, B, C], g: Leibniz[L, H, A, B]): Leibniz[L, H, A, C]

Equality is transitive
Equality is transitive

Definition Classes
LeibnizFunctions
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
implicit def witness[A, B](f: ===[A, B]): (A) ⇒ B

We can witness equality by using it to convert between types We rely on subtyping to enable this to work for any Leibniz arrow
We can witness equality by using it to convert between types We rely on subtyping to enable this to work for any Leibniz arrow

Definition Classes
LeibnizFunctions

object Leibniz extends LeibnizInstances with LeibnizFunctions

Type Members

type ===[A, B] = Leibniz[⊥, ⊤, A, B]

Value Members

final def !=(arg0: AnyRef): Boolean

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: AnyRef): Boolean

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def finalize(): Unit

def force[L, H >: L, A >: L <: H, B >: L <: H]: Leibniz[L, H, A, B]

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

implicit def leibniz: Category[===]

def lift[LA, LT, HA >: LA, HT >: LT, T[_ >: LA <: HA] >: LT <: HT, A >: LA <: HA, A2 >: LA <: HA](a: Leibniz[LA, HA, A, A2]): Leibniz[LT, HT, T[A], T[A2]]

def lift2[LA, LB, LT, HA >: LA, HB >: LB, HT >: LT, T[_ >: LA <: HA, _ >: LB <: HB] >: LT <: HT, A >: LA <: HA, A2 >: LA <: HA, B >: LB <: HB, B2 >: LB <: HB](a: Leibniz[LA, HA, A, A2], b: Leibniz[LB, HB, B, B2]): Leibniz[LT, HT, T[A, B], T[A2, B2]]

def lower[LA, HA >: LA, T[_ >: LA <: HA], A >: LA <: HA, A2 >: LA <: HA](t: ===[T[A], T[A2]]): Leibniz[LA, HA, A, A2]

def lower2[LA, HA >: LA, LB, HB >: LB, T[_ >: LA <: HA, _ >: LB <: HB], A >: LA <: HA, A2 >: LA <: HA, B >: LB <: HB, B2 >: LB <: HB](t: ===[T[A, B], T[A2, B2]]): (Leibniz[LA, HA, A, A2], Leibniz[LB, HB, B, B2])

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

implicit def refl[A]: Leibniz[A, A, A, A]

implicit def subst[A, B](a: A)(implicit f: ===[A, B]): B

def symm[L, H >: L, A >: L <: H, B >: L <: H](f: Leibniz[L, H, A, B]): Leibniz[L, H, B, A]

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

def trans[L, H >: L, A >: L <: H, B >: L <: H, C >: L <: H](f: Leibniz[L, H, B, C], g: Leibniz[L, H, A, B]): Leibniz[L, H, A, C]

final def wait(): Unit

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

implicit def witness[A, B](f: ===[A, B]): (A) ⇒ B

Inherited from LeibnizFunctions

Inherited from LeibnizInstances

Inherited from AnyRef

Inherited from Any

Ungrouped