trait
Leibniz
[-L, +H >: L, A >: L <: H, B >: L <: H]
extends AnyRef
Abstract Value Members
-
def
subst
[F[_ >: L <: H]]
(p: F[A]): F[B]
Concrete Value Members
-
def
!=
(arg0: AnyRef): Boolean
-
def
!=
(arg0: Any): Boolean
-
def
##
(): Int
-
def
==
(arg0: AnyRef): Boolean
-
def
==
(arg0: Any): Boolean
-
def
andThen
[L2 <: L, H2 >: H, C >: L2 <: H2]
(that: Leibniz[L2, H2, B, C]): Leibniz[L2, H2, A, C]
-
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]
-
def
eq
(arg0: AnyRef): Boolean
-
def
equals
(arg0: Any): Boolean
-
def
finalize
(): Unit
-
def
getClass
(): java.lang.Class[_]
-
def
hashCode
(): Int
-
def
isInstanceOf
[T0]
: Boolean
-
def
ne
(arg0: AnyRef): Boolean
-
def
notify
(): Unit
-
def
notifyAll
(): Unit
-
def
synchronized
[T0]
(arg0: ⇒ T0): T0
-
def
toString
(): String
-
def
wait
(): Unit
-
def
wait
(arg0: Long, arg1: Int): Unit
-
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 that A = B, and that both of its types are between L and H. Subtyping lets you loosen the bounds on L and H.
If you just need a witness that A = B, then you can use A===B which is a supertype of any Leibniz[L,H,A,B]
The more refined types are useful if you need to be able to substitute into restricted contexts.