scalaとか・・・

HaskellのGADTsすごいなーと思ったのと、それをscalaz.Leibniz使って頑張る話

haskell, scala, scalaz | 11:10 |

まず、下記の10行程度のScalaコードをご覧ください

sealed abstract class Foo[A, B]
final case class X[A]() extends Foo[A, A]
final case class Y[A, B](a: A, b: B) extends Foo[A, B]

object Main {
  def hoge[F[_, _], A, B, C](foo: Foo[A, B], bar: F[A, C]): F[B, C] =
    foo match {
      case X() => bar
      case Y(a, b) => ??? // Yの場合のコードはどうでもいいので
    }
}

これは、コンパイルエラーになります(Scala2.11.1)。しかし、HaskellでGADTs使って同様のコード書くと、コンパイル通るらしいです。これの話をします。

Scalaのversionによって基本的に差異はないと思いますが、これ書いている時点の最新安定版のScala 2.11.1ということで話を進めます。

さて、上記のコードは、どういうコンパイルエラーになるかわかりますか？正解はこちら

Main.scala:8: error: type mismatch;
 found   : bar.type (with underlying type F[A,C])
 required: F[B,C]
      case X() => bar
                  ^
one error found

Scalaコンパイラは

「F[B, C] を要求しているのに、見つかったのは F[A, C] で、型が合わない」

と言っています。たしかにそうですね。では、なぜHaskellで同様のコードを書くとコンパイル通るのでしょうか？ポイントは

final case class X[A]() extends Foo[A, A]

となっていて、 foo: Foo[A, B] を X() でパターンマッチしたあと、というところです。

最初、*1これの意味がわかるのに何時間もかかってしまいました。が、わかってしまえば単純といえば単純かもしれません(?)

そして「Haskellこんなことできるのか、すごい！」となりました。*2

さて、解説に入っていきます。FooはXかYのどちらかになる、代数的データ型です。また、型パラメータを2つとります。ここで

「FooがXの場合に、Fooの型パラメータは、2つとも同じものが当てはめられている」

というのがポイントです。*3つまり

「Foo[A, B] 型の変数 foo が、もし(Yではなく) X だとしたら、その時点で A と B の型は同じだということが判明する。そして、その "A と B の型が同じ" という情報は、Haskell の場合には、fooがXにmatchした以後の文脈で、自動で利用できる」

ということらしいです。なので "A と Bが同じ" ということは "F[B, C]" と "F[A, C]" も同じ型、とHaskellは勝手に空気読んで判断してくれます。Haskellすごい・・・。そしてScalaだと通常それは不可能なはずです。*4 うっ、Scalaつらい・・・。

Scalaにおいては、実質単にキャストしてしまえば解決する問題です。しかし、キャストは安全ではないので使いたくないですね？この場合、Scalaが貧弱なだけで、本当は安全にキャストというか

「AとBが同じ型」という情報をもとに「"F[B, C]" と "F[A, C]" も同じ型」という情報を導く

ということをしたいのです。

そして考えた結果、scalaz.Leibnizを使えば、一応できる気がしたのでそのやり方を紹介します。他にもっと簡単な方法があったら誰か教えて下さい。

https://github.com/scalaz/scalaz/blob/v7.1.0-RC1/core/src/main/scala/scalaz/Leibniz.scala

さて、Leibnizという聞きなれない単語ですが、自分もこの言葉の由来とかしりません。*5 ScalazのLeibnizのscaladocに論文のリンクあるので、興味のある人はそれ読んでください。

Leibnizがなんなのか？を一言でいうと

「Scala標準ライブラリのPredefにある =:= と同じだが、合成可能で優れてるもの」

でしょうか。ちょうどそのあたり、最近typelevel.orgにblog記事上がってるので読みましょう

*6

http://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html

また、そもそも「Predefにある =:= 」を知らない人は、yuroyoroさんのこれ

Scalaで <:< とか =:= を使ったgeneralized type constraintsがスゴすぎて感動した話

などを読みましょう。また、これもScalazのversionによって変わらないとは思いますが、一応これ書いている時点の最新であるScalaz 7.1.0-RC1としておきます。

「合成可能」がどういうことか？というと、つまりは例えばさきほどのように

「AとBが同じ型」なら「"F[B, C]" と "F[A, C]" も同じ型」

という判断が可能になる、ということです。もう少し言い換えると

「A === B」が存在すれば、そこから「F[B, C] === F[A, C]」を生成可能

です。ここでいきなり === という記号が出てきましたが、

• type ===[A,B] = Leibniz[⊥, ⊤, A, B] と定義されてる*7
• 型パラメータ2つ持つものは中置記法で記述できる

というだけです。

では実際に、最初のコード例をscalaz.Leibniz使って書いていくとどうなるか？の詳細な説明です。

まず、パターンマッチはやめて、Fooにcatamorphismのためのメソッドを定義します。*8

sealed abstract class Foo[A, B] {
  def cata[Z](x: => Z, y: (A, B) => Z): Z = this match {
    case X() => x
    case Y(a, b) => y(a, b)
  }
}

しかし、このように普通に定義しただけでは、なんの解決にもなりません。ここで以下のように少し工夫します。

def cata[Z](x: (A === B) => Z, y: (A, B) => Z): Z = this match {
  case X() => x(Leibniz.force[Nothing, Any, A, B])
  case Y(a, b) => y(a, b)
}

とても残念*9ですが、Xだった場合は「AとBが同じ型だという情報」つまりは「A === B」を手動で生成して渡してあげるようにします。Leibniz.forceを使ってる時点で安全でない(実質キャストすることになる)のですが、安全でない操作をする箇所をできるだけ少なくするために、このようにする以外思いつきませんでした。

さて、すると、このcataを使う側では以下のように書くことができます

def hoge[F[_, _], A, B, C](foo: Foo[A, B], bar: F[A, C]): F[B, C] =
  foo.cata(
    _.subst[({type λ[a >: Nothing <: Any] = F[A, C] === F[a, C]})#λ](refl).apply(bar),
    (a, b) => ???
  )

やった、これでコンパイル通りましたね！

substというメソッドを使うことにより、「A === B」から「F[B, C] === F[A, C]」を生成しています。「A === B」から「F[B, C] === F[A, C]」の生成、は安全な操作です。また、Scala標準ライブラリの =:= には、このような機能がありません。これが、先ほどいった「Leibnizが合成可能」という意味です。*10

最後に、全部のコードを載せておきましょう

import scalaz._
import Leibniz._

sealed abstract class Foo[A, B] {
  def cata[Z](x: (A === B) => Z, y: (A, B) => Z): Z = this match {
    case X() => x(Leibniz.force[Nothing, Any, A, B])
    case Y(a, b) => y(a, b)
  }
}
final case class X[A]() extends Foo[A, A]
final case class Y[A, B](a: A, b: B) extends Foo[A, B]

object Main {
  def hoge[F[_, _], A, B, C](foo: Foo[A, B], bar: F[A, C]): F[B, C] =
    foo.cata(
      _.subst[({type λ[a >: Nothing <: Any] = F[A, C] === F[a, C]})#λ](refl).apply(bar),
      (a, b) => ???
    )
}

scalaVersion := "2.11.1"

libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.1.0-RC1"

単にキャストすればすむもの*11を、Leibnizを使って安全にキャストするために、これくらい色々とやらなければいけなくて、とても面倒です。

さて、なんでこんなこと書いたのか？というと、実際のコードでこの問題に遭遇したからです。もみあげさんが、HaskellのコードをScalaに移植してるらしいのですが

• https://github.com/atzeus/reflectionwithoutremorse 移植元
• https://github.com/pocketberserker/reflectionwithoutremorse-scalaz 移植中

自分もいじってみて、とりあえず

「ScalazのFreeと同様に、型がAnyに落ちてしまう問題」

https://github.com/scalaz/scalaz/commit/d76c426b2b9

があったので、抽象型つかった面倒なテクニック使って一部書き直しました

https://github.com/xuwei-k/reflectionwithoutremorse-scalaz/commit/3833aec222

そうした時点で、コンパイルエラーが6箇所でした。それで、その6箇所は、全部上記のパターンで、(この方法がベストなのかどうかは別として)ひとまずLeibniz使えば解決可能なようです。

めでたしめでたし?

しかし、Leibniz使えば解決可能とはいえ、これとても面倒なので、もっと優れた解決方法募集中です・・・Scalaつらい・・・

追記

解決策ではないが、有用っぽい情報もらったので、そのままtweet貼っておく

ツイートする