trait
Leibniz[-L, +H >: L, A >: L <: H, B >: L <: H] extends AnyRef
Abstract Value Members
-
abstract
def
subst[F[_ >: L <: H]](p: F[A]): F[B]
Concrete 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
-
def
andThen[L2 <: L, H2 >: H, C >: L2 <: H2](that: Leibniz[L2, H2, B, C]): Leibniz[L2, H2, A, C]
-
final
def
asInstanceOf[T0]: T0
-
def
clone(): AnyRef
-
def
compose[L2 <: L, H2 >: H, C >: L2 <: H2](that: Leibniz[L2, H2, C, A]): Leibniz[L2, H2, C, B]
-
final
def
eq(arg0: AnyRef): Boolean
-
def
equals(arg0: Any): Boolean
-
def
finalize(): Unit
-
final
def
getClass(): Class[_]
-
def
hashCode(): Int
-
final
def
isInstanceOf[T0]: Boolean
-
final
def
ne(arg0: AnyRef): Boolean
-
final
def
notify(): Unit
-
final
def
notifyAll(): Unit
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
-
def
toString(): String
-
final
def
wait(): Unit
-
final
def
wait(arg0: Long, arg1: Int): Unit
-
final
def
wait(arg0: Long): Unit
Inherited from AnyRef
Inherited from Any
Leibnizian equality: a better
=:=This technique was first used in Typing Dynamic Typing (Baars and Swierstra, ICFP 2002).
It is generalized here to handle subtyping so that it can be used with constrained type constructors.
Leibniz[L,H,A,B]says thatA=B, and that both of its types are betweenLandH. Subtyping lets you loosen the bounds onLandH.If you just need a witness that
A=B, then you can useA===Bwhich is a supertype of anyLeibniz[L,H,A,B]The more refined types are useful if you need to be able to substitute into restricted contexts.