Scala 3 Kan Extensions
可以跑的源码在这里 👉 https://github.com/jcouyang/meow
什么是 看展? 可以看下 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 可以得到一个 免费函子:
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 的新写法:
*
是 kind projector 表示 kind, Scala 3 不再需要编译器插件,只需要打开toggle-Ykind-projector
即可。 https://dotty.epfl.ch/docs/reference/changed-features/wildcards.htmlgiven
是新的表示 typeclass instance 的 implicit。 https://dotty.epfl.ch/docs/reference/contextual/givens.html
右看
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])
这也有个 免费函子:
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)))
}
其中:
using
是新的 implicit 参数写法, 而且还可以匿名。 https://dotty.epfl.ch/docs/reference/contextual/using-clauses.html
当然看展不仅仅引出这么些概念,还可以推出 ConT, Limits, CoLimits… http://comonad.com/reader/2008/kan-extensions/ 更重要的是,实现它几乎把所有我们学过GADT,Rank-N Types, Phantom Types, Typeclasses(given, using) 这些 Scala 3 新特性都用了个遍,真是两仪生四象,四象生八卦,八卦生万物。
有兴趣的同学可以下源码看下测试,这看展的 property based testing 写得真是太费劲了。