HOME | EDIT | RSS | INDEX | ABOUT | GITHUB

Scala 3 Kan Extensions


可以跑的源码在这里 👉 https://github.com/jcouyang/meow


什么是 看展Kan Extensions? 可以看下 ekmett 怎么解释

简单的说呢:

All concepts are Kan extensions. The notion of Kan extensions subsumes all the other fundamental concepts of category theory. – Categories for the Working Mathematician

所有的概念都是看展,这就厉害了。感觉会了这个就会了整个猫论。

但是我们关心的其实是 Scala 3,既然猫论可以由看展归纳出来,如果我们能用Scala 3实现看展,其它的是不就都唾手可得呢。

下面开始翻译 http://hackage.haskell.org/package/kan-extensions-5.2

左看

Haskell 的定义用了 GADT

data Lan g h a where
  Lan :: (g b -> a) -> h b -> Lan g h a

对阿,我们才学过 GADT, 用 enum 就好了:

enum Lan[G[?], H[?], A] {
 case LeftKan[G[?], H[?], A, B](f: (G[B] => A), v: H[B]) extends Lan[G, H, A]
}

看起来不是很复杂,重要的是 Lan 可以得到一个 免费函子Free Functor:

given [G[?],H[?]] as Functor[Lan[G, H, *]] {
  def [A, B](r: Lan[G, H, A]).map(f: A => B):Lan[G,H,B] = r match {
    case Lan.LeftKan(g, v) => Lan.LeftKan(f compose g, v)
  }
}

这怎么这么眼熟,难道这不就是用来实现 Free Monad 的 Coyoneda? 果然可以引出所有概念。

type CoYoneda[F[?], A] = Lan[Id, F, A]

而且注意到其中 Scala 3 的新写法:

右看

newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }

从 Haskell 翻译过来也容易,我们不是才学的 Rank N Types 么? forall b. (a -> gb) 很好表示:

case class Ran[G[?], H[?], A](run: [B] => (A => G[B]) => H[B])

这也有个 免费函子Free Functor:

given [G[?],H[?]] as Functor[Ran[G, H, *]] {
  def [A, B](r: Ran[G, H, A]).map(f: A => B):Ran[G,H,B] =
    Ran([C] => (k:B=>G[C]) => r.run(k.compose(f)))
}

不用想也知道那么这个应该可以推出 Yoneda 吧:

type Yoneda[F[?], A] = Ran[Id, F, A]

不仅有免费的函子,更有免费的单子,当 H 也是 G 的时候:

given [G[?]](using Functor[Ran[G, G, *]]) as Monad[Ran[G, G, *]] {
  def pure[A](a: A): Ran[G, G, A] = Ran([C]=>(k:A=>G[C]) => k(a))
  def [A, B](r: Ran[G, G, A]).map(f: A => B):Ran[G,G,B] = r.map(f)
  def [A, B](ran: Ran[G, G, A]) >>= (f: A => Ran[G,G,B]):Ran[G,G,B] =
    Ran([C] => (k: B => G[C]) => ran.run((a)=> f(a).run(k)))
}

其中:

当然看展不仅仅引出这么些概念,还可以推出 ConT, Limits, CoLimits… http://comonad.com/reader/2008/kan-extensions/ 更重要的是,实现它几乎把所有我们学过GADT,Rank-N Types, Phantom Types, Typeclasses(given, using) 这些 Scala 3 新特性都用了个遍,真是两仪生四象,四象生八卦,八卦生万物。

有兴趣的同学可以下源码看下测试,这看展的 property based testing 写得真是太费劲了。

Footnotes: