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

haskell scala scalaz

まず、下記の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記事上がってるので読みましょう

*7

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]」を生成可能


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

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

というだけです。*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に移植してるらしいのですが

自分もいじってみて、とりあえず
「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貼っておく

*1: 追記: ちなみに、GADTs自体はScalaでも可能で、今回の話はGADTsそのものとはある意味別らしい?です。コメント欄の議論参照してください

*2:実際の例はもう少しだけ込み入っていたり、他の可能性を探っていたりしたので

*3:一番下に追記しましたが、OCamlもできるらしい

*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:実際の処理としても、結局はキャストしてるだけ