HListを使った「しりとりの圏」とLemmaパターン #Scala

初めて圏論をググったとき「しりとりの圏」というのがヒットして、これが直感的に理解できてとても分かりやすかった。この記事では、しりとりの圏を Shapeless のHList を使って書いてみる。

お題

オリジナルとの対応は以下の通り

圏論	元記事	この記事の実装
圏	しりとりの圏	HListしりとりの圏
対象	ひらがな文字	Scala の型
射	ひらがな文字列	HListで表現された heterogeneous lists 型
恒等射	一文字のひらがな文字列	要素一個のHList型
合成	しりとり結合	HList型のしりとり結合

※ 文字列やHListが「射」というのは語感的に初めはわかりにくいが、「ただ一つの対象をもつ圏」として見た場合のモノイドもそうだったりして圏論的には普通らしい。

実装方針

"Type Astronaut's Guide To Shapeless"に載っている、Lemma パターンを使って、恒等射、射の合成、結合法則、単位法則を書いてみる。

Lemma パターンとは、Auxなどでつなげたimplicitな型クラスの連鎖をさらに別の型クラスとしてまとめたもの。これの Lemma を、文字通り「補題」「補助定理」として型の制約を構成して、その正しさをコンパイラに検証させるというもの。

Gistはこちら: HList type chain

依存等

scalaVersion := "2.12.4"

"com.chuusai" %% "shapeless" % "2.3.2",
"org.typelevel" % "cats-core_2.12" % "1.0.1",
"org.typelevel" % "cats-free_2.12" % "1.0.1",
"org.typelevel" % "cats-laws_2.12" % "1.0.1",
"org.scalacheck" %% "scalacheck" % "1.13.5" % "test",
"org.scalatest" %% "scalatest" % "3.0.4" % "test"

HListしりとりの圏

オブジェクトtypeChainCatの中に各 Lemma を書いていく。

object typeChainCat {
  //...
}

恒等射： Id

オリジナルではunit: H -> HStr（H:ひらがな文字の集合、HStr: ひらがな文字列の集合）となっている恒等射を、ここではId[A]型として表現した。AuxのOutとして、要素型を一つだけもつHList,A :: HNilを出力している。

trait Id[A] {
  type Out
  def apply(l: A): Out
}
object Id {
  type Aux[L, O] = Id[L] { type Out = O }
  def apply[L](implicit s: Id[L]): Aux[L, s.Out] = s

  implicit def typeChainId[A]: Id.Aux[A, A :: HNil] = new Id[A] {
    type Out = A :: HNil
    def apply(a: A): Out = a :: HNil
  }
}

射の合成：Compose

ひらがなのしりとりと同じように末尾の型と先頭の型が同じHListを接続する。つまりA :: 〜 :: B :: HNilとB :: 〜 :: C :: HNilをつなげて、A :: 〜 :: B :: 〜 :: C :: HNilとする。

trait Compose[L, R] {
  type Out
  def apply(l: L, r: R): Out
}
object Compose {
  type Aux[L, R, O] = Compose[L, R] { type Out = O }
  def apply[L, R](implicit s: Compose[L, R]): Aux[L, R, s.Out] = s

  implicit def typeChainCompose[
    L <: HList,
    LL,
    R <: HList,
    TR <: HList,
    O <: HList](
  implicit
    last:    Last.Aux[L, LL],
    isHCons: IsHCons.Aux[R, LL, TR],
    prepend: Prepend.Aux[L, TR, O]
  ): Compose.Aux[L, R, prepend.Out] = new Compose[L, R] {
    type Out = prepend.Out
    def apply(l: L, r: R): Out = prepend.apply(l, isHCons.tail(r))
  }
}

結合法則

上で定義したIdとComposeを使って、圏の法則も Lemma として表現する。結合法則は以下のようになる。

trait Assoc[A, B, C] {
  type Out
  def apply(a: A, b: B, c: C): Out
}
object Assoc {
  type Aux[A, B, C, O] = Assoc[A, B, C] { type Out = O }
  def apply[A, B, C](implicit s: Assoc[A, B, C]): Aux[A, B, C, s.Out] = s

  implicit def typeChainAssociativity[
      A <: HList, B <: HList, C <: HList, AB <: HList, BC <: HList, O <: HList
    ]( implicit
      ab: typeChainCat.Compose.Aux[A,  B,  AB],
      o1: typeChainCat.Compose.Aux[AB, C,  O],  // (AB)C = O
      bc: typeChainCat.Compose.Aux[B,  C,  BC],
      o2: typeChainCat.Compose.Aux[A,  BC, O]   // A(BC) = O = (AB)C
  ): Assoc.Aux[A, B, C, O] = new Assoc[A, B, C] {
    type Out = O
    def apply(a: A, b: B, c: C): Out = o1.apply(ab.apply(a, b), c)
  }
}

以下のように具体的な型を与えて確認できる。

def testAssoc[
    A <: HList, B <: HList, C <: HList, O <: HList
  ](implicit ab: typeChainCat.Assoc.Aux[A, B, C, O]): Unit = ()//何もしない

testAssoc[
  Int    :: String  :: HNil, // A
  String :: Double  :: HNil, // B
  Double :: Boolean :: HNil, // C
  Int    :: String  :: Double  :: Boolean :: HNil // A・B・C
]

型が違っていると、実行時ではなくコンパイル時にエラーとなる

単位法則

恒等射を左から合成しても変わらないという法則。これも Lemma として定義する。

trait LeftIdentity[A, B] {
  def apply(a: A, b: B): B
}
object LeftIdentity {
  def apply[A, B](implicit s: LeftIdentity[A, B]): LeftIdentity[A, B] = s
  implicit def typeChainLeftIdentity[A, IDA <: HList, B <: HList](
    implicit
      id: typeChainCat.Id.Aux[A, IDA],
      ab: typeChainCat.Compose.Aux[IDA, B, B] // IDa・B = B
    ): LeftIdentity[A, B] = (_, b) => b
}

右も同様。

trait RightIdentity[A, B] {
  def apply(a: A, b: B): A
}
object RightIdentity {
  def apply[A, B](implicit s: RightIdentity[A, B]): RightIdentity[A, B] = s
  implicit def typeChainRightIdentity[A <: HList, B, IDB <: HList](
    implicit
      id: typeChainCat.Id.Aux[B, IDB],
      ab: typeChainCat.Compose.Aux[A, IDB, A] // A・IDb = A
    ): RightIdentity[A, B] = (a, _) => a
}

これも具体的な型で確認できる。

def testLeftIdentity[A, B <: HList](
  implicit id: typeChainCat.LeftIdentity[A, B]): Unit = ()

testLeftIdentity[Int, Int :: String :: HNil]

def testRightIdentity[A <: HList, B](
  implicit ab: typeChainCat.RightIdentity[A, B]): Unit = ()

testRightIdentity[Double :: String :: HNil, String]

これも誤りがあれば実行時ではなくコンパイル時にエラーとなる。

ちなみに testAssociativity だけを使って書くこともできる。

testAssoc[
  Int     :: HNil,            // IDa
  Int     :: Boolean :: HNil, // B
  Boolean :: HNil,            // IDc
  Int     :: Boolean :: HNil  // IDa・B = B・IDc = B
]

HListを使った「しりとりの圏」とLemmaパターン

お題