Strong arrow: 段階的型付けの新しいアプローチ by José Valim

本記事は，ElixirConf US 2023 でのJosé Valimのkeynoteで議論された「段階的集合論的型付け」のトピック(The foundations of the Elixir type system)を元にした翻訳記事です．

元記事 "Strong arrows: a new approach to gradual typing"

Elixir の型システムの研究と開発は，CNRS 上級研究員の Giuseppe Castagna が主導し，Guillaume Duboc が博士課程の研究の一環として取り組んでいる進行中の取り組みです(元記事 : "Type system updates: moving from research into development" 翻訳: 「型システムのアップデート: 研究から開発への移行 by José Valim」)．

本記事では，Giuseppe Castagna et al. 2023(The Design Principles of the Elixir Type System)で提示されたアイデアを紹介することを目的として，提案された型システムが段階的型付けにどのように取り組むのか，またそれが集合論的型とどのように関連するのかについて説明します．

集合論的型

Elixir 用に現在研究開発している型システムは，集合論的な型に基づいています．つまり，その演算は，和集合・積集合・否定の基本的な集合演算に基づいています．

たとえば、アトム:okは Elixir の値であり，型 :ok で表すことができます．Elixir 内のすべてのアトムは，型システム内でそれ自体で表されます． :ok または :error のいずれかを返す関数は，:ok or :error を返すとします．ここで，or 演算子は和集合を表します．

:ok および :error 型は、すべてのアトムを表す無限集合である atom() 型に含まれています． :ok と atom() 型の和集合は，:ok or atom() として記述でき，atom() と等価です(:ok は atom() の部分集合であるため)． :ok と atom() 型の共通部分は、:ok and atom() として記述でき，:ok と等価です．

同様に，integer() は、すべての整数を表す無限集合です．integer() or atom() は、すべての整数とアトムの和集合です． 共通部分 integer() and atom() は空集合であり，これを none() とします．Elixir に存在するすべての型の和集合は term() です．

集合論的型の利点は，基本的な集合演算に基づいて Elixir プログラムに見られる多くの興味深い特性をモデル化できることです．これにより，Elixir での入力がより表現力豊かになり，アクセスしやすくなることが期待されます．有界数量化(bounded quantification) (または有界多相性(bounded polymorphism)) と呼ばれる型システムの特徴を集合論的型で実装する方法の例を見てみましょう．

上界・下界

恒等関数は引数を受け取り，それをそのまま返す関数です．Java では次のように記述します:

static <T> T identity(T arg) {
    return arg;
}

Typescriptでは次のとおりです:

function identity<T>(arg: T): T {
  return arg;
}

Haskellでは次のとおりです:

id :: a -> a
id arg = arg

上記のすべての例で、関数は型変数 T (または Haskell の場合は型変数 a) の引数を受け取り，同じ型 T の値を返すとします．関数のパラメーター(引数)が，多くの(poly)型をとる(morphs)ので，これをパラメトリック多相性(parametric polymorphism)と呼びます．Elixir では，次のように表します:

$ a -> a
def identity(arg), do: arg

場合によっては，これらの型変数をさらに制限したい場合があります．例として，Java の恒等関数を数値に制限してみましょう:

static <T extends Number> T identity(T arg) {
    return arg;
}

Typescriptでは次のとおりです:

function identity<T extends number>(arg: T): T {
    return arg;
}

HaskellではOrd などの型クラスに制約できます:

id :: Ord a => a -> a
id x = x

言い換えれば，これらの関数は，指定された制約を満たす限り，任意の型を受け入れることができます．受け取ることのできる型に制限を設けているため，これは有界多相性(bounded polymorphism)と呼ばれます．

そうは言っても，集合論的型で有界多相性を実装するにはどうすればよいでしょうか？ 型変数 `a`` があると想像してください．それが別の型に制限または制約されていることを確認するにはどうすればよいでしょうか？

集合論的型では，この操作は共通部分になります．a and atom() がある場合、a は :foo 型になりえます． a はすべてのアトム型を表す atom() 型にすることもできますが，integer() and atom() は空集合を返すため、a を integer() にすることはできません．言い換えれば，型変数に上界を設定するために共通部分を使用できるため，新しい意味論的構造を導入する必要はありません．したがって，Elixir の恒等関数を次のような数値に制限できます:

$ a and number() -> a and number()
def identity(arg), do: arg

もちろん，これらの制約に対するシンタックスシュガー(syntax sugar)を提供することもできます(訳註: つまり，1つ後のプログラムは，1つ前のプログラムと同じ意味で，よりわかりやすい表現としています):

$ a -> a when a: number()
def identity(arg), do: arg

しかし，結局のところ，それは単に共通部分にまで拡大するだけです(訳註: 前の共通部分の例a and atom() で，型変数aを最も大きくした場合は，atom()でした．そのことを指しています)．重要なのは，セマンティック レベルでは追加の構成や表現が必要ないということです．

注: 型に興味のある読者のために説明すると，集合論的型は，Kernel Fun 風の限定された形式の有界数量化(bounded quantification)を実装しています．一言で言えば，関数の範囲が同じである場合にのみ関数を比較できることを意味します．たとえば，私たちの型システムは，a -> a when a: integer() or boolean() が a -> a when a: integer() の部分型ではないことを示します．

下界も同様に取得できます．共通部分により型変数に上界を設定できる場合，型変数が常に和集合で拡張されることを指定するため，和集合は下界と等価になります．たとえば，a or atom() は,
結果には常にアトムと，a で指定された他のもの (1つのアトム，アトム型atom() 自体，または integer() などの完全にatom()と素な型の可能性がある) を含むことを示します．

Elixir のプロトコルは，Haskell の型クラス または Java のインターフェイスと同等の Elixirの構文であり，追加のセマンティクスなしで集合論的型をモデル化および構成できる機能のもう 1 つの例です．これを行うための正確なメカニズムは，読者の演習として残します(または将来のブログ投稿のトピック)．

段階的型付けを入力する

Elixir は関数型動的プログラミング言語です．既存の Elixir プログラムは型が指定されていません．つまり，型システムには，既存の Elixir コードを将来の静的に型を指定された Elixir コードとインターフェースするためのメカニズムが必要です．これは，段階的に入力することで実現できます．

1つの段階的な型システムとして，dynamic()型を定義する型システムがあります．?と表記されることもあります．any型として知られることもあります (ただし、TypeScript のような言語では短すぎて緩すぎるため、any は避けたいと思っています)．

Elixir では，dynamic() 型は，その型が実行時にのみ認識されることを意味し，その型の静的チェックを効果的に無効にします．さらに興味深いことに，集合演算を使用して動的型(訳註: dynamic()型ということか？)に上限と下限を設定することもできます．すぐにわかるように，これにより，型システムに関する興味深い特性が明らかになります．

段階的に入力するのが両方の言葉の長所であるとよく言われます．おそらく皮肉なことに，それは真であると同時に偽でもあります．段階的な型システムを使用するが，dynamic() 型をまったく使用しない場合，静的型システムとまったく同じように動作します．ただし、dynamic() 型を使用すればするほど，型システムが提供する保証が減り，dynamic() 型がシステム全体に伝播する量が増えます．したがって，dynamic() 型の出現をできる限り減らすことが私たちの関心事であり，それを実行することにしました．

静的コードと動的コードのインターフェイス:dynamic()の問題

数値のみを受け入れる制約付き恒等関数identityに戻りましょう:

$ a -> a when a: number()
def identity(arg), do: arg

ここで，次のような，この関数を呼び出す型指定されていないコードがあると想像してください:

def debug(arg) do
  "we got: " <> identity(arg)
end

debug/1 は型指定されていないため，その引数は型dynamic()を受け取ります。

debug/1 は引数を指定してidentityを呼び出し，文字列連結演算子(<>)を使用して"we got:"をidentity(arg)の結果に連結します．identity/1 は数値を返すことを目的としており，文字列の連結にはオペランドとして2つの文字列が必要であるため，このプログラムには入力エラーがあります．一方，実行時にdebug("hello")を呼び出すと，コードは機能し，例外は発生しません．

つまり，プログラムの静的型付けバージョンとその実行時の実行のふるまいは一致しません．では，これにどう対処すればよいでしょうか？

1つの選択肢は，すべてが期待どおりのふるまいであるとみなすことです．debug/1が型指定されていない場合，その引数はdynamic()型になります．このプログラムの型チェックを行うには，identity(dynamic()) がdynamic()型を返し，文字列とdynamic()の連結もdynamic() を返し，その結果，debug/1 は型dynamic()->dynamic()を取得し，型エラーは発生しません．

問題は，これはあまり有用な選択ではないということです．dynamic()がシステムに入ると，あらゆる場所に広がり，実行するチェックが減り，identity/1が数値を返すという情報が事実上破棄され，型システム全体があまり役に立たなくなります．

別の選択肢は，「dynamic()を使用して静的に型指定された関数を呼び出したら，dynamic()型を無視する」とみなすことです．関数が「number() を返す」と指定している場合，それは間違いなく数値です．このバージョンでは，identity(dynamic()) はnumber() を返し，文字列と数値を連結するときに型システムが型エラーを捕捉します．

これは，TypeScript で採用されているアプローチに似ています．これは，さらに静的なチェックを実行できることを意味しますが，debug("foobar") を呼び出すと，文字列"we got: foobar"が返されることも意味します．しかし，型システムが，identity がnumber()を返すと教えてくれたのに，どうやってそれが可能でしょうか？ これにより，実行時に混乱や予期せぬ結果が生じる可能性があります．このシステムは不健全(訳註: unsound，つまり，論証が妥当ではないか，その論証の前提の全てが真だとは言えないこと．ここでは後述のように実行時の型が一致しない問題がある)だと言えます．実行時の型がコンパイル時の型と一致しないからです．

これまでのところ，私たちのソリューションはどれも，静的ふるまいと実行時のふるまいを一致させようとしたものではなく，どちらかを優先して選択しました．

しかし，絶望しないでください．さらに別の選択肢があります．「動的 <-> 静的」の境界を越えるたびに実行時チェックを導入できます．この場合，`identity(dynamic())` は`number()`を返すとみなすこともできますが，それが事実であることを保証するためにコードに実行時チェックを導入します．これは，静的チェックを取得し，実行時に値が正しいことを確認しますが，実行時に追加のチェックを導入するというコストがかかります．残念ながら，データ構造の複雑さや「動的<->静的」の境界を何回越えたかによっては，これらのチェックがパフォーマンスに影響を与える可能性があります．

注: 最近の研究では，段階的型システムによって導入された実行時チェックを使用してコンパイラを最適化する方法が研究されています．これらのテクニックの一部は，パターンとガードに基づいてコードを最適化するために Erlang VM によってすでに活用されています．

要約すると，次の3つの選択肢があります:

• 動的コードから静的コードを呼び出すと，dynamic()が返され，さらなる静的型付けチェックの機会が失われます(これは健全です)．
• 動的コードから静的コードを呼び出すと静的型が返され，実行時に型の不一致が発生する可能性があります (これは不健全です)．
• 動的コードから静的コードを呼び出すと，実行時チェックが追加された静的型が返され，両方の動作が統合されますが，パフォーマンスに影響を与える可能性があります(これは健全です)．

Strong arrow　の導入

私はいつも，Erixir は Erlang のおかげでアサーティブな言語であると述べてきました，たとえば，恒等関数identityが数値のみに制限されている場合，実際には次のように記述することになるでしょう:

$ a -> a when a: number()
def identity(arg) when is_number(arg), do: arg

上の例では，数値以外の値が指定された場合，関数identityは失敗します．私たちはパターン・マッチングとガードに依存することが多く，これらは，作業している型を表明するのに役立ちます．それだけでなく，Erlang の JIT コンパイラーはすでにこの情報に依存して，可能な限り最適化を実行します(リンク先: Type-Based Optimizations in the JIT)．

また，Elixir は関数と演算子が暗黙的な型変換を回避するため，厳密に型指定されているとも言えます．次の関数は，入力がその型と一致しない場合にも失敗します:

$ binary() -> binary()
def debug(string), do: "we got: " <> string

$ (integer() -> integer()) and (float() -> float())
def increment(number), do: number + 1

<> は引数としてバイナリのみを受け入れ，それ以外の場合は例外を発生します．+は数値(整数または浮動小数点)のみを受け入れ，それ以外の場合は例外を発生します。 + は，次に示すように，文字列から数値へのような非数値型の暗黙的な変換を実行しません:

iex(1)> increment(1)
2
iex(2)> increment(13.0)
14.0
iex(3)> increment("foobar")
** (ArithmeticError) bad argument in arithmetic expression: "foobar" + 1

言い換えれば，Elixir のランタイムは実行時に値とその型を一貫してチェックします．数値以外の値が指定されたときにインクリメントが失敗する場合は，dynamic() 型が実行時の入力と一致しないときに失敗します．これにより，increment が宣言された型を返すことが保証されるため，型なしコードから関数を呼び出すときに実行時の型チェックを導入する必要がなくなります．

上記のidentity, debug, およびincrement関数を見ると，開発者として，これらの関数は入力と一致しない値が与えられたときに例外が発生するとみなせます．しかし，この特性を型システム自体によって計算されるように一般化するにはどうすればよいでしょうか？ これを行うために，集合論的な型に依存してこのプロパティを導き出す，strong arrowと呼ばれる新しい概念を導入します．

strong arrowの考え方は次のとおりです: strong arrowは，入力型(つまり，その定義域)以外の値で評価されるとエラーになることが静的に証明できるような関数です．たとえば，increment関数でstring()を引数として渡すと，string() + integer() は有効な演算ではないため，型チェックは行われません．集合論的型のおかげで，集合の否定を計算することで定義域外のすべての値を計算できます．increment/1 がnumber() 以外のすべての型で失敗することを考えると，この関数はstrongだと言えます．

このルールをすべての型付き関数に適用すると，どの関数がstrongでどの関数がそうではないかがわかります． 関数がstrongであれば，型システムは，dynamic() 型で呼び出すと常にその戻り値の型が評価されると認識します．したがって，increment(dynamic()) の戻り値の型はnumber() であると言えます．これは健全であり，それ以上の実行時チェックは必要ありません．

debug関数に戻ると，ガードされたidentity関数とともに使用すると，追加の実行時チェックを導入することなく，コンパイル時に警告を発し，実行時にエラーを発することができます:

$ a -> a when a: number()
def identity(arg) when is_number(arg), do: arg

def debug(arg) do
  "we got: " <> identity(arg)
end

ただし，identity関数がstrongでない場合は，前のセクションの戦略のいずれかにフォールバックする必要があります．

strong arrowのもう1つの強力な特性は，構成可能であることです．論文から例を取り上げてみましょう:

$ number(), number() -> number()
def subtract(a, b) do
  a + negate(b)
end

$ number() -> number()
def negate(int), do: -int

上の例では，negate/1 の型は，定義域の入力に対して発生するため，strong arrowです． + と私たちのnegateも両方ともstrong arrowであるため，subtract/2 の型もstrong arrowです．これは，dynamic() 型がシステム全体に広がる方法を制限するため，重要な能力です．

正誤表: 私のプレゼンテーションでは，上記の例で，number() の代わりに integer() 型を使用しました．しかし，それはスライドの間違いでした．integer() 型を指定すると，integer() -> integer() でsubtract関数を呼び出し，integer() -> integer() でnegate関数を呼び出しても，subtractはstrong arrowにはなりません． 理由を考えてみてください．

幸いなことに，他の段階的に型付けされた言語でも，strong arrowを利用できます．ただし，言語とその関数がpolymorphicであればあるほど，与えられた関数がstrongであると結論付ける可能性は低くなります．たとえば，Python や Ruby などの他の段階的に型付けされた言語では，+ 演算子は拡張可能であり，ユーザーは演算が有効なカスタム型を定義できます．TypeScript では，"foobar" + 1 も有効な操作であり，関数定義域を拡張します．どちらの場合も，演算子はnumber()以外のすべての型で失敗しないため，数値に制限されたincrement関数にはstrong arrow型はありません．したがって，健全性を維持するには，さらなる実行時チェックでオペランドを制限するか，dynamic() を返す(コンパイル時チェックの数を減らす)必要があります．

最後に考慮すべきシナリオが1つありますが，簡潔にするためにkeynoteでは含めませんでした．この関数を取り上げます:

$ integer() -> :ok
def receives_integer_and_returns_ok(_arg), do: :ok

上記の関数は任意の型を受け取り、:ok を返すことができます． この型はstrong arrowでしょうか？ 私たちの定義によれば，そうではありません． 入力を否定しても，型チェックは失敗せず，:ok を返すからです．

ただし，戻り値の型が常に同じであることを考えると，これはstrong arrowになるはずです．そのために，strong arrowの定義を修正して言い換えてみましょう．関数の定義域(つまり，入力)を否定し，それを型チェックします．関数が none() (つまり，型チェックは受け入れられない) またはそのs終域(訳註: codomain, 写像$f: X \arrow Y$の集合$Y$，これに対し，値域は$f(X)$を指すので注意)の部分集合である型 (つまり，その出力) を返す場合，それはstrong arrowです．

段階的な型付けと偽陽性による誤検知

これは，動的コードと静的コードをインターフェイスするときに考慮する必要がある最後のシナリオです．次のコードを想像してください:

def increment_and_remainder(numerator, denominator) do
  rem(numerator, increment(denominator))
end

$ (integer() -> integer()) and (float() -> float())
def increment(number), do: number + 1

increment_and_remainder/2 関数は型指定されていないため，両方の引数が dynamic() 型を受け取ります．次に，この関数は，分母(denominator)に 1 を加えて，分子(numerator)を割った時の余り(remainder, rem関数)を計算します．この例では，プログラム内での increment_and_remainder/2 の使用はすべて，引数として 2 つの整数を渡すと仮定しましょう．

定義によれば，increment/1 がstrong arrow型を持つ場合，increment(dynamic()) は integer() と float() の和集合 (これはnumber() とも呼ばれます) を返します．ここに問題があります．increment(dynamic()) が integer() と float()の和集合を返す場合，rem/2 は float を受け入れないため，上記のプログラムは型チェックは受け入れられません．

この問題に直面した場合，考えられる対応策は2つあります．

1. incrementがfloatを返す可能性があるため，関数が型チェックを受け入れないのは正しいことです．

2. 説明されているエラーはコードベースでは決して発生しないため，関数が型チェックを受け入れないのは正しくありません．

段階的集合論型のもう 1 つの興味深い特性は，dynamic() 型に上界(upper bound)を設定できることです．関数がnumber()を返す場合，呼び出し元はinteger()とfloat()の両方を処理する必要があることを意味します． ただし，関数がdynamic()とnumber()を返す場合，それは型が実行時に定義されていることを意味しますが，コンパイル時にそれがinteger()またはfloat()のいずれかであることを確認する必要があります．

したがって，実行時に型チェックを満たす型が1つ(integer())あるため，rem/2は2番目の引数がdynamic()およびnumber() 型を持つかどうかを型チェックします， 一方，dynamic() とnumber() で文字列連結演算子 (<>) を使用しようとすると，許容可能な実行時型がないため，依然として型指定違反が発生します．

strong arrowの話に戻ると，strong arrowからは2つの戻り型が考えられます:

1. strong arrowは，dynamic型とともに表示されると，その終域を返します．

2. strong arrowは、dynamic型とともに表示されると，終域と dynamic() 型の共通部分(intersection)を返します．

2番目の選択肢では，偽陽性による誤検知に対処することなく，既存のコードベースを静的型に徐々に移行できる可能性が開かれます．dynamicが存在することによる偽陽性の誤検知は，ノイズが多い，または静的型には問題を起こすので価値がないことを示していると見なされる場合があります．strong arrowと段階的な集合論タイプを使用すると，混合コードベースでのさまざまなトレードオフを検討できるようになります．上記2つの選択肢のうちどちらをデフォルトとして採用するか，またそれらをどのようにカスタマイズするかはまだ決定されていません．型システムを実験して統合するときのコミュニティからのフィードバックに依存します．

Dialyzer を使用する Erlang および Elixir の開発者は，これらのトレードオフに精通しているでしょう．2番目の選択肢は、偽陽性による誤検知がないDialyzerの動作を反映しているためです．ここでの違いは，セマンティクスが完全な型システムに統合されていることです．型シグネチャが存在しない場合は，dynamic()型が使用され，ここで説明する手法を利用して動的コードと静的コードをインターフェースします．関数に型シグネチャがあり，dynamic()型が存在しない場合，静的に型指定された引数を指定して呼び出された場合，その関数は静的に型指定されたコードとして動作します．静的型に移行すると，動的コードと静的コード間の対話ポイントが自然に減り，dynamic() 型への依存がなくなります．

まとめ

集合論的型を使用すると，和集合，積集合，否定の集合演算に基づいて多くの型指定機能を表現できます．

特に，私たちは，型システムが既存のコードベースとどのように統合されるか，また Erlang 仮想マシンのセマンティクスを最大限に活用できる方法に特別な注意を払いながら，Elixir の漸進的集合論的型システムを調査してきました．型システムは，(論文で説明されているように) パターンとガードに基づいて限定的な推論も実行します．これにより，strong arrowに加えて，コードを 1 行も変更することなく，静的型付けの利点の一部をコードベースにもたらすことが期待されます．

私たちの取り組みは正式に研究から開発に移行し，実装計画の概要を示しましたが，規模の大小を問わず，既存の Elixir コードベースにおける集合論型の使いやすさをまだ完全には実装しておらず，評価もしていません． 実装して検証すべきことはたくさんあり，振り出しに戻る可能性のある予期せぬ取引の破綻が見つかる可能性も否定できません． しかし，私たちはこれまでの新たな展開に満足しており，慎重ながらも興奮しています．

Elixir の型システムの開発は，Fresha (採用中!)，Starfish* (採用中!)，Dashbit によって後援されています．