LeibnizAndLiskov.scala

sealed abstract class Leibniz[-L, +H >: L, A >: L <: H, B >: L <: H] {
  def subst[F[_ >: L <: H]](fa: F[A]): F[B]
  
  def flip: Leibniz[L, H, B, A] = {
    type f[a >: L <: H] = Leibniz[L, H, a, A]
    subst[f](Leibniz.refl[A])
  }
}
object Leibniz {
  def refl[A]: Leibniz[A, A, A, A] = new Leibniz[A, A, A, A] {
    def subst[F[_ >: A <: A]](fa: F[A]): F[A] = fa
  }
  
  def assert[L, H >: L, A >: L <: H, B >: L <: H] = new Leibniz[L, H, A, B] {
    def subst[F[_ >: L <: H]](fa: F[A]): F[B] = fa.asInstanceOf[F[B]]
  }
}

sealed abstract class LiskovF[-L, +H >: L, A >: L <: H, B >: L <: H] {
  type Lower >: L <: (B with Upper)
  type Upper >: A <: H
  def lower: Leibniz[L, H, A, Lower]
  def upper: Leibniz[L, H, B, Upper]
  
  def loosen: Liskov[L, H, A, B] = {
    type f1[x >: L <: H] = Liskov[L, H, x, Upper]
    type f2[x >: L <: H] = Liskov[L, H, A, x]
    upper.flip.subst[f2](lower.flip.subst[f1](Liskov.refl[Lower] : Liskov[L, H, Lower, Upper]))
  }
  
  def substCt[F[-_ >: L <: H]](fb: F[B]): F[A] =
    lower.flip.subst[F](upper.subst[F](fb) : F[Lower])
  
  def substCo[F[+_ >: L <: H]](fa: F[A]): F[B] =
    upper.flip.subst[F](lower.subst[F](fa) : F[Upper])
}
object LiskovF {
  def refl[A]: LiskovF[A, A, A, A] = new LiskovF[A, A, A, A] {
    type Lower = A
    type Upper = A
    def lower = Leibniz.refl[A]
    def upper = Leibniz.refl[A]
  }
}

sealed abstract class Liskov[-L, +H >: L, -A >: L <: H, +B >: L <: H] {
  def fix[L1 <: L, H1 >: H, A1 >: L1 <: A, B1 >: B <: H1]: LiskovF[L1, H1, A1, B1]
  
  def substCt[F[-_ >: L <: H]](fb: F[B]): F[A] =
    fix[L, H, A, B].substCt[F](fb)
  
  def substCo[F[+_ >: L <: H]](fa: F[A]): F[B] =
    fix[L, H, A, B].substCo[F](fa)
}
object Liskov {
  def refl[A]: Liskov[A, A, A, A] = new Liskov[A, A, A, A] {
    def fix[L1 <: A, H1 >: A, A1 >: L1 <: A, B1 >: A <: H1]: LiskovF[L1, H1, A1, B1] = new LiskovF[L1, H1, A1, B1] {
      type Lower = A1
      type Upper = B1
      def lower = Leibniz.refl[Lower]
      def upper = Leibniz.refl[Upper]
    }
  }
}