まず、下記の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使って同様のコード書くと、コンパイル通るらしいです。これの話をします。*1
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()
でパターンマッチしたあと、というところです。
最初、*2これの意味がわかるのに何時間もかかってしまいました。が、わかってしまえば単純といえば単純かもしれません(?)
そして「Haskellこんなことできるのか、すごい!」となりました。*3
さて、解説に入っていきます。FooはXかYのどちらかになる、代数的データ型です。また、型パラメータを2つとります。ここで
「FooがXの場合に、Fooの型パラメータは、2つとも同じものが当てはめられている」
というのがポイントです。*4つまり
「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だと通常それは不可能なはずです。*5 うっ、Scalaつらい・・・。
Scalaにおいては、実質単にキャストしてしまえば解決する問題です。しかし、キャストは安全ではないので使いたくないですね?この場合、Scalaが貧弱なだけで、本当は安全にキャストというか
「AとBが同じ型」という情報をもとに「"F[B, C]" と "F[A, C]" も同じ型」という情報を導く
ということをしたいのです。
そして考えた結果、scalaz.Leibnizを使えば、一応できる気がしたのでそのやり方を紹介します。他にもっと簡単な方法があったら誰か教えて下さい。
https://github.com/scalaz/scalaz/blob/v7.1.0/core/src/main/scala/scalaz/Leibniz.scala
さて、Leibnizという聞きなれない単語ですが、自分もこの言葉の由来とかしりません。*6 ScalazのLeibnizのscaladocに論文のリンクあるので、興味のある人はそれ読んでください。
Leibnizがなんなのか?を一言でいうと
「Scala標準ライブラリのPredefにある =:= と同じだが、合成可能で優れてるもの」
でしょうか。ちょうどそのあたり、最近typelevel.orgにblog記事上がってるので読みましょう
http://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html
http://typelevel.org/blog/2014/07/06/singleton_instance_trick_unsafe.html
また、そもそも「Predefにある =:= 」を知らない人は、yuroyoroさんのこれ
Scalaで <:< とか =:= を使ったgeneralized type constraintsがスゴすぎて感動した話
などを読みましょう。また、これもScalazのversionによって変わらないとは思いますが、一応これ書いている時点の最新であるScalaz 7.1.0としておきます。
「合成可能」がどういうことか?というと、つまりは例えばさきほどのように
「AとBが同じ型」なら「"F[B, C]" と "F[A, C]" も同じ型」
という判断が可能になる、ということです。もう少し言い換えると
「A === B」が存在すれば、そこから「F[B, C] === F[A, C]」を生成可能
です。ここでいきなり === という記号が出てきましたが、
というだけです。*9
では実際に、最初のコード例をscalaz.Leibniz使って書いていくとどうなるか?の詳細な説明です。
まず、パターンマッチはやめて、Fooにcatamorphismのためのメソッドを定義します。*10
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) }
とても残念*11ですが、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が合成可能」という意味です。*12
最後に、全部のコードを載せておきましょう
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"
単にキャストすればすむもの*13を、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貼っておく
@dico_leque おっ、自分が書いたこれ URL って、やはりそのissueと同じ問題なんですかね?
*1: 追記: ちなみに、GADTs自体はScalaでも可能で、今回の話はGADTsそのものとはある意味別らしい?です。コメント欄の議論参照してください
*2:実際の例はもう少しだけ込み入っていたり、他の可能性を探っていたりしたので
*4:ちなみにYのほうは、単に説明のためにX以外のものがとにかく必要だっただけで、具体的にa: Aやb: Bのフィールドを持っているのは、なんの意味もありません
*5:この後にこれを頑張る方法紹介しますが、Scalaで誰かそれ以外の方法知ってたら教えて下さい
*6: https://twitter.com/xuwei_k/status/485617226406309890
*7:ちなみに、それ書いたのは、Scalazのコミッター、かつekmettの同僚、かつekmettが作ってる ermine https://github.com/ermine-language 一緒に作ってる人、です
*8:⊥ や ⊤ は、NothingやAnyのalias
*9:ちなみに、scalaz.Equalのsyntaxに===がありますが、それとは直接は関係ありません
*10:べつに、必ずしもcatamorphismのメソッド定義する必要なかった気もする?
*11:このあたり色々勝手にやって欲しいのに、手動でしかも安全でないメソッドで生成するのが残念、ということ
*12:このsubst以外にも、いくつかメソッドあります
*13:実際の処理としても、結局はキャストしてるだけ