Scalaの合併型と全称型

カリー=ハワード同型対応から交差型と存在型を用いて合併型と全称型を導きます。

Scalaの型と論理

Scalaが標準で備える型と論理の対応は次のようになります。

論理
Any
Nothing
A with BA かつ B
A => B または A <:< BA ならば B
P[A] forSome { type A }P[A] である A が存在する

Anyは全ての型のスーパータイプ、Nothingは全ての型のサブタイプです。

A with BABの交差型を作ります。

A <:< BABのサブタイプであることを表します。

forSomeは存在型を構成します。

否定型

この対応から論理における否定は次のようになります。

type Not[A] = A => Nothing

Nothingはボトム型なのでNothing以外の型では包含関係を満たせないことがわかります。

また、Scalaの型システムにおいてNot[Not[A]] =:= Aが成り立たないことに注意しましょう。

合併型

この否定型と交差型を使って合併型を作ることができます。

type Or[A, B] = Not[Not[A] with Not[B]]

この定義はド・モルガンの法則から導かれます。

合併型は次のように使うことができます。

def double[A](a: A)(implicit ev: Not[Not[A]] <:< Or[Int, String]): String =
  a match {
    case i: Int => (i + i).toString
    case s: String => s + s
  }

assert(double(2) == "4")
assert(double("2") == "22")

Orが二重否定を含むためNot[Not[A]]とすることで型を合わせています。

このdouble関数はInt型とString型以外の値を受け付けません。

また、Eitherに比べ値をラップする必要がなく効率が良いです。

構造的部分型

構造的な型に対しても合併型は直感的な包含関係を満たします。

構造的な型に対する交差型は各フィールドの和集合を持つ型をスーパータイプに持ちます。

type Foo = { def foo: String; def baz: Int }
type Bar = { def bar: String; def baz: Int }
implicitly[Foo with Bar <:< { def foo: String; def bar: String; def baz: Int }]

構造的な型に対する合併型は各フィールドの積集合を持つ型をスーパータイプに持ちます。

type Foo = { def foo: String; def baz: Int }
type Bar = { def bar: String; def baz: Int }
implicitly[Or[Foo, Bar] <:< Not[Not[{ def baz: Int }]]]

Scalaでは構造的部分型があまり使われませんが、例えばJSONの型付けなどに利用できるかもしれません。

全称型

Scalaにおける全称型は次のように定義できます。

trait Forall[P[_]] {
  def apply[A]: P[A]
}

これを用いると任意の型を扱う値を表現できます。

type Nat[F[_], G[_]] = Forall[({ type H[A] = F[A] => G[A] })#H]

def mapping[F[_], G[_], A, B](f: Nat[F, G])(pair: (F[A], F[B])): (G[A], G[B]) = (f[A](pair._1), f[B](pair._2))

def opt2list: Nat[Option, List] =
  new Nat[Option, List] {
    def apply[A]: Option[A] => List[A] = _.toList
  }

assert(mapping(opt2list)((Some("hoge"), None)) == (List("hoge"), Nil))

def list2opt: Nat[List, Option] =
  new Nat[List, Option] {
    def apply[A]: List[A] => Option[A] = _.headOption
  }

assert(mapping(list2opt)((List(0, 1, 2), Nil)) == (Some(0), None))

Nat[F, G]は任意の型Aに対してF[A]G[A]に対応させる型です。

mapping(F[A], F[B])Nat[F, G]を使って(G[A], G[B])に変換します。

この全称型もまた否定型と存在型により表現が可能です。

全てのAはPであるということはPでないAは存在しないと言い換えることができます。

type Forall[P[_]] = Not[Not[P[A]] forSome { type A }]

この全称型も合併型と同様に二重否定を含みます。

継続渡し形式(CPS)により二重否定を導入できます。

def opt2list: Nat[Option, List] = k => k(_.toList)

def list2opt: Nat[List, Option] = k => k(_.headOption)

利用する際には二重否定を除去する必要があります。

最も簡単な定義はreturnを使ったものです。

def callCC[A](f: Not[Not[A]]): A = f(a => return a)

これで最初に定義した全称型と同じように使えます。

def mapping[F[_], G[_], A, B](f: Nat[F, G])(pair: (F[A], F[B])): (G[A], G[B]) =
  (callCC[F[A] => G[A]](f)(pair._1), callCC[F[B] => G[B]](f)(pair._2))

assert(mapping(opt2list)((Some("hoge"), None)) == (List("hoge"), Nil))

assert(mapping(list2opt)((List(0, 1, 2), Nil)) == (Some(0), None))

この定義は関数リテラルが使えるためtraitで定義した場合よりも簡単に全称型を作れます。

参考