Scala
圏論
関数型プログラミング
shapeless

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

初めて圏論をググったときに直感的に理解できて分かりやすかった「しりとりの圏」を、Shapeless のHListのしりとりの圏として書いてみた。

お題

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

  • 圏: しりとりの圏 → HListしりとりの圏
  • 対象: ひらがな文字 → Scala の型
  • 射: ひらがな文字列 → HListで表現された'heterogeneous lists'型
  • 恒等射: 一文字のひらがな文字列 → 要素一個のHList型
  • 合成: しりとり結合 → HList型のしりとり結合

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

実装方針

"Type Astronaut's Guide To Shapeless"に載っている、"Lemma"パターンを使って、恒等射、射の合成、結合法則、単位法則を書いてみる。"Lemma"パターンとは、Auxなどでつなげたimplicitな型クラスの連鎖をさらに別の型クラスとしてまとめたもの。

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]型として表現した。AuxOutとして、要素型を一つだけもつ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 :: HNilB :: 〜 :: 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))
  }
}

結合法則

上で定義したIdComposeを使って、圏の法則も"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 // ABC
]

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

単位法則

恒等射を左から合成しても変わらないという法則。これも"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  // IDaB = BIDc = B
]

リンク