高阶 kleisli (scala) 中的类型相等

Question

到目前为止的故事 -

type :**:[F[_], G[_]] = ({ type λ[α] = F[G[α]] })

trait HBind[M[_]] extends HFunctor[M] {
  def hbind[F[_], G[_]](f: F ~> (M :**: G)#λ)(implicit MG: Functor[(M :**: G)#λ], F: Functor[F], G: Functor[G]): (M :**: F)#λ ~> (M :**: G)#λ

  def hjoin[F[_]: Functor]: (M :**: (M :**: F)#λ)#λ ~> (M :**: F)#λ

  def hflatMap[F[_], G[_], A](fa: M[F[A]])(f: F ~> (M :**: G)#λ)(implicit MG: Functor[(M :**: G)#λ], F: Functor[F], G: Functor[G]): M[G[A]] = hbind(f)(MG, F, G)(fa)

  def hflatten[F[_]: Functor, A](m: M[M[F[A]]]): M[F[A]] = hjoin(implicitly[Functor[F]])(m)

}

...

trait HMonad[M[_]] extends HBind[M] with HPointed[M]


final class HKleisli[M[_], F[_], G[_]](val run: F ~> (M :**: G)#λ) extends AnyVal {
  import HKleisli.hkleisli
  def apply[A](x: F[A]): M[G[A]] = run(x)
  def hflatMap[K[_]](phi: G ~> ({ type λ[α] = F ~> (M :**: K)#λ })#λ)(implicit M: HMonad[M], H: Functor[(M :**: K)#λ], F: Functor[F], G: Functor[G], K: Functor[K]): HKleisli[M, F, K] =
  hkleisli({
    val psi: (F ~> (M :**: K)#λ) =
      new (F ~> (M :**: K)#λ) {
        def apply[A](fa: F[A]) =
          M.hflatMap(run(fa)) {
            //hole: G ~> [α]M[K[α]]
            val gmk: (G ~> (M :**: K)#λ) =
              new (G ~> (M :**: K)#λ) {
                def apply[A](ga: G[A]) = {
                  val fmk: F ~> (M :**: K)#λ = phi(ga)
                  hkleisli(fmk).run(fa)  // type mismatch; found : fa.type (with underlying type F[A]) required: F[A]
                }
              }
            gmk
          }
      }
    psi
  })

}

object HKleisli {
  def apply[M[_], F[_], G[_]](k: F ~> (M :**: G)#λ) = new HKleisli(k)
  def hkleisli[M[_], F[_], G[_]](k: F ~> (M :**: G)#λ) = apply(k)
}

问题，

现在就所有这一切而言，有两个目标，首先我有兴趣在 scala 中实现 2 类（到目前为止我已经非常成功{我认为程序可能通过在合适的类别中绘制和组合图表来设计 Scala 具有我观察到的 BiCCC 2-Category 结构（至少我很确定）}），第二个通用编程， Free Monad 是更高阶的 monad HMonad yoneda 和 coyoneda 有 HFunctor 实例，我想知道 HKleisli 会是什么样子。

现在我遇到了A 参数相互遮蔽并创建 F[A]-not-F[A] 问题的问题。现在我的第一个想法是添加一个隐含的Leibniz[F[A], F[A']]（A' 是伪代码）并希望我可以用它来见证 [A]F[A] [A']F[A'] 的相等性，但我还没有弄清楚它是如何工作的，或者它是否足够，而且我也想知道我是否只是在这方面钻了太久，并且错过了一些明显的重写，让我到达了我正在尝试的地方去，所以我向这里的好人开放。我希望能提供任何帮助，并尽可能详细地说明如何实现这一点，我希望能分享关于高阶分类抽象的任何想法。

Answer 1

所以...还有测试要做，但与此同时，我赢了。请注意与普通 kleisli 箭头绑定的相似之处。问题不是量化类型相等，是的，但问题更多在于嵌套，这个版本就像两层更浅，并且与通过连接竞价非常相似，有趣的是我直到后来才注意到。我会把这个问题留一会儿，以防有人绊倒并有比我更好的答案。 就/@> 而言，这只是一个小小的组成· 代表scala。我直接在~>上定义了，并为函数写了一个隐式转换。

    final class HKleisli[M[_], F[_], G[_]](val run: F ~> (M :**: G)#λ) extends AnyVal {
      import HKleisli.hkleisli
      def apply[A](x: F[A]): M[G[A]] = run(x)

      final def >=>[K[_]](that: HKleisli[M, G, K])(implicit M: HMonad[M], G: Functor[G], K: Functor[K]): HKleisli[M, F, K] = {
        hkleisli({
          val phi =
            new (F ~> (M :**: K)#λ) {
             def apply[A](fa: F[A]) = {
               M.hbind(that.run)(G, K)(run(fa))
           }
        }
      phi
     })
   }

   final def hbind[K[_]](phi: G ~> ({ type λ[α] = F ~> (M :**: K)#λ })#λ)(implicit M: HMonad[M], K: Functor[K]): HKleisli[M, F, K] = {
   hkleisli({
     val psi =
      new (F ~> (M :**: K)#λ) {
      def apply[A](fa: F[A]) =
        M.hjoin(K)(M.map(M.transmap[G, ({ type λ[α] = F ~> (M :**: K)#λ })#λ](phi)(run(fa))) { (nt: F ~> (M :**: K)#λ) => nt(fa) })
     }
     psi
   })
  }

  final def local[X[_]](f: X ~> F) = hkleisli { 
    val phi = 
      new (X ~> (M:**:G)#λ) {
       def apply[A](x: X[A]) =
        (f /@>[(M:**:G)#λ] run)(x)
    }
    phi
  }
}

object HKleisli {
  def apply[M[_], F[_], G[_]](k: F ~> (M :**: G)#λ) = new HKleisli(k)

  def hkleisli[M[_], F[_], G[_]](k: F ~> (M :**: G)#λ) = apply(k)

  type HKleisliAr[M[_]] = ({ type λ[φ[_], ψ[_]] = HKleisli[M, φ, ψ] })

  def hkIdentity[M[_], F[_]](implicit M: HMonad[M], F: Functor[F]): HKleisli[M, F, F] =
    hkleisli(M.hpoint(F))

  implicit def category[M[_]: HMonad]: HCategory[HKleisliAr[M]#λ] =
    new HCategory[HKleisliAr[M]#λ] {
      def identity[F[_]: Functor] = hkIdentity[M, F]
      def composition[A[_]: Functor, B[_]: Functor, C[_]: Functor](g: HKleisli[M, B, C])(f: HKleisli[M, A, B]) =
        f >=> g
    }
   }