HaskellのLinearTypes言語拡張について少し調べた

Posted on February 13, 2021 , Tags: Linear Haskell, Haskell, LinearTypes

最近リリースされた GHC 9.0.1 で使えるようになった LinearTypes 言語拡張について気になったので調べた。

LinearTypes言語拡張とは

GHC9.0.1から使えるようになった言語拡張で、Linear Typeを導入できる。ただ、上記リリースノートに “a first cut” とある通り、まだ実験的な機能としてリリースされた段階のようだ。
通常のGHCの言語拡張のように

とすることで使えるようになる

Linear Typeとは

そもそもLinear Typeとはどのような概念なのか、簡単に説明すると、「関数の引数がちょうど1度だけ評価される」、という条件を指定できるもののようだ。
理論的な基礎となるLinear type systemsについては前から広く知られていたものの、なかなか実装までは至らず、今回Haskellで晴れて実装までこぎつけたとのことだった。
具体例を挙げる。

としてコンパイルすると以下のようなエラーがでる

tuple1はコンパイル可能だが、tuple2は2箇所でエラーとなる。 エラー内容はそれぞれ

  • a はLinear Typeなのに2回評価されているのでエラー
  • b はLinear Typeなのに1回も評価されていないのでエラー

となる。「ただ1度だけ評価される」という制約を導入できる、という意味がなんとなくつかめただろうか。

LinearTypes言語拡張のproposalは こちら にある。
また、論文も こちら で公開されていたため、かいつまんで読んでみた。

Linear Typeが何の役に立つのか

論文によると、GHCにLinear Typeを導入するにあたって、下記2点にフォーカスして仕様策定すすめたそうだ。

  • 値の変更の安全性
  • 外部リソース(ファイルやネットワークなど)にアクセスする際の安全性

Linear Typeがこの2点にどのように対応できるのか、論文の例を挙げつつ見ていく。

値の変更の安全性

以下のようなArrayに関する変更を安全にすることを考える

上記 array という関数はarrayの長さを第1引数に、インデックスと値のタプルのリストを第2引数に受けとり、immutableなArrayを生成する。ここで unsafeFreeze は、freeze後の挙動については制約をかけることができず、状況によってはfreeze後にwriteされる可能性もあり得る。
これをLinear Typeを使って以下のように定義し直す。

ここで、 readwrite はLinear Typeになっているので1度しかMArrayを評価できない。ただ、返り値としてMArrayを返すので、論理的には新しい MArray ということになり、 readwrite をつなげて書くことができる。
freeze は引数を消費して、 Unrestricted (Array a) としてimmutableなArrayを返している。そのため、これ以上 MArray として readwrite ができない。 Unrestricted というのはLinear Typeの制限を受けない値として扱うことを意味する。つまり何度でも評価されるかもしれないし、1度も評価されないかもしれない。 Array 自体はimmutableなので Unrestricted でも安全、ということだろう。
この 「関数は引数を消費する。その後の関数でも続けて消費できる場合は論理的に新しい値として返す」 という流れがLinear Typeでの安全性保証の肝になっているようだ。

外部リソースアクセスの安全性

Linear Typeを使ったファイルアクセスについても見ておく。

readLineFileHandler を消費し、返り値として新しい FileHandler を返す。一方 closeFileFileHandler を消費し、新しい FileHandler は返さない。
通常のIOと異なり、 IO_L では返り値をLinear Typeで指定できる。これにより返り値の FileHandler をただ1度だけ消費する、という制限をかける。
上記により、close忘れやclose後の呼出を防ぐことができる。

後方互換性

論文によると、Linear Typeの設計として、multiplicity(linearかどうか)の型注釈がない場合はmultiplicityをmany(linearじゃない状態)にする、という設計にしたそうだ。これにより言語拡張を使ってもLinear Typeを明示的に指定しないところは通常のHaskellとして書ける。このように後方互換性を大事にしている旨が何度か言及されていた。

Rustとの比較

Linear Typeの挙動や目的について、Rustのmoveやborrowに似てるな、と思ったが、Rustのborrowについても論文内で言及があった。
論文によると、borrowシステムはその性質上、あるvが関数fによってborrowされていたら、fが処理を終えるまでvを保持しないといけない。そのため、tail-call eliminationができない。関数型言語ではtail-call eliminationは必須のため導入できないそうだ。
tail-call elimination(いわゆる末尾再帰最適化)ができないという制約があるとは知らなかったため、あとで調べてみようかと思う。

パフォーマンス

詳しくは読めていないが、Linear TypeによってUnboxed valueを使った最適化なども安全に行うことができ、性能向上にもつながった、というようなことが書いてあるようだ。

Future work

future workとしては以下のような内容があげられていた。

  • プログラム最適化
    • 最適なインライン化を行うためにカーディナリティの宣言にこのmultiplicityの型注釈を使うのはどうか、という話
  • multiplicitiesを拡張
    • 今回は引数をちょうど1度呼びだすかそれ以外か、という話だったが、もっと拡張はできる、という話
  • Streaming I/OやProgramming foreign heapsなどの実際の例への適用
    • 引数が評価される回数の制約がつけられるなら、引数が使いおわった時点で開放すればいいので、GCがいらなくなるためメモリ管理も容易になる

感想

引数の評価される回数を型で表現する、というのがなかなか興味深いなと思って調べはじめた。
調べてみると、Rustのmoveやborrowのようにリソースが使われている状態、もう使えなくなった状態をうまく扱うために設計されたものということが理解できた。
また、 こちら に言及されている通り、HaskellからWebAssemblyへのコンパイラを開発しているところでもあるので、WASMでGCどうするのか問題を解決する案としても意義があるのかなと思う。

参考