Skip to content

Latest commit

 

History

History
300 lines (228 loc) · 13.7 KB

Contravariant.MD

File metadata and controls

300 lines (228 loc) · 13.7 KB
Raw
classDiagram
   Contravariant~F[-_]~ <|-- Divide~F[-_]~
   Divide <|-- Divisible~F[-_]~
   Divide <|-- Decide~F[-_]~
   Decide <|-- Decidable~F[-_]~
   Divisible <|-- Decidable

   class Contravariant {
     // contravariant Functor
     )  contramap(F[A], B => A): F[B]
   }
   class Divide {
     // contravariant Apply
     )  divide(A => (B,C), F[B], F[C]): F[A]
   }
   class Decide {
     // contravariant Alt  
     )  choose[A,B,C](A => Either[B, C], F[B], F[C]): F[A]
   }
   class Divisible {
     // contravariant Applicative
     )  conquer[A]: F[A]
   }
   class Decidable {
     // contravariant Alternative  
     )  loose[A](A => Void): F[A]
   }
Loading

Opposite category

Opposite category (nLab) is a category where all arrows are reversed.

case class Op[K[_,_],A,B](unOp: K[B,A])

or using type alias and specializing to category of Scala types and pure functions:

object Op {
  type Op[A,B] = B => A
}

Constructions in category C have dual constructions in category Op. Properties in given category holds also for dual construction in opposite category.

Examples of duality nLab

definition dual (opposite) definition
initial object terminal object
product coproduct
limits colimits
monads comonads
flatmap coflatmap
functor functor
free cofree
monoid comonoid
end coend
initial F-algebra terminal co-algebra

Contravariance is different concept than duality.

Contravariant (Contravariant Functor)

Type constructor that can be contramap, so map in opposite direction.

If we imagine Functor, as abstracting over some output, then Contravariant abstract over input.

In Category Theory Contravariant Functor is a Functor from opposite category (opposite category formalization in CubicalTT).

trait Contravariant[F[_]] {
  def contramap[A, B](f: B => A): F[A] => F[B]
}
flowchart RL
  FA1(("F[A]")) --"contramap(id)"--> FA2(("F[A]"))
  FA(("F[A]")) --"contramap(f andThen g)"--> FC(("F[C]"))
  FA(("F[A]")) --"contramap(f)"--> FB(("F[B]"))--"contramap(g)"--> FC(("F[C]"))
Loading

1 contramap identity

//         contramap(id)
// F[A]  ================> F[A]
contramap(fa)(identity[A]) == fa

2 contravariant composition

//        contramap f
// F[A] ==============> F[B]
val fb: F[B] = contramap(fa)(f)

//        contramap g
// F[B] ===============> F[C]
val l: F[C] = contramap(fb)(g)

//        contramap (g . f)
// F[A] =====================> F[B]
val r: F[C] = contramap(fa)(f compose g)

l == r

Divide (Contravariant Apply)

trait Divide[F[_]] extends Contravariant[F] {
  def divide[A,B,C](f: A => (B,C), fb: F[B], fc: F[C]): F[A]
}
def divideComposition[A](fa1: F[A], fa2: F[A], fa3: F[A]): Boolean = {
  //                divide(delta)
  //  F[A1], F[A2] ===============> F[A12]
  val fa12: F[A] = divide(delta[A], fa1, fa2)

  //                 divide(delta)
  // F[A12], F[A3] =================> F[A123]
  val l: F[A] = divide( delta[A], fa12, fa3)


  //                divide(delta)
  //  F[A2], F[A3] ===============> F[A23]
  val fa23: F[A] = divide(delta[A], fa2, fa3)

  //                  divide(delta)
  //  F[A1], F[A23] ===============> F[A123]
  val r: F[A] = divide( delta[A], fa1, fa23 )
  
  l == r
}

This is simplified version. Proper version is shown in Haskell.

  • Derived methods:
def divide1[A1, Z]    (a1: F[A1])           (f: Z => A1): F[Z] // contramap
def divide2[A1, A2, Z](a1: F[A1], a2: F[A2])(f: Z => (A1, A2)): F[Z]
// ...
def tuple2[A1, A2]    (a1: F[A1], a2: F[A2]):            F[(A1, A2)]
def tuple3[A1, A2, A3](a1: F[A1], a2: F[A2], a3: F[A3]): F[(A1, A2, A3)]
// ...
def deriving2[A1, A2, Z](f: Z => (A1, A2))(implicit a1: F[A1], a2: F[A2]): F[Z]
def deriving3[A1, A2, A3, Z](f: Z => (A1, A2, A3))(implicit a1: F[A1], a2: F[A2], a3: F[A3]): F[Z]
// ...
  • Resources
    • (Haskell) Contravariant Functors: The Other Side of the Coin - George Wilson (video)
    • (Haskell, Category Theory) Discrimination is Wrong: Improving Productivity - Edward Kmett (video) slides pdf

Divisible (Contravariant Applicative)

trait Divisible[F[_]] extends Divide[F] {
  def conquer[A]: F[A]
}

  1. all Contravariant and Divide laws including composition divide(divide(a1, a2)(delta), a3)(delta) == divide(a1, divide(a2, a3),(delta))(delta) (see Divide law)

  2. right identity: divide(fa, conquer)(delta) == fa

def rightIdentity[A](fa: F[A]): Boolean = {
  //                 divide(delta)    
  // F[A], conquer ===============> F[A]
  val l: F[A] = divide(delta, fa, conquer[A])
  
  l == fa
}
  1. left identity: divide(conquer, fa)(delta) == fa
def leftIdentity[A](fa: F[A]): Boolean = {
  //                 divide(delta)    
  // conquer, F[A] ===============> F[A]
  val l: F[A] = divide(delta, conquer[A], fa)
  
  l == fa
}

  • Instances: Predicate, Sorting, Serializable, Pritty Printing

  • Resources

    • Cats PR #2034 explaining design choices different that in Haskell, Scalaz
    • (Haskell) Contravariant Functors: The Other Side of the Coin - George Wilson (video)
    • (Haskell, Category Theory) Discrimination is Wrong: Improving Productivity - Edward Kmett (video) slides pdf

Contravariant Adjuctions & Representable

Contravariant Adjunction

Contravariant Rep

Contravariant Kan Extensions

Contravariant Yoneda

Contravariant Coyoneda

Similar a Coyoneda yet, with existenctial function running in opposite direction.

trait ContravariantCoyoneda[F[_], A] {
  type B
  val fb: F[B]
  val m: A => B


  def lowerCoyoneda(implicit CF: Contravariant[F]): F[A] = CF.contramap(fb)(m) // run
}

def liftCoyoneda[F[_], AA](fa: F[AA]): ContravariantCoyoneda[F, AA] = new ContravariantCoyoneda[F, AA] {
  type B = AA
  val fb: F[B] = fa
  val m: AA => B = identity[AA]
}

We can define Contravariant instance for Contravariant Coyoneda:

def cotraContraCoyo[F[_]] = new Contravariant[ContravariantCoyoneda[F, ?]] {
  def contramap[AA, BB](fa: ContravariantCoyoneda[F, AA])(f: BB => AA): ContravariantCoyoneda[F, BB] = new ContravariantCoyoneda[F, BB] {
    type B = fa.B
    val fb: F[B] = fa.fb
    val m: BB => B = fa.m compose f
  }
}

Contravariant Day