Underground型システム

Underground 型システム Show（@ajfAfg） 関数型まつり 2025

Show（@ajfAfg） プログラミング言語と型が好き 2025/6/15 関数型まつり 2025 2

Overground型システム • 型システムとは、ある種のバグを静的に検査可能な手法のこと • 多くの型システムは健全性を満たす 正しいことしか言わないよ的な性質 2025/6/15 関数型まつり 2025 3

Underground型システム • 実世界の型システムは健全性を壊す「穴」が存在することも • つまり、型検査が通っても実行時エラーが出る場合がある • 罠を事前に知って、型システムをもっと有効活用！ 2025/6/15 関数型まつり 2025 4

Java編 バージョン: OpenJDK 25-ea 2025/6/15 関数型まつり 2025 5

Quiz: 実行時エラーはどこで起きる？ 2025/6/15 関数型まつり 2025 6

Quiz: 実行時エラーはどこで起きる？ Exception in thread "main" java.lang.ArrayStoreException: A 2025/6/15 関数型まつり 2025 7

Quiz: 実行時エラーはどこで起きる？ Exception in thread "main" java.lang.ArrayStoreException: A 2025/6/15 関数型まつり 2025 8

原因深掘り（1/2） • クイックな回答 • Javaの配列の部分型付けが共変だから • 共変とは <∶は二項演算子で、SはTの部分型と読む • 型引数を取る型I<S>, I<T>に対して、S<∶TならばI<S><∶I<T> となること • なお、双対な概念として反変がある • T<∶SならばI<S><∶I<T>（前提の順序が逆） 2025/6/15 関数型まつり 2025 9

原因深掘り（2/2） • 配列の部分型付けが共変だと 何が問題？ • →配列の要素を書き換える際に困る foo的には?<∶Sを期待 S[] foo 参照 ・・・・・・ ?にはSもTも入りうるので、 S<∶SかつT<∶SかつS<∶TかつT<∶T が満たされてほしい T[] bar bar的には?<∶Tを期待 2025/6/15 関数型まつり 2025 10

余談: 配列が共変な理由 • JDK 1.5以前はジェネリクスがなかったから • 配列の要素に関わらず使用可能な関数を定義するとき、 Object[]として受け取るしかなかった TAPLに書いてた 2025/6/15 関数型まつり 2025 11

余談: AltJavaの配列の変性 • ScalaとKotlinは非変 • つまり、S<∶TかつT<∶S • 右のコードはコンパイル時に怒られる • （AltJavaではないけど）TypeScriptは…… • 共変みたいです（なんでだろ） TypeScriptに おける配列の共変性| sititou70 • C.f. TypeScriptにおける配列の共変性 | sititou70 2025/6/15 関数型まつり 2025 12

• https://sititou70.github.io/TypeScriptにおける配列の共変性/

OCaml編 バージョン: 5.2.1 2025/6/15 関数型まつり 2025 13

Quiz: 実行時エラーはどこで起きる？ https://github.com/ocaml/ocaml/issues/7241#issuecomment-1594348867 から引用 2025/6/15 関数型まつり 2025 14

• https://github.com/ocaml/ocaml/issues/7241#issuecomment-1594348867

Quiz: 実行時エラーはどこで起きる？ segmentation fault ocaml foo.ml https://github.com/ocaml/ocaml/issues/7241#issuecomment-1594348867 から引用 2025/6/15 関数型まつり 2025 15

• https://github.com/ocaml/ocaml/issues/7241#issuecomment-1594348867

Quiz: 実行時エラーはどこで起きる？ segmentation fault ocaml foo.ml https://github.com/ocaml/ocaml/issues/7241#issuecomment-1594348867 から引用 2025/6/15 関数型まつり 2025 16

• https://github.com/ocaml/ocaml/issues/7241#issuecomment-1594348867

原因深掘り • クイックな回答 • ガード節で破壊的変更をしてるから • 最後の節で取りうる組み合わせは、{a=true;b=Some y}のみ • なので、コンパイラ的には、検査なしにSomeの中身を参照しても ええやろ！と判断できる • そのはずだったのにガード節でbがNoneに変更されてしまった 2025/6/15 関数型まつり 2025 17

余談: Ocaml 5.3.0で修正されました 2025/01/08リリース！ • 実行時検査が入るようになり、セグフォで落ちなくなった • 「Exception: Match_failure」で落ちるようになった • 型検査時に落とすのは難しいかも…… OxCamlか？ • Rustはこの種のエラーを静的に検出できるが、それは所有権のおかげ • HaskellやErlangのように、ガード節で非純粋関数を呼び出せないよう にする方針もありそう 2025/6/15 関数型まつり 2025 18

Rust編 バージョン: 1.84.0 2025/6/15 関数型まつり 2025 19

時間ないのでいきなり解答！ 何もプリントされない 2025/6/15 関数型まつり 2025 20

原因深掘り • 前提として、配列のcloneは 要素の型がCopyを実装しているならば copyが使われる • Vecも同じ（c.f. 1521-copy-clone-semantics - The Rust RFC Book） • Weirdはstaticな場合にのみCopyを実装しているが、Rustのバグに より、ライフタイムを無視してcopyが使われた • rust-lang/rust#132442 2025/6/15 関数型まつり 2025 21

• https://rust-lang.github.io/rfcs/1521-copy-clone-semantics.html
• https://github.com/rust-lang/rust/issues/132442

原因深掘り • 前提として、配列のcloneは 要素の型がCopyを実装しているならば copyが使われる • Vecも同じ（c.f. 1521-copy-clone-semantics - The Rust RFC Book） • Weirdはstaticな場合にのみCopyを実装しているが、Rustのバグに より、ライフタイムを無視してcopyが使われた • rust-lang/rust#132442 2025/6/15 関数型まつり 2025 22

• https://rust-lang.github.io/rfcs/1521-copy-clone-semantics.html
• https://github.com/rust-lang/rust/issues/132442

アングラ 最高！！ 2025/6/15 関数型まつり 2025 23

もっと型システムの闇が知りたい方へ https://counterexamples.org/ 2025/6/15 関数型まつり 2025 24

• https://counterexamples.org/