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 B は A と B の交差型を作ります。

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

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

否定型

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

type Not[A] = A => Nothing

// もしくは
// 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]
}

これは任意の A に対して P[A] が成り立つことを表します。

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

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

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

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

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))

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

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

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

opt2list はOptionからListへ、list2opt はListからOptionへの変換を行います。

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 }]

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

この Forall の定義で opt2list と list2opt を実装すると以下のようになります。

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

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

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

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

関数リテラルが使えることでより簡単に Forall の値を作ることができます。

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

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

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

二重否定の除去は継続の呼び出しに対応します。

これを用いて mapping は以下のように定義できます。

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))

callCC は Forall に具体的な型を与えて利用するので少々冗長な記述になります。

参考