2

迄今为止的故事——

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 HMonadyoneda 和 coyoneda 有HFunctor实例,并且我想知道 aHKleisli会是什么样子。

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

4

1 回答 1

0

所以......还有测试要做,但与此同时,我赢了。注意与普通 kleisli 箭头绑定的相似之处。问题不是量化类型相等,但是问题更多在于嵌套,这个版本就像是浅了 2 层,并且与通过 join 竞标非常相似,有趣的是我直到后来才注意到。我会把这个问题留一会儿,以防有人绊倒并有比我更好的答案。就目前/@>而言,这只是·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
    }
   }
于 2014-10-09T06:33:22.047 回答