Elixirと私の未来: 集合論型 by José Valim

原文: https://elixir-lang.org/blog/2022/10/05/my-future-with-elixir-set-theoretic-types/

続報!!! https://qiita.com/zacky1972/items/33fd39ef2a1dcdbb8b73

本記事は，Elixir と私の未来に関する3つの記事シリーズです．ElixirConf Europe 2022とElixirConf US 2022のKeynoteからの抜粋が含まれています．

Elixir の最初の公開リリースである Elixir v0.5が発表されてから10周年を，2022年5月にて，迎えました．

こういう時には，Elixirが10年後にどのようになるかを予測したくなるかもしれません．しかし，それは無駄な努力だと思います．なぜならば，10 年前には，Elixir がウェブ開発に優れている(訳註: Phoenix Framework)だけでなく，組込みソフトウェア(訳註: Nerves Project)のような分野に進んだり，Nx (Numerical Elixir)，Explorer，Axon，Livebookなどのプロジェクトで，機械学習やデータ分析に参入したりするとは想像もしていなかったからです．Elixirは拡張できるように設計されており，それをどのように拡張するか，常にコミュニティが取り組んでいます．

これらの理由から．私はElixirと私の未来に焦点を当てることにしました．これらは，私が個人的に興奮している，他のコミュニティメンバーとともに取り組んでいるプロジェクトです．今日の記事の話題は，2022年5月の ElixirConf EU プレゼンテーションで説明した型システムです．

見て見ぬふりをしていた問題(the elephant in the room): 型

何年にもわたり，Elixir Core Teamはコミュニティの最大のニーズに対応してきました．Elixir v1.6 ではElixirコードフォーマッタが導入されました．これは，成長するコミュニティと大規模なチームが，大規模なコードベースに関するスタイルガイドと規約の必要性を認識したためです．

Elixir v1.9 では，リリース機能を言語に組み込んでサポートすることにしました: すなわち，アプリケーションコード．そのすべての依存関係，およびErlang VM全体とランタイムで構成される自己完結型のアーカイブをリリースする機能です．その目標は，ElixirコミュニティとErlangコミュニティの両方で試みられたアプローチを公式ツールに導入することで，Elixirプロジェクトをデプロイする際に困難だと認識されている問題に対処することでした．リリース機能を言語機能として組み込んだことにより，Phoenixアプリケーションに合わせたDockerfileを自動的に生成するmix phx.gen.releaseなど，将来の自動化への道が開かれました．

コミュニティとの関係性を考えると，Elixirと私の将来について，今日のコミュニティの最大のニーズであると思われる静的型付けに触れずに語るのは不誠実であろうと思います．しかし，コミュニティでElixirに静的型付けを要求している時，私たちは実際には何を期待しているのでしょうか？ Elixirコミュニティは静的型付けによってどんな利点を得られるのでしょうか？

型とElixir

プログラミング言語やプラットフォームが異なれば，型から得られる価値も異なります．他の言語における価値は，Elixirにも適用される場合と適用されない場合があります．

たとえば，他の言語では，型によってパフォーマンス上の利点を引き出すことができます．しかし，Elixirでは，動的に型付けされる Erlang VM 上で実行される関係で，Elixirコードを型付けしても意味のあるパフォーマンス向上を期待できません．

型による別の利点は，ドキュメンテーションを支援することです(型がドキュメントに取って代わるとは思えないので，支援という言葉をあえて使う点に注意してください)． Elixirでは既にTypespecs(訳註: @specによる型記述のこと)から同様の利点を享受しています．統合型システムによって，この分野にさらに価値をもたらすと期待しています．

しかしながら，静的型付けの長所と短所は，特にテストなどの他のソフトウェア検証手法と型を比較する際に，コードの保守という文脈で議論すると，正しく認識されなかったり，誇張されがちになったりします．そのような状況では，「静的型システムにより，Elixirのコードのバグの8割を捕捉できる」とか「静的型が得られると，より少ないテストを書くだけで済む」などの非現実的な主張をよく耳にします．

ElixirConf Europe 2022のkeynoteで，これらの主張が真実ではないと私が思う理由を探りますが，静的型システムがバグの検出に役立つという主張は，静的型システムによって特定するはずのバグの種類を正確に議論しない限り役に立ちません．

たとえば，Rust の型システムは，メモリ割り当ての解放を2回以上実行することや，ダングリングポインタ(訳註: 無効なメモリ領域を指し示すポインタ)，スレッドでのデータ競合といったバグを防ぐのに役立ちます．しかし，そのような型システムを Elixir に追加することは非生産的です．それらのバグを防ぐという特性は，ガベージコレクターとErlangランタイムによって既に保証されているため，そもそも遭遇するバグではないからです．

このことは，別の論点をもたらします: すなわち，型システムは．コードに関する特定の特性を証明するために，特定のプログラミングスタイルを拒否する必要があり，そのことにより記述できるコードの量を自ずと制限することになります．しかし，Elixirの表現力を制限することは避けたいと考えています．なぜなら，正直なところ，言語のセマンティクス(訳註: セマンティクスは，プログラミング言語としての意味のことで，たとえば特定のプログラミング言語(たとえばElixir)で記述されたコードによって，どのように実行されるかを示すもの)——大部分は Erlang から継承したもの——に満足しているからです．

Elixir にとって，型システムの利点は主に契約プログラミング(訳註: 後述するように，呼び出し元(caller)と呼び出し先(callee)が整合するために満たさなければならない条件のことを指して契約(contract)と呼んでいます．詳しくは WikipediaのDesign by Contract や，Bertrand Meyer の書いたObject-Oriented Software Construction (邦訳: オブジェクト指向入門 原則・コンセプト，オブジェクト指向入門 方法論・実践)を参照してください．ただし後者はものすごいボリュームです)に関係しています。関数caller(arg)が callee(arg)という名前の関数を呼び出す場合，これらの関数は両方とも時間の経過とともに変化するため，その呼び出し元(caller)が有効な引数(arg)を呼び出し先(callee)に渡し、呼び出し元(caller)が呼び出し先(callee)からの戻り値の型を適切に処理することを保証したいと考えています(訳註: つまり，引数argと戻り値の型に整合性があることを保証したいということです)．

このような機能を提供するのを保証するのは単純に見えるかもしれません．しかし，小さなコード例でも難しい場合がありました．たとえば，負の数を返す negate関数を定義したとしましょう．次のように実装することができます:

def negate(x) when is_integer(x), do: -x

negateの型はinteger() -> integer()である(訳註: 整数を引数として受け取って，整数を戻り値として返すような関数である)と言えます．

ここで定義したnegateを使用して，次のようにsubtract関数を定義できます:

def subtract(a, b) when is_integer(a) and is_integer(b) do
  a + negate(b)
end

整数のみを扱っているので，これはすべて機能し，期待どおりに型チェックします．しかし，将来誰かがnegateをポリモーフィック(訳註: 複数の型を同じ関数で処理すること)にすることを決定したと想像してください．そのため，真偽値もnegate関数が適用されるとします:

def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

negate の型が integer() | boolean() -> integer() | boolean()である(訳註: 整数または真偽値を引数として受け取って，整数または真偽値を戻り値として返す関数である)とすると，subtractの実装で次のような偽陽性(訳註: 正しいコードなのに間違って「エラーである」と判定されること)の警告が表示されます:

Type warning:

  |
  |  def subtract(a, b) when is_integer(a) and is_integer(b) do
  |    a + negate(b)
         ^ the operator + expects integer(), integer() as arguments,
           but the second argument can be integer() | boolean()

(演算子+は2つの整数を引数として期待しているが，2番目の引数が整数または真偽値である)

したがって，関数間の契約プログラミングを型付けできるような型システムが必要であると同時に，偽陽性のような誤検知の警告を回避し，かつElixir 言語を制限しないようにしたいです． これらのトレードオフ(訳註: あちらを立てればこちらが立たず，のような関係性)のバランスを取ることは，技術的な課題であるだけでなく，コミュニティのニーズを考慮する必要もあります．Erlang で実装され、Elixir プロジェクトで利用可能な Dialyzerプロジェクトは，誤検知を避けることを選択しました．ただし，これは，特定のバグが検出されない可能性があることを意味します．

現時点では，たとえ誤検知が増えることを意味するとしても，コミュニティ全体が，より潜在的なバグを検出するシステムを好むようです．これは，Elixir と Erlang の文脈では特にトリッキーになる可能性があります．なぜなら，私はそれらを表明を用いた(assertive)言語(訳註: プログラムで，ある条件が常に成立することを前提にしていることと陽に表明することで，もし成立しない状況である時に，それは予期しない状態に陥っていることを意味するので，後述するようにElixirでは，そのような場合を検出した際にクラッシュさせる＝エラーを生成してプロセスを異常終了させることを推奨しています．これは，子プロセスの異常終了を検知して復旧・再起動させるスーパバイザーという機能と組み合わせることで，他の言語でするようなtry ... catch ...のようなエラー処理よりも，より適切に扱うことができるのがElixirの特長の1つになっています．このことを指して「表明を用いた言語」と呼んでいます)として説明するのが好きだからです．予期しないシナリオに直面するとクラッシュするコードを記述します．これは，アプリケーションの一部を再起動するためにスーパーバイザーに依存しているためです．この機能は，ElixirとErlangの言語で自己修復システム，フォールト・トレラント・システム(訳註: 障害(フォールト: fault)に耐性のあるシステム，耐障害性システム)を構築するための基盤です．

一方，これが Erlang/Elixir の型システムを非常にエキサイティングで唯一無二なものにしている理由です: コンパイル時と実行時の両方で故障モード(failure modes: 訳註: 故障の原因，すなわち，要求された機能を遂行する，機能単位の能力がなくなった原因を類型化したもの)をエレガントに処理する能力です．結局のところ，選択した型システムに関係なく，特にファイルシステム，API，分散ノードなどの外部リソースとやり取りするときに，予期しないシナリオに遭遇するためです．

重大発表

これは，ElixirConf EU 2022 からの大きな発表につながります: すなわち，集合論型に基づいたElixirの型システムを研究開発するための，進行中のPhD scholarship(訳註: 博士後期課程の学生を経済的に支援すること)を行なっています． Guillaume Duboc(博士後期課程学生)は，(この記事の原著者であり，Elixirの原作者である)José Valimの支援を受けて，Giuseppe Castagna(上級研究員)の指導のもとで，このPhD scholarshipを実施します．

このscholarshipは，CNRSとRemoteの提携です．これは、Supabase(採用活動中)，Fresha(採用活動中)，Dashbitの後援です．これらの企業は，すべて Elixir の将来に多額の投資を行っています．

なぜ集合論型か？

私たちは Elixir のすべてのイディオムをエレガントにモデル化できる型システムを望んでいます．一目見て，集合論型は見事に一致しているように思いました．集合論型では，集合演算を使用して型を定義し，対応する集合演算の結合則と分配則の特性を型が満たすようにします．

たとえば，Elixir の数値は整数または浮動小数点数になる可能性があるため，それらを和集合 integer() | float() として書くことができます(これはfloat() | integer() と等価です)．

前述の negate 関数を思い出してみましょう:

def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

この関数を，(integer() -> integer()) と (boolean() -> boolean()) の両方の型を持つ関数(訳註: すなわち，整数を引数として受け取った時には整数を返し，真偽値を引数として受け取った時には真偽値を返す関数)であると考えることができます．これは共通部分です．これにより，前節で説明した問題が自然に解決されます．整数で呼び出された場合，整数のみを返すことができます．

Elixir にはアトムと呼ばれるデータ構造もあります．それらは，独自の名前で与えられる値を一意に表します． たとえば，:sundayや:banana などです．型atom()は，すべてのアトムの集合と考えることができます．さらに，:sundayと:banana の値は、すべてのアトムの集合に含まれているため、atom() の部分型と考えることができます．:sundayと:bananaは値が1つしかないため，シングルトン型とも呼ばれます．

実際，それぞれの整数をinteger()集合に属するシングルトン型と見なすこともできます．型システムでシングルトンになる値の選択は，前節で定義したトレードオフに大きく依存します．

さらに，型付けされたElixirコードは型付けされていないElixirコードと結合して相互作用する必要があるため，型システムは段階的に導入できなければいけません．

個人的には，集合論的型は，型について推論するためのエレガントでアクセスしやすいアプローチだと思います．結局のところ，Elixir の開発者は，複数のclauseを含む関数を作成するときに，共通部分について考える必要はありませんが，内部を念入りに調べた(look under the hood)としてもモデリングは容易(straight-forward)です．

Elixir のセマンティクスと集合論型はこのように相性が一見していいようなのですが，この2つを組み合わせるには未解決の問題と既知の課題があります．ここではいくつかの例を示します:

• Elixir には，パターンマッチングとガードで使用されるイディオムによる強力な表現がありますが，それらすべてを集合論型に対応づけられるか？
• Mapと呼ばれるElixirの連想データ構造は，レコードとしても辞書としても使用できるが，それらも統一基盤で型付けすることは可能か？
• 段階的な型システムでは，健全性を保持するためにランタイム型チェックを導入する必要があるが，Erlang VM によって既に実行されている型チェックに加えて，これらの型チェックが行われるため，パフォーマンスが低下する可能性がある．したがって、Erlang VMによって実行される既存の実行時チェックを活用し，結果として得られる型システムが健全であることは可能か？

Giuseppe CastagnaとGuillaume Dubocと一緒に仕事をすることに興奮しているのは，まさにこれらの課題です．実装を深く掘り下げる前に，これらの問題とその解決策を形式化することが重要であると考えているからです．集合論型から始めるには，Giuseppe Castagna によるProgramming with union, intersection, and negation types(和集合・積集合・否定の型によるプログラミング)をお勧めします．

最後に，プロセス間のメッセージの入力など，現時点で取り組む予定のない領域があることに注意することが重要です．

期待とロードマップ

この時点で，Elixir は確実に将来のある時点で徐々に型付けされた言語になると予想しているかもしれません．しかし，私たちの前には長い道のりがあるため，そうではない可能性があることに注意することが重要です．

型システムを実装する際の課題の1つは，少なくとも私のように関連する学歴を持っていない人にとっては，1つの分割できないステップのように感じることです．1つは，途中でフィードバックを得る洞察や機会があまりないことです．したがって，段階的に型システムをElixirに組み込むことを計画しており，私はこれを「漸進的漸進型システム」と呼んでいます: つまり，漸進的型を漸進的に(徐々に)言語に追加するシステムです．

私たちが現在取り組んでいる最初のステップは，Elixirプログラムにある既存の型情報を活用することです．前述のように，Elixir では表明コードを記述します．つまり，パターンとガードには多くの型情報があります．この情報を取り上げて，既存のコードベースの型チェックに使用したいと考えています．Erlangコンパイラは，単一モジュール内のパフォーマンスを向上させるために既にそうしていますが，最終的にはモジュールやアプリケーション全体でもそうしたいと考えています．

このフェーズでは，Elixir開発者は型システムの利点を活用するためにコードを1行も変更する必要はありません．もちろん，既存のバグの一部のみをキャッチしますが，これにより，ストレステスト，ベンチマーク，開発者からのフィードバックを収集し，舞台裏で改善を行うことができます(または，それによって期待した通りにうまくいかないと思われる場合は，すべてを元に戻すことさえできます)．

次のステップは，型付き構造体を言語に導入することです．これにより，コードベース全体で構造体のパターンマッチを行うときに，構造体型がシステム全体に伝播できるようになります．この段階では，構造体を定義するための新しいAPIを導入しますが，これについてはまだ説明していません．開発者は，新しいAPIを使用してその利点を享受する必要があります．

最後に，改善と収集されたフィードバックに満足したら，Elixirコードベースで関数シグネチャ(訳註: 関数にそれぞれの引数の型と戻り値の型の注釈をつけたもの)を入力するための新しい構文を導入するために移行できます．これには，ポリモーフィック型などのより高度な機能のサポートが含まれます．これらを使用すると，Enumモジュールにあるような複雑な構造を入力できます．

心に留めておくべき重要な点は，これらの機能は段階的に調査および開発され，コミュニティからのフィードバックを収集する機会が十分にあるということです．また，私たちの経験が，型システムを既存のプログラミング言語に段階的に導入したいと考えている他のエコシステムに役立つことを願っています．

お読みいただきありがとうございます．また，今後の「Elixirと私の未来」シリーズの記事でお会いしましょう．

P.S. 合わせてこちらもお楽しみください．「Enum関数とパイプライン演算子からなるプログラミング「パラダイム」の起源: シリーズ「Elixirの歴史のインタビュー - Elixirの10周年を祝って」(1)」