scala/存在型入門 - Windymeltの公開メモ帳

scala/存在型入門

#scala #型

存在型というのがある

全称型と対になる存在

全称型: Scalaにおける型パラメータ、いわゆるジェネリクスのこと

二人はマブダチ

全称型と存在型とで、型を量化できるようになる

量化: (型の文脈では)特定の型に限った話ではなくて、「こういう型ならなんでも」という柔軟な制約を導入すること

! オレオレ定義なのであまり真面目に読まないで

持っておきたい視点: 型とは制約である

型は主張だと言ってもいい

型は何を主張するのか？→この型に対応する値があるはずです、ということ

Int型は「整数があるはず」と言っている

これだけだと意味不明だが・・・

def add(n: Int, m: Int): Intは「Intがあって別のIntがあったら、対応するIntがあるはず」ということを言っている

カリーハワード同型対応というのを学ぶとなるほど〜となるはず

型は命題に対応するよ

値/実装はその証明に対応するよ

code:scala

val x: Int = // Intが存在するはず(命題)

42 // 本当だ〜 (証明)

// カード番号と製品番号があれば、製品が存在するはず

def buy(cardNumber: String, productId: String): Product

// ユーザIDがあれば、ユーザのエンティティが得られるかもしれない

def findUserById(id: UserId): OptionUserEntity

実装がホンマに正しいかはプログラマの責任ということになっている

そこはテストで保証すること

すくなくとも型レベルではコンパイラが正しさを保証する

関数は型から型への対応付けを定義している

ここでは(IntとInt)をIntに写す一対一対応を定めている、ということになる

全称型, universal types (型パラメータ/ジェネリクス)

全称型からおさらいしていく

全称型が主張していること: 「任意の型Aについて、この型が成り立ちますよ」

成り立つ: その型の有効な値がかならずある、くらいの意味

値レベルで考えると、引数に対して返り値の値が存在することを保証している

具体例

code:scala

type PairA = (A, A)

「任意の型Aについて、Pairという型が成り立って、その中身は(A, A)になるはずですよ」

「任意の型Aの値があるなら、(A, A)という型の値もあるはず」

Scala 3でType Lambdaが導入されたので、より直感的に以下のように書き下すことができる:

code:scala

type Pair = A =>> (A, A)

「適当な型Aをくれたら作れまっせ〜」というのがよくわかる

あらゆる型Aについて、Pair[A]の値は存在できる

より卑近な例を挙げると、Option[A]とかList[A]などがある

「任意の型Aについて、Option型を作れますよ」「任意の型Aについて、List型を作れますよ」

前述したように、その型の値を作れる証明は実装で示す

code:scala

def makePairA(a: A): PairA = (a, a) // 自明な証明だが・・・

全称型で導入した任意の型、例えばAはまったく制限がないので、どんな型がきても良いように実装しなければならない

全称型の何がうれしいか

いろいろな関数を書いていくと，引数の型に関わらず同じことをする関数が出現する場合がしばしば現れる．

... これらの関数は引数の型を除いて同じ格好をしている．それならば，共通部分はひとつの定義におさめ，差異をパラメータ化できないだろうか? パラメータ化するとしたら，パラメータは一体なんであろうか?

高階関数，多相性，多相的関数

型だけ違っていて実装は全く同じ関数、クラス、etc. というものを抽象化する能力を獲得できる

もしジェネリクスがなかったら？

使いたい型ごとにListForInt, ListForString, ListForBoolean, ... を定義しなければならない

しかも実装はほぼ同じ

実例

code:scala

def swapA, B(pair: (A, B)): (B, A) = // 任意の型A, Bについて、(A, B)があるとき、(B, A)の値があります

(pair._2, pair._1) // その証明はこれです

具体的な型が一度も登場しなかったけど、便利なものが作れた

存在型, existential types

存在型に対応する機能はこれです、というものは明にはない

古代のScalaにはforSomeがあったが、別にそれを使わなくても同じことができるので削除された

全称型と比べると、明示的に取り扱われることが少ない

その理由はあとでわかる

! 全称型と存在型とでは、全称型のほうが制約がかなり強い

存在型が主張していること: 「この型を満たすようなAがどっかにありますよ」

？？？

言い換えると: 「型の制約はあるけど外には見せない」 -- つまり内的な制約の表現に向いた量化

外に見せないことで何が嬉しいのか？

外に見せてる例: 全称型

code:scala

type PairA = (A, A)

Aを外に見せており、外から制約を与えられる

外に見せない: 存在型

code:scala

trait Pair2:

type Inner

val lhs: Inner

val rhs: Inner

外からはBoxなので内部の制約は見えない

同じことを全称型でやると:

code:scala

trait Pair2Inner

val lhs: Inner

val rhs: Inner

一緒じゃん

と思いますが・・・

制約の強さがぜんぜん違う！

具体例

いったん、明に存在型を利用するようなシナリオについて説明する

TypeScriptでexistential typeが欲しくなったときはカプセル化で我慢しようからほぼ転載

ジョブキューみたいなのがあるとする

関数と、それに渡す引数をペアにして、そのリストを保持したい

当然ながら、関数と引数はちゃんと型が合致している必要がある

A => Unitという関数があったらAとしかペアになれないよ、ということ

あたりまえ

任意の型Aで成り立ちそうなので、ペアをtraitと型パラメータを使って表現してみる。つまり全称型で試してみよう

code:scala

trait DispatchmentA:

val func: A => Unit

val arg: A

値は以下のようにして作れる:

code:scala

val d1 = new DispatchmentInt:

val func: Int => Unit = println(_)

val arg: Int = 1

コンパイラが制約を守っているか確認するので、funcとargが噛み合わないDispatchmentを作ることは許されない

「任意の型Aについて、Dispatchment[A]が成り立ちますよ」という主張が守られる

そうだね

実際にDispatchmentを利用し、実際にfuncを実行する関数を作る

code:scala

def dispatchA(d: DispatchmentA): Unit = d.func(d.arg)

dispatch(d1) // => Unit

// 1と出力される

やったー

ところでジョブキューなので、リストで一斉に処理したい

素朴にforeachするか・・・

code:scala

def dispatchAllA(ds: Seq[DispatchmentA]): Unit = ds.foreach(dispatch)

ところがこれだと困る。以下のようなd2があるとする:

code:scala

val d2 = new DispatchmentString:

val func: String => Unit = println(_)

val arg: String = "Hello, World!"

List(d1, d2)を渡すとうまくいくだろうか？

d1: Dispatchment[Int]とd2: Dispatchment[String]との型が違うので、呼び出せない！

dispatchAllの型をもう一度見てみると・・・

def dispatchAll[A](ds: Seq[Dispatchment[A]]): Unit

「任意の型Aについて、Seq[Dispatchment[A]]があるとき・・・」と主張している

任意の型Aと言ってしまっているので、Dispatchment[A]の型が固定されてしまう！

そこで、Dispatchmentから引数の型Aを隠します

code:scala

trait Dispatchment:

val func: A => Unit

val arg: A

しかしこれだとAが定義されていないので動かない

Scalaはtraitの中にもtypeを置けるのでDispatchmentの中でtypeを仮置きしてしまう

code:scala

trait Dispatchment:

type A

val func: A => Unit

val arg: A

このDispatchment型が主張しているものは何？

「仮にfunc: A => Unitとarg: Aがあったとして、これらを満たすようなAという型があるはずです」

全称型よりもかなり弱い主張をしている

任意の型Aについて成り立つかは分かんないっス

でもDispatchment型の値が成り立つのであれば、型を満たすようなAがあるはずっス

以前に述べた通り、型の証明は実装で示すのだが、その困難さが違う

全称型: Aがなんのかはまったく分からないが、とにかく成り立つような実装が必要

きびしい！

「任意の型について成り立つ」なので外側から型引数が与えられる

存在型: 具体的にその型が成り立つようなAを一つでも示せば実装が成り立つ

かんたん！

「成り立つ型が存在する」なので実装する側が型を決めていい

! 内部的な型の制約を与えたいときに利用しよう

こうして作られた、型パラメータを持たない(i.e. 全称型ではなく存在型を用いて量化した)Dispatchmentではうまくいくだろうか？

code:scala

def dispatchAll(ds: SeqDispatchment): Unit = ds.foreach(dispatch)

型から型変数が消えているので、うまくいく

それでいて、各Dispatchmentの中の制約は守られる

「型はなんでもいいけど、Dispatchmentの中の制約は守ってくださいね〜」

やったー

実装レベルの話をすると、(明に扱う)存在型とはtrait内部で抽象型変数を置くこと、と言ってもよい

対になること: 全称型とはtraitなどで型パラメータを用いること、と言ってもよい

実装を提供する(i.e. 型を証明する)ときにその違いがあらわれる

存在型はどこにでもある

存在型は全称型よりもはるかに制約が弱いことがわかった

実装する側は1つでも該当する型があればよい、つまり具体例を与えるだけでよいため

はるかに制約が弱いので、明に言語機能として利用するのではなく、自然と他の言語機能に溶け込む形で利用されている

code:scala

def output(x: { def show: String }): Unit = println(x.show)

これは「show: Stringを持っている」という制約を満たすような型であるところのxが欲しいです、と言っている

すべての型Aについて・・・という要求はしていない

具体例を変数として1つだけ渡せばよい

code:scala

trait Showable:

def show: String

同じことをtraitで書いたものだが、「こういう制約を満たす型があったらください」と言っているので、存在型といえる

Q.「存在型をつかいこなしてみたいです！」

A. もう使ってます

Scalaのtrait、Rustのtrait、Swiftのprotocolが、それです

「それを実装できるような型であればなんでも」と言っているので、存在型そのもの

存在型は、全称型よりも柔軟な制約をもたらす

? いつ明示的に存在型を書くべきか？

型の中に内的な制約があるとき

e.g. 関数と引数の型は整合していなければならない

全称型とワイルドカード

全称型を使うと柔軟な制約をうまく表現できない、という話をしばらく前にした

code:scala

trait DispatchmentA:

val func: A => Unit

val arg: A

def dispatchA(d: DispatchmentA): Unit = d.func(d.arg)

def dispatchAllA(ds: Seq[DispatchmentA]): Unit = ds.foreach(dispatch)

なんで困るかというと、型変数Aが明に露出しているため、コンパイラがAを具体的な型で固定してしまうから

ありがたいことに、ScalaやJavaでは、「型変数だけど別になんでもいいよ」というのを表現するためのワイルドカード型がある

Scalaだと?を渡す

code:scala

def dispatch(d: Dispatchment?): Unit = d.func(d.arg)

def dispatchAll(ds: Seq[Dispatchment?]): Unit = ds.foreach(dispatch)

「Dispatchment型だけど、渡す型が何かは知らん」

?を渡すと名前がつかなくなるので、関数の型パラメータからは消えてしまう

dispatchとdispatchAllから型パラメータリストがなくなっている

結果的に、存在型がやっていることと同じことができる

! ワイルドカード型を使うと全称型でも存在型として利用できる

整理すると、以下のことが言える

全称型が成り立っているとき、これを変形してつねに存在型が得られる

「任意の型Aについて・・・」が成り立っているのだから、「この型が成り立つような型Aが存在する」は当然導けますね

制限を弱めているだけ

Scalaのtrait

全称型も存在型もtraitでエンコーディングできて便利!!!