Profunctor optics + Yoneda encoding

ComputationalTrinitarianism.MD

@@ -15,7 +15,7 @@
 
 ## [Higher Category Theory](https://ncatlab.org/nlab/show/higher+category+theory)
 
-* 2-Dimensional Categories - Niles Johnson, Donald Yau [(arXiv:2002.06055)](https://arxiv.org/pdf/2002.06055.pdf)
+* 2-Dimensional Categories - Niles Johnson, Donald Yau [(arxiv:2002.06055)](https://arxiv.org/abs/2002.06055), [(pdf)](https://arxiv.org/pdf/2002.06055.pdf)
 * Introduction to higher category theory -  Tobias Dyckerhoff [(Lecture Notes, Problem Sets)](https://www.math.uni-hamburg.de/home/dyckerhoff/higher/index.html)
 * An Introduction to n-Categories - John C. Baez [(arXiv)](https://arxiv.org/abs/q-alg/9705009)
 * Basic Bicategories - Tom Leinster [(arXiv)](https://arxiv.org/abs/math/9810017)
@@ -145,6 +145,7 @@ This is very opinionated selection of authors that publish interesting papers ab
 * [Mauro Jaskelioff](https://dblp.uni-trier.de/pers/hd/j/Jaskelioff:Mauro)
 * [Johan Jeuring](https://dblp.uni-trier.de/pers/hd/j/Jeuring:Johan), [Utrecht University page](http://www.staff.science.uu.nl/~jeuri101/homepage/Publications/index.html)
 * [André Joyal](https://dblp.uni-trier.de/pers/hd/j/Joyal:Andr=eacute=), [arxiv](https://arxiv.org/search/math?query=Andr%C3%A9+Joyal&searchtype=author)
+* [Jacob Lurie](https://www.math.ias.edu/~lurie/)
 * [Jade Master](https://arxiv.org/search/math?searchtype=author&query=Master%2C+J)
 * [Lucius Gregory Meredith](https://dblp.org/pers/hd/m/Meredith:Lucius_Gregory)
 * [David Jaz Myers](http://davidjaz.com/), [arxiv](https://arxiv.org/search/math?searchtype=author&query=Myers%2C+D+J)
@@ -166,7 +167,7 @@ This is very opinionated selection of authors that publish interesting papers ab
 * [Wouter Swierstra](https://dblp.org/pers/hd/s/Swierstra:Wouter), [Utrecht University page](http://www.staff.science.uu.nl/~swier004/publications/)
 * [Tarmo Uustalu](http://cs.ioc.ee/~tarmo/papers/), [arXiv](https://arxiv.org/search/?query=Tarmo+Uustalu&searchtype=author&source=header)
 * [Christina Vasilakopoulou](https://thalis.math.upatras.gr/~cvasilak/), [arXiv](https://arxiv.org/search/math?searchtype=author&query=Vasilakopoulou%2C+C)
-* Philip Wadler [Monads, arrows, applicatives](http://homepages.inf.ed.ac.uk/wadler/topics/monads.html), [Parametricity](http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html)
+* [Philip Wadler](https://iohk.io/en/research/library/authors/philip-wadler/), [Monads, arrows, applicatives](http://homepages.inf.ed.ac.uk/wadler/topics/monads.html), [Parametricity](http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html)
 
 ## [Proof Theory](https://ncatlab.org/nlab/show/proof+theory)
 
@@ -270,12 +271,13 @@ SCALING DOT TO SCALA - SOUNDNESS - Martin Odersky [(blog post)](https://www.scal
 * Monoidal categories in Python [oxford-quantum-group/discopy](https://github.com/oxford-quantum-group/discopy), paper: DisCoPy: Monoidal Categories in Python Giovanni de Felice, Alexis Toumi, Bob Coecke [arxiv 2005.02975](https://arxiv.org/abs/2005.02975)
 * Evan Patterson: Realizing Applied Category Theory in Julia [(video)](https://www.youtube.com/watch?v=7dmrDYQh4rc)
 
-## Logic
+## (Constructive) Logic
 
 * Substructural Logics - Carnegie Mellon University - Frank Pfenning [(course notes)](http://www.cs.cmu.edu/~fp/courses/15816-f16/schedule.html) [(assignments)](http://www.cs.cmu.edu/~fp/courses/15816-f16/assignments.html)
 * Constructive Logic - Carnegie Mellon University - Frank Pfenning [(course notes)](http://www.cs.cmu.edu/~fp/courses/15317-f17/schedule.html) [(assignments)](http://www.cs.cmu.edu/~fp/courses/15317-f17/assignments.html)
 * Linear Logic - Carnegie Mellon University - Frank Pfenning [(course)](http://www.cs.cmu.edu/~fp/courses/linear/schedule.html)
 * [Logical_Graphs](https://oeis.org/wiki/Logical_Graphs#Peirce.27s_law)
+* [Applied Logic course - Erik Palmgren](http://www2.math.uu.se/~palmgren/tillog/) (contains nice lecture notes, exercises in Coq)
 
 ## Nominal Techniques
 

KanExtensions.MD

@@ -7,40 +7,72 @@ Construction that abstract over type constructor and allow to efficiently stack
 In Category Theory
 
 Yoneda Lemma states that:
-`[C,Set](C(a,-),F) ~ Fa`
-Set of natural transformations from `C` to `Set` of the Hom functor `C(a,-)` to Functor `F: C -> Set`
-is isomorphic to `Fa`
+`[C,Set](C(a,-),F) ~ F a`
+natural transformation between `Hom(a,-)` and functor `F: C -> Set` is isomorphic to value of Functor F on a `F a`.
 
-It is possible to formulate Yoneda Lemma in terms of Ends, and we get Ninja Yoneda Lemma:
-∫ `Set(C(a,x),F(x)) ~ Fa`
+In Haskell this can be expressed as
+```haskell
+f a  ~ forall x. (a -> x) -> f x
+````
 
-That corresponds to:
+In Scala we ca define:
 
-`def yoneda[R](cax: A => X, fx F[X]) ~ F[A]`
+```scala
+abstract class Yo[F[+_], A] {
+  def runYo(): Reader[A, *] ~> F[*]
+}
+
+type YonedaLemma[F[+_], A] = Yo[F, A] ~ F[A]
+def yonedaLemma[F[+_], A](implicit FF: Functor[F]): YonedaLemma[F, A] =
+  new YonedaLemma[F, A] {
+    def to: F[A] => Yo[F, A] = fa =>
+      new Yo[F, A] {
+        def runYo(): (A => *) ~> F =
+          λ[(A => *) ~> F](atox => FF.map(fa)(atox))
+      }
+
+    def from: Yo[F, A] => F[A] =
+      (fa: Yo[F, A]) => {
+        val raf: Reader[A, *] ~> F = fa.runYo()
+        raf.apply(identity[A])
+      }
+  }
+```
+
+where:
 
 ```scala
-trait Yoneda[F[_], A] {
-  def run[R](f: A => R): F[R]
+type Reader[-R, +A] = R => A
+
+trait ~[A, B] {
+  def to: B => A
+  def from: A => B
 }
 ```
 
-* we need Functor instance for F to create instance of Yoned for F
+In practice of FP following data structure is used:
+
+```scala
+trait Yoneda[F[_], A] {
+  def run[X](f: A => X): F[X]
+}
+```
+we need Functor instance for F to create instance of Yoneda for F
 ```scala
 def liftYoneda[F[_], A](fa: F[A])(implicit FunctorF: Functor[F]): Yoneda[F, A] =
   new Yoneda[F, A] {
-    def run[R2](f: A => R2): F[R2] = FunctorF.map(fa)(f)
+    def run[X2](f: A => X2): F[X2] = FunctorF.map(fa)(f)
   }
 ```
-
-* we don't need the fact that F is a Functor to go back to F
+yet we don't need the fact that F is a Functor to go back to F
 ```scala
 def lowerYoneda[F[_], A](y: Yoneda[F, A]): F[A] = y.run(identity[A])
 ```
 
-* we can define Functor instance, without any requirement on F:
+We can define Functor instance, without any requirement on F:
 ```scala
-def yonedaFunctor[F[_]]: Functor[Yoneda[F, ?]] =
-  new Functor[Yoneda[F, ?]] {
+def yonedaFunctor[F[_]]: Functor[Yoneda[F, *]] =
+  new Functor[Yoneda[F, *]] {
     def map[A, B](fa: Yoneda[F, A])(f: A => B): Yoneda[F, B] =
       new Yoneda[F, B] {
         def run[C](f2: B => C): F[C] = fa.run(f andThen f2)

Profunctors.MD

@@ -153,7 +153,7 @@ trait StrongProfunctor[P[_, _]] extends Profunctor[P] {
 }
 ```
 
-* Laws [Haskell](https://hackage.haskell.org/package/profunctors/docs/Data-Profunctor-Strong.html) [Cats](https://github.com/typelevel/cats/blob/master/laws/src/main/scala/cats/laws/StrongLaws.scala)
+* Laws [Haskell](https://hackage.haskell.org/package/profunctors/docs/Data-Profunctor-Strong.html) [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Strong.scala#L16-L90) [Cats](https://github.com/typelevel/cats/blob/master/laws/src/main/scala/cats/laws/StrongLaws.scala)
   1) `first == dimap(swap, swap) andThen second`
   2) `lmap(_.1) == rmap(_.1) andThen first`
   3) `lmap(second f) andThen first == rmap(second f) andThen first`

src/main/scala/educational/category_theory/Alternative.scala

@@ -0,0 +1,52 @@
+package educational.category_theory
+
+import cats.data.NonEmptyList
+
+trait MonoidK[F[_]] {
+  def empty[A]: F[A]
+  def combine[A](lhs: F[A], rhs: F[A]): F[A]
+}
+
+object MonoidK {
+  val listMonoidK: MonoidK[List] = new MonoidK[List] {
+    override def empty[A]: List[A] = Nil
+    override def combine[A](lhs: List[A], rhs: List[A]): List[A] = lhs ++ rhs
+  }
+
+  val vectorMonoidK: MonoidK[Vector] = new MonoidK[Vector] {
+    override def empty[A]: Vector[A] = Vector.empty
+    override def combine[A](lhs: Vector[A], rhs: Vector[A]): Vector[A] = lhs ++ rhs
+  }
+
+  val optionMonoidK: MonoidK[Option] = new MonoidK[Option] {
+    override def empty[A]: Option[A] = None
+
+    override def combine[A](lhs: Option[A], rhs: Option[A]): Option[A] = (lhs, rhs) match {
+      case (None, r) => r
+      case (l, _) => l
+    }
+  }
+}
+
+trait Alternative[F[_]] extends MonoidK[F] with Applicative[F] {
+  def some[A]: F[A] => F[NonEmptyList[A]] = v => map(v)(NonEmptyList.one)
+  def many[A]: F[A] => F[List[A]] = v => map(v)(List(_))
+}
+//
+//object Alternative {
+//  val vectorMonoidK: Alternative[Vector] = new Alternative[Vector] {
+//    override def empty[A]: Vector[A] = Vector.empty
+//    override def combine[A](lhs: Vector[A], rhs: Vector[A]): Vector[A] = lhs ++ rhs
+//    override def pure[A](a: A): Vector[A] = Vector(a)
+//    override def ap[A, B](ff: Vector[A => B])(fa: Vector[A]): Vector[B] = ???
+//  }
+//
+//  val optionMonoidK: Alternative[Option] = new Alternative[Option] {
+//    override def empty[A]: Option[A] = None
+//
+//    override def combine[A](lhs: Option[A], rhs: Option[A]): Option[A] = (lhs, rhs) match {
+//      case (None, r) => r
+//      case (l, _) => l
+//    }
+//  }
+//}

src/main/scala/educational/category_theory/Comonad.scala

@@ -42,3 +42,13 @@ extend(duplicate)   \        |
 
    */
 }
+
+object Comonad {
+  implicit def TupleComonad[T]: Comonad[(T,*)] = new Comonad[(T, *)] {
+    override def extract[A](wa: (T, A)): A = wa._2
+
+    override def duplicate[A](wa: (T, A)): (T, (T, A)) = (wa._1, wa)
+
+    override def map[A, B](wa: (T, A))(f: A => B): (T, B) = (wa._1, f(wa._2))
+  }
+}

src/main/scala/educational/category_theory/Invariant.scala

@@ -0,0 +1,5 @@
+package educational.category_theory
+
+trait Invariant[F[_]] {
+  def imap[A, B](fa: F[A])(f: A => B, g: B => A): F[B]
+}

src/main/scala/educational/category_theory/kan/DensitySimpleImpl.scala

@@ -44,7 +44,7 @@ object DensitySimpleImpl {
     def comonadInstance[K[_]]: Comonad[Density[K, *]] =
       new Comonad[Density[K, *]] {
         def extract[A](w: Density[K, A]): A = w.f(w.fb)
-        def duplicate[A](wa: Density[K, A]): Density[K, Density[K, A]] =
+        override def duplicate[A](wa: Density[K, A]): Density[K, Density[K, A]] =
           Density[K, Density[K, A], wa.Z](
             kx => Density[K, A, wa.Z](wa.f, kx),
             wa.fb

src/main/scala/educational/category_theory/two/profunctor/closed/Closed.scala

@@ -1,11 +1,9 @@
 package educational.category_theory.two.profunctor.closed
 
-import educational.category_theory.two.profunctor.Profunctor
-import educational.category_theory.two.profunctor.ProfunctorLaws
+import educational.category_theory.two.profunctor.{Profunctor, ProfunctorLaws}
 import educational.category_theory.two.profunctor.ProfunctorInstance.Function1Profunctor
-import Function.const
-import Function.uncurried
-import Function.untupled
+
+import scala.Function.{const, uncurried, untupled}
 
 /**
   * Closed Profunctor

src/main/scala/educational/collections/HeadNel.scala

@@ -23,7 +23,7 @@ case class Nel[+A](head: A, tail: Nel[A])
 object NelInstances {
   val nelComonad: Comonad[Nel] = new Comonad[Nel] {
     def extract[A](w: Nel[A]): A = ???
-    def duplicate[A](wa: Nel[A]): Nel[Nel[A]] = ???
+    override def duplicate[A](wa: Nel[A]): Nel[Nel[A]] = ???
     def map[A, B](fa: Nel[A])(f: A => B): Nel[B] = ???
   }
 }

src/main/scala/educational/collections/RoseTree.scala

@@ -8,7 +8,7 @@ object RoseTreeInstances {
 
   val roseTreeComonad: Comonad[RoseTree] = new Comonad[RoseTree] {
     def extract[A](na: RoseTree[A]): A = na.tip
-    def duplicate[A](na: RoseTree[A]): RoseTree[RoseTree[A]] =
+    override def duplicate[A](na: RoseTree[A]): RoseTree[RoseTree[A]] =
       RoseTree(na, na.subTrees.map(duplicate))
     def map[A, B](na: RoseTree[A])(f: A => B): RoseTree[B] =
       RoseTree(f(na.tip), na.subTrees.map(s => map(s)(f)))

src/main/scala/educational/data/CoReader.scala

@@ -13,7 +13,7 @@ object CoReaderInstances {
       def map[A, B](x: CoReader[R, A])(f: A => B): CoReader[R, B] =
         CoReader(f(x.extract), x.ask)
       def extract[A](w: CoReader[R, A]): A = w.extract
-      def duplicate[A](wa: CoReader[R, A]): CoReader[R, CoReader[R, A]] =
+      override def duplicate[A](wa: CoReader[R, A]): CoReader[R, CoReader[R, A]] =
         CoReader(wa, wa.ask)
     }
 }

src/main/scala/educational/data/Cofree.scala

@@ -13,6 +13,15 @@ case class Cofree[A, F[_]](extract: A, sub: F[Cofree[A, F]])(implicit
     duplicate.map(f) // coKleisi composition
 }
 
+object Cofree {
+
+  implicit def CofreeComonad[F[_]]: Comonad[Cofree[*, F]] = new Comonad[Cofree[*, F]] {
+    override def extract[A](w: Cofree[A, F]): A = w.extract
+    override def duplicate[A](wa: Cofree[A, F]): Cofree[Cofree[A, F], F] = wa.duplicate
+    override def map[A, B](fa: Cofree[A, F])(f: A => B): Cofree[B, F] = fa.map(f)
+  }
+}
+
 case class CofreeList[A](extract: A, sub: List[CofreeList[A]])
 
 object CofreeList {
@@ -22,7 +31,7 @@ object CofreeList {
       def map[A, B](ca: CofreeList[A])(f: A => B): CofreeList[B] =
         CofreeList(f(ca.extract), ca.sub.map(i => map(i)(f)))
       def extract[A](ca: CofreeList[A]): A = ca.extract
-      def duplicate[A](ca: CofreeList[A]): CofreeList[CofreeList[A]] =
+      override def duplicate[A](ca: CofreeList[A]): CofreeList[CofreeList[A]] =
         CofreeList(ca, ca.sub.map(duplicate))
     }
 }

src/main/scala/educational/data/Fix.scala

@@ -0,0 +1,7 @@
+package educational.data
+
+import educational.category_theory.Functor
+
+// Matryoshka: https://github.com/precog/matryoshka/blob/master/core/shared/src/main/scala/matryoshka/data/Fix.scala
+// Y combinator on type level
+case class Fix[F[_]](unFix: F[Fix[F]])

src/main/scala/educational/data/Id.scala

@@ -8,6 +8,6 @@ object IdInstances {
   val idComonad: Comonad[Id] = new Comonad[Id] {
     def map[A, B](x: Id[A])(f: A => B): Id[B] = Id(f(x.value))
     def extract[A](w: Id[A]): A = w.value
-    def duplicate[A](wa: Id[A]): Id[Id[A]] = Id(wa)
+    override def duplicate[A](wa: Id[A]): Id[Id[A]] = Id(wa)
   }
 }

src/main/scala/educational/data/Nu.scala

@@ -0,0 +1,7 @@
+package educational.data
+
+trait Nu[F[_]] {
+  type A
+  val a: A
+  val unNu: A => F[A]
+}

src/main/scala/educational/optics/Iso.scala

@@ -0,0 +1,21 @@
+package educational.optics
+
+trait ~[A,B] {
+  def to: B => A
+  def from: A => B
+}
+
+object Iso {
+  type Equivalence[A, B] = ~[A, B]
+  type Bijection[A, B] = ~[A, B]
+}
+
+case class Iso[S,A](from: S => A, to: A => S) { self => // Adapter
+  def modifyB(f: A => A): S => S =
+    (from andThen f) andThen to
+//  def andThen[B](other: Iso[A,B]): Iso[S,B] = Iso[S,B](
+//    self.from andThen other.from,
+//
+//  )
+}
+

src/main/scala/educational/optics/Lens.scala

@@ -0,0 +1,43 @@
+package educational.optics
+
+case class Lens[+A,-B,-S,+T](
+  view: S => A,
+  update: (B,S) => T
+)
+
+object LensExamples {
+
+  def tupleFoucsFirst[A,B,C]: Lens[A, B, (A,C), (B,C)] = {
+    def getFst: ((A,C)) => A = { case (a, _) => a }
+    def overrideFst: (B,(A,C)) => (B,C) = { case (b, (_,c)) => (b,c) }
+    Lens[A, B, (A,C), (B,C)](getFst, overrideFst)
+  }
+
+  def tupleFoucsSecond[A,B,C]: Lens[A, B, (A,C), (B,C)] = {
+    def getFst: ((A,C)) => A = { case (a, _) => a }
+    def overrideFst: (B, (A,C)) => (B,C) = { case (b, (_, c)) => (b, c) }
+    Lens[A, B, (A,C), (B,C)](getFst, overrideFst)
+  }
+
+  // monomorphic - types have to be the same for A,B and S,T
+  val signNonNegative: Lens[Boolean, Boolean, Int, Int] = {
+    def isNonNegative: Int => Boolean = _ >= 0
+    def asNonNegative: (Boolean,Int) => Int = { case(b,n) =>
+      if(b) Math.abs(n)
+      else -Math.abs(n)
+    }
+
+    Lens[Boolean, Boolean, Int, Int](isNonNegative, asNonNegative)
+  }
+
+  // Nat and isOdd would work
+  // Nat and isPrime would be tricky (enforcing property could be hard)
+
+  // compsing lens
+//  def tupleInnerFirst[A,B,C,D]: Lens[A, B, ((A,C),D), ((B,C),D)] = {
+//    def overrideFst: (B,(A,C)) => (B,C) = { case (b, (_,c)) => (b,c) }
+//    Lens[A, B, ((A,C),D), ((B,C),D)](tupleFoucsFirst.view andThen tupleFoucsFirst.view, overrideFst)
+//  }
+
+  // TODO finish + check if we use Option instead of Either if that helps?
+}