🍭

Haskell は Rust になれるのか？──2023年の Linear Haskell 体験記

2023/10/01に公開

Haskell

追記：いくらなんでもあまりにも長いので、配列演算に焦点を絞ってより「Rustっぽさ」の気持ちを強調した姉妹編を書きました。手っ取り早く雰囲気を掴みたい方はこちらもどうぞ。

TL;DR

GHC 9.0 から Haskell に入った線型型（Linear Types）の機能を一部割とガッツリ使ってみたので、Linear Haskell の現在の使い心地と将来の展望を報告するよ。
使おうと思えば使える段階にあるけれど、一部バグもあるし、まだ言語機能面で実装が追い付いていない部分もあって、快適に書けるようになるにはもうちょっと掛かるよ。それでも実用しようと思えばできるレベルにあるよ。
RustのようになるにはLinear Constraintsに期待。

更新履歴

2023/12/15 11:45 姉妹編へのリンク追加。
2023/10/01 12:30 線型性を納得してくれない場合の $\eta$ -展開や Unsafe 系関数の言及
2023/10/01 05:30 初版公開

Linear Haskell とは

みなさん、Haskell、してますか？している？それは結構！
ではみなさん、Linear Haskell、してますか？

している、という方は、すばらしい！是非知恵を貸してください。主に off-heap allocation まわりがもっと便利になるといいですよね。Linear Haskell における並列計算などもちょっと考えたいなという気分になっています。

していない、気になっているがしていない、そもそも Linear Haskell ってなんやねん、という方。ようこそ！この記事は主にそういった方々向けに Haskell における線型型がどんなもので、現状どんな感じで使えるのかというのを説明するものです^[1]。

というわけで、Linear Haskell の話です。

Linear Haskell というのはそういう名前の言語があるという訳ではなく、GHC 9.0 系から導入された LinearTypes 言語拡張、およびそれにより使えるようになる線型型を活かした新しい Haskell の書き方をふんわりと指します。

線型型（せんけいがた；Linear Types）というのは、Girard ^[2] が導入した線型論理というものに起源を持っていて──というとなんか難しそうですが、Rust の Ownership みたいなもんです。
これは嘘で、Rust で導入されているのはアファイン型と呼ばれるもの（の亜種）で、ある資源（メモリなど）が高々一回だけ消費されるという事実を型レベルで表現できるものです。
一方で、Haskellに入った線型型は資源がきっかり一回だけ消費されることを型レベルで保証するものです。Rustは一回も使わなくて良い が、Linear Haskellでは必ず一回使わなければいけない わけです。違いは回数の制限だけではなくて、利用回数の制約はRust では主に値の方が持っている^[3]のに対して、Haskell の線型型では関数型の矢印が持つようになっています。これは、既に確立した言語である Haskell に線型型を入れるに当っては、そちらの方が既存のエコシステムと共存させやすいから、というのが主たる理由です。

Linear Haskell の線型関数型は以下のように表されます：

f :: a %1-> b

普通の関数矢印 -> の代わりに %1-> を使います^[4]。これは普通の関数型に似ていますが、「式 f x がちょうど一回だけ消費された時、 x も必ずちょうど一回だけ消費される」という特別な条件を持つ関数で、コンパイラがこの条件が成り立つことを型検査時にチェックしてくれます。つまり、引数を何回つかうかによって複数の関数型がを導入するわけです。この、「引数を何回使うか」を重複度（multiplicity）と呼びます。GHCは現状「きっかり一回」を表す重複度 $1$ と、無制限を表す重複度 $\omega$ を扱うことができ、%1-> が重複度 $1$ の、旧来の -> が重複度 $\omega$ の関数型に対応します^[5]。

なるほどー、という場合はこれでいいんですが、「一回だけ消費する」っていうのはどういう意味なの？と気になるんじゃないかと思います。
厳密な定義は原論文に譲るとして、「消費する」というのは次のような意味です：

整数などのプリミティヴな値が「一回だけ消費」されるのは、値が評価されたとき。
関数が「一回だけ消費」されるのは、引数が一つ与えられ、その返値が「一回だけ消費」されたとき。
代数的データ型が「一回だけ消費」されるのは、コンストラクタに対するパターンマッチが行われて、その線型なフィールド^[6]がすべて「一回だけ消費」されたとき。

こういうのがあると何故うれしいのかというと、たとえば以下のようなことが実現できます：

メモリやファイルハンドルなどのリソースが必ず解放されることが保証できる^[7]。
配列や参照などの可変状態が「世界に一つ」しかないことが保証できる

これらのお陰で、以下のような機能が使えるようになります：

配列・参照などの破壊的変更を純粋に行える
- 純粋で効率的なハッシュテーブルの実装などもこれでできるようになる
- 自動的に指数的にリアロケートする growable な配列なども使える
配列の構築が融合変換（Fusion, rewrite ruels）の助けなしに効率的にできる
- 線型に束縛すれば、配列を構築する際の中間形式が外に漏れないのでアロケーションを一発しか行わないベクトルの変換がフュージョンに頼らなくてもできる
リソースの解放忘れなどを防げる
- 必ず一回消費しないと型エラーになるので、Handle の close や FFI のメモリの free などが強制できる
- より型安全な FFI などに使える
GCに管理されないメモリアロケーション・解放（off-heap allocation）
- 注意：これは、「Linear Haskell を使うとGCで管理されていないデータ型をアロケートする仕組みを創れる」ということであって、Linear Haskell を使うと値が GC の管理外に必ず置かれるという訳ではないです。今回主に扱う範囲の話は、ほぼすべてメモリは GC が管理するものになっています。

なにやらよさげですね。Linear Haskell でこれまでの Haskell で書けなかったプログラムが安全に書けるようになるわけです！
安全に、というところが大事ですね。安全でないインタフェースであれば、Linear Haskell でなくても書けますが「ちょうど一回だけ消費」の保証を型検査器がしてくれるお陰で安全になります。
もちろん、Linear Haskell は銀の弾丸ではないです。Linear Haskell に関してよくある誤解として、「Linear Haskell を使えば必ず速くなる」「Linear Haskell は高速化のための拡張」というものがあります。確かに、Linear Haskell によって、Haskell で安全に書くことができる最適化の種類はグンと増えます。ですが、もちろん使ったからといって無条件で速くなるわけではないです。要は、使い様ですね。

というところで、そろそろ Linear Haskell に興味が湧いてきたのではないでしょうか。湧いていない人は、今湧いたことに私がしたので、これから Linear Haskell を使ったプログラミングがどんなものなのか、その雰囲気を見ていきましょう。

といっても、今回私が主に使ってみたのは (1) のあたりで、沢山挙げた割には 2-4 はそんなに触れられていないので……このあたりの話を書くのは、画面の前の君だ^[8]！

2023 年の Linear Haskell の雰囲気

というところで、実際に Linear Haskell の雰囲気を見てみましょう。ここ数ヶ月ほど、いくつかの理由^[9]でCDCL（矛盾節学習）に基づくSATソルバをLinear Haskellで実装してみていたコードが以下にあるので、その経験を基に話していくことになります。

Linear Types を使って書いているのは、具体的には以下の二つのモジュールです：

現時点では合計2千行弱程度ですね。

また、現時点では Linear Haskell で実用的なプログラムを書くには Tweag の人達が開発している linear-base パッケージを使うことになりますが、これには Boxed な Vector しかないなど微妙に欲しいものが足りなかったりします。そこで、linear-baseに足りない機能を補うための補助ライブラリとして linear-extra も併せて開発してます：

こっちは似たような処理の重複もありますが、全部で1.8万行くらいあります。これら二つ併せれば2万行ちょい、まあ「Linear Haskell をがっつり使ってみた」と称するには十分かと思います。

補足：SATソルバとは？

本節ではCDCLの具体的な部分には踏み入らずに、SATソルバがなんなのかについては簡単に説明しておきます。
知っている人は「選言からなる節集合の連言として表された CNFのSATを解く」と思っといて貰えば大丈夫です。以下簡単に知らない人向けの説明です。

詳しい説明

SATソルバというのは Satisfiability（充足可能性）ソルバの頭文字を取ったものです。Satisfiability というのは、適当な論理体系を固定した時に、与えられた論理式を真とするような割り当てがあるのか？という意味です。一般の論理体系について考えることができますが、単に「SATソルバ」と言った場合古典命題論理の充足可能性判定問題のソルバを指すことが多いです。

命題論理というのは、命題変数から、かつ、または、ならば、否定を使って表現できる論理式だけを扱う論理体系です。述語記号や量化子が入っていない一番原始的な^[10]論理体系だと思ってもらえればよいです。「古典」というのは、排中律を仮定しているということで、これは「命題変数は True または False のどちらかが割り当てられる」という前提に立っていると思えば基本的に問題ないです^[11]。
つまり、「かつ（ $\land$ ）、または（ $\lor$ ）、ならば（ $\to$ ）、でない（ $\neg$ ）、で作られた論理式に現れる命題変数に True / False のどちらかを割り当てて、全体と真になるか？」というを判定するのがSATということになります。

今回解くのは、その中でもCNF（連言標準形）と呼ばれる形の論理式の充足可能性です。これは、「節」＝「命題変数の肯定か否定を〈または〉で繋いだもの」を「and」で更に繋いだものです。任意の古典命題論理式はあるCNFと同値になることは論理学の初歩です。
ここで、「命題変数の肯定か否定」をリテラル、「リテラルを〈または〉で繋いだもの」を節（clause）と呼びます。節を〈かつ〉で繋いだものが CNF という訳です。
こむづかしく聞こえるかもしれませんが、「リテラルは命題変数の否定または肯定の形をしており、節はリテラルの集合で、複数の節が与えられてそれらを同時に充足したい」ということだけ押さえていれば大丈夫です。

Linear Haskell はじめの一歩 - 純粋な可変配列を例に

それでは早速一つめの例です。CDCLソルバでは節ごとに、最大二つの監視リテラルが割り当てられており、これを使って高速に真偽値の伝播を行っています。
以下は、節を表す型 Clause と、全ての節を格納する線型なベクトル Clauses 型の定義の簡略化版です^[12]：

{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
import Data.Vector.Mutable.Linear qualified as LV
import Prelude.Linear

type ClauseId = Int
type Index = Int
type Clause = LV.Vector Clause
data Clause = Clause
  { watched1, watched2 :: {-# UNPACK #-} !Index
  , literals :: {-# UNPACK #-} ![Lit]
  }
  deriving (Show, Eq, Ord, Generic)

data WatchVar = W1 | W2 deriving (Show, Eq, Ord, Generic)

このとき、指定した節の監視リテラルを切り替える関数 setWatchVar は次のように書けます^[13]：

setWatchVar :: ClauseId -> WatchVar -> Index -> Clauses %1-> Clauses
{-# INLINE setWatchVar #-}
setWatchVar cid W1 vid clauses =
  LV.get cid clauses & \(Ur c, clauses) ->
    LV.set cid c { watched1 = vid } clauses
setWatchVar cid W2 vid clauses = {- W1 と同様 -}

なんだか見慣れない構築子 Ur と、とつぜんよくわからない (&) 演算子が出てきてますね。一つずつ見ていきましょう。

魔法の箱 `Ur` と線型性の呪い

ここで、LV.set および LV.get の型は次のようになっています：

set :: Int -> a -> Vector a %1 -> Vector a
get :: Int -> Vector a %1 -> (Ur a, Vector a)

set の型はそれっぽい感じですね。set n a v は v の n 番目の要素を a にセットする関数です。これは副作用を伴う破壊的変更で、旧来であれば ST モナドや IO モナドに包まれている必要があるところです。しかし、ここでは純粋関数になっています。どうしてこれが可能なのでしょうか？
それは、Vector a を作成する関数の型をあわせて見てみるとわかります：

empty :: (Vector a %1 -> Ur b) %1 -> Ur b
constant :: Int -> a -> (Vector a %1 -> Ur b) %1 -> Ur b
fromList :: [a] -> (Vector a %1 -> Ur b) %1 -> Ur b

linear-base が提供する Vector の初期化関数はこれらだけです。注目すべきは、アロケートされた Vector a が全て %1-> の左辺に現れているため必ず線型に消費する必要があることです^[14]。
このことと、set と get 以外の他の書き込み・読み込みの関数いずれも Vector a は必ず線型に消費する定式化になっています。
これにより、Vector aの実体は常に一つしか存在しないことが保証されるため、set によって破壊的変更をしてもその影響が外に漏れることがなく、また、続きの計算では返ってきた Vector a を使って計算が続行できる、という訳です。

set はよいですね。get も概ねよさそうですが、返値が Ur で包まれています。もっと言えば、 empty やら fromList やらも返値は Ur を期待しています。いったいこれはなんでしょうか？

Ur は Unrestricted の略で、「しまった値を何回でも複製して取り出せるようにする」という魔法の箱です^[15]。魔法の箱、と書きましたが、コンパイラで特別扱いされている訳ではなく、Ur は唯一のフィールドは 非線型フィールドを持つデータ型として定義されています。関数として見たときに、Ur :: a -> Ur a という型になっているデータ型だと思えばとりあえず問題ないです。
具体的な定義は後ほどするので、今は「そんなもんか」と思っておいてください。

Ur は第1引数を非線型に消費するので、線型に束縛した値をそのまま渡すことは不可能です。なので、次のように可変状態を外に持ち出そうとすると……

leakMutable :: [a] %1-> Ur (LV.Vector a)
leakMutable xs = LV.fromList xs (\vec -> Ur vec)

vec の部分に次のようなエラーが出て怒られる訳です：

• Couldn't match type ‘'Many’ with ‘'One’
    arising from multiplicity of ‘vec’

可変ベクトルである LV.Vector を線型な文脈の外に持ち出して更に set などで変更されると困るので、fromList などの最終的な結果を Ur で包まれたものに限定して漏れ出るのを防いでいるという訳です。

これを踏まえて、set と get の型をもう一度見てみましょう：

set :: Int -> a -> Vector a %1 -> Vector a
get :: Int -> Vector a %1 -> (Ur a, Vector a)

ここで set が a を非線型に消費することと、get が a を Ur に包んでいることは対応しています。
配列の中の値は何度も読み出して使いたいだろう、という気持ちがあるので、get は Ur a を返します。ここで、Vector などの他の可変状態を含み得る set できるとそこから情報が漏れ得るので、 set も a を非線型に消費するようにしているのです。

`(&)` やラムダ抽象の利用 - `let` と `where`, `if` の利用制限

さきほどの定義に戻ってみましょう：

setWatchVar cid W1 vid clauses =
  LV.get cid clauses & \(Ur c, clauses) ->
    LV.set cid c { watched1 = vid } clauses

set と get はそれぞれ配列を線型に消費する書き読み関数で、get の返値が包まれている Ur は結果を何度も引き回せるようにするための「魔法の箱」でした。
ところで、通常の Haskell に慣れている人であれば、これは次のように書けるんじゃないかと思うでしょう：

setWatchVar cid W1 vid clauses =
  let (Ur c, clauses') = LV.get cid clauses
   in LV.set cid c { watched1 = vid } clauses'

しかし、これは次のように「clauses の線型性が破れているよ」怒られてコンパイルできません：

• Couldn't match type ‘'Many’ with ‘'One’
    arising from multiplicity of ‘clauses’

これは、現状のGHCは let-式や where-節で定義されている値の右辺は非線型に消費されると見做されるからです。
なぜかというと、GHCに実装されている多重度の推論機構が let/where に対応していないためです。
なので、上の例では let の左辺で定義されている clauses' の多重度がいちばん間違いの少ない非線型束縛されていると見做され、エラーになっているのです。
これは、let が複数の局所定義間の相互再帰を許したり、最適化時に式の内部へとfloatしたりするという複雑性に起因して、まだそこを考慮するまで実装が追い付いていないためだと私は理解しています。

一方で、普通の $\lambda$ -式や case 式についは GHC がある程度ちゃんと多重度を推論・検査してくれます。
なので、最初の実装では、Prelude.Linear で提供されている普通の (Data.Function.&) の線型版：

(&) :: a %1-> (a %1-> b) %1-> b

とλ抽象を使って

  LV.get cid clauses & \(Ur c, clauses) ->
    LV.set cid c { watched1 = vid } clauses

のように書いた訳です。また、Linear Haskellだからといって全ての let-式が使えなくなる訳ではないです。
束縛した値が非線型に用いられるので良い場合、次のように問題なく let 式を使うことができます：

getWatched1 :: ClauseId -> Clauses %1-> (Ur Lit, Clauses)
getWatched1 cid clauses =
  LV.get cid clauses & \(Ur Clause{literals, watched1}, clauses) ->
    let l = literals !! watched1 -- literals も l も共に線型に束縛・消費されるので問題なし
     in (Ur l, clauses)

また、右辺が線型束縛された変数を含まないのであれば、ちゃんと適切な型註釈を書いてやれば let や where 内で線型関数型を持つような関数定義をすることもできます。

別の構文上の制限として、これは単純に人手が足りないからか、if-式でも同様の対応が必要になる場合があります。特に、if の条件式中に線型束縛変数は登場できません。
そこで人工的な例ですが、正の値かどうかを「無駄に if-式を使って」確かめる次の関数を考えます：

positive :: Int -> Bool
positive n = if n <= 0 then False else True

ただし、(<=) :: Int %1-> Int %1-> Bool は Prelude.Linear で定義されている、通常の (<=) の線型版です。
ここで、positive の型を Int %1-> Bool に変更すると「nが非線型に消費されているよ！」とエラーが出てしまいます。
これを回避するには、(&) と case式とを使って次のようにすればOKです：

positive :: Int %1-> Bool
positive n = (n <= 0) & \case 
  True -> False
  False -> True

これらは普通の Haskell の書き方からは乖離しやや不自然ですが、それでもこれである程度読み書きはできるので、これで妥協する、というのが現在の Linear Haskell の実践方法になります。悲しいですが、まあ、慣れれば問題なく読み書きできるので、今は我慢しましょう。

こうした制限は、GHCが個別の変数の多重度の註釈を与える構文をサポートしたり、多重度推論のアルゴリズムが強化されればやがて改善することが期待されます。

Shadowing について

Haskellの慣習に染まっている（私のような）人の場合、これまでの例では clauses の変数名が衝突して shadowing が起きているのが気持ち悪い、バグの温床だ！と思うかもしれません。
たしかに、今回の場合は clauses の再束縛は一回だけなので、& 以降の二つめの clauses は clauses' としてもいいでしょう。
しかし、2023 年の Linear Haskell を前提としたAPIの設計では^[16]、set や get など可変状態を扱う関数は、配列を解放したり複製可能な値にして Ur に包んで返すような最終消費者以外は、常にその可変状態をきっかり一回消費し、返された新しい変数に対して続きの操作をする必要があります。
たとえば、めちゃくちゃ人工的な例ですが、「配列の最初の3つの要素だけ二倍にする」みたいな操作を書こうと思うと、

doubleInit3 :: Vector Int %1-> Vector Int
doubleInit3 vec = 
  get 0 vec & \(Ur i, vec') ->
    set 0 (i * 2) vec' & \vec'' ->
      get 1 vec'' & \(Ur j, vec''') ->
        set 1 (j * 2) vec''' & \vec'''' ->
          get 2 vec'''' & \(Ur k, vec''''') ->
            set 2 (k * 2) vec'''''

この例の場合は modify_ 関数を使えばチェインは三つで済みますし、インデックスごとに値を二倍する関数を書いて3回ループしてやればまだなんとかなります。
それでも非自明な操作を連続的に行うたびに新しい名前を考えるのはつらいし、変数名がややこしくなりそう、というのはわかると思います。
なぜ Haskell では一般に shadowing が忌み嫌われているのかといえば、名前の衝突によるバグを見逃がさないためであり、衝突して過去の値を参照できなくなるのを防ぐためです。
一方で、Lienar Haskell を使う場合では、いちど線型に束縛・消費された変数はそもそも再利用できないですから、線型束縛変数に限っていえば shadowing が起きても何も問題がない訳です。心理的にも、本来同じ筈だが線型性の要請によって再束縛が起きているような変数名は一貫させたいところですし、下手に名前を変えたために過去のもう使えない変数を呼んでしまい、意図せず重複度検査に引っ掛かる、という事態も防げます。

なので、私が Linear Haskell を書く場合は、なるべく Lienar Haskell 流に書くモジュールとそうでないものを分離した上で、Linear Haskell を多用するモジュールでは -Wno-name-shadowing オプションを有効化して、積極的に線型変数の名前をshadowingしています。

`Ur` の正体 - 線型および非線型フィールド

ふう。配列の更新をするだけで、なんか長々と書いてしまいましたね。説明をもう少し先に進めましょう。「値を非線型に取り出せる魔法の箱 Ur」というのが出て来ました。これは非線型フィールドの性質によるものという話でしたが、具体的にどのように定義されているのでしょう？
ということでUrの定義を見てみましょう：

{-# LANGUAGE LinearTypes, GADTs #-}

data Ur a where Ur :: a -> Ur a

型 Ur a は唯一の構築子 Ur :: a -> Ur a を持つ型として定義されており、そのの唯一のフィールドは非線型なフィールドとして宣言されていることになります。
どういうことか？冒頭で書いた、「一回だけ消費」の代数的データ型の部分を思い出しましょう：

代数的データ型が「一回だけ消費」されるのは、コンストラクタに対するパターンマッチが行われて、その線型なフィールドがすべて「一回だけ消費」されたとき。

ここでは Ur の第1引数は GADTs の構文を使って非線型な関数 -> の左辺として登場しているので、Ur は非線型なフィールドとみなされるわけです。
なので、Ur を「一回だけ消費」するにあたっては、単純に Ur データ構築子に対してパターンマッチさえすれば、内側の値を何回使おうが、あるいは全く使わなかろうが型検査器は文句を言わないというわけです。
では、次のように定義してはいけないのでしょうか？

data Ur a = Ur a

結論から言うと、これはだめです。何故かというと、GADTs構文ではない通常の代数的データ型コンストラクタのフィールドはデフォルトでは線型フィールドとして解釈されるためです。
これは、旧来の Haskell のエコシステムと Linear Haskell とでデータ型を可能な限り使い回すためです。
仮に、デフォルトで通常のフィールドが非線型と解釈されたとしましょう。リスト型について考えてみます：

data [a] = [] | a : [a]

ここで、ただ一つの要素からなるリストを構築する関数の Linear 版、 singleton :: a %1-> [a] について考えてみましょう。
プレーンな代数的データ型のフィールドがデフォルトで線型な場合、つまりは (:) :: a %1-> [a] %1-> [a] の場合は次のように素直に書くことができます：

singleton :: a %1-> [a]
singleton a = a : []

しかし、もしデフォルトで非線型だった場合、つまり (:) :: a -> [a] -> [a] の場合、次のようなエラーが出てしまいます：

Multiplicity coercions are currently not supported

GHCのバージョンによっては多重度が合わなかった場合、定義全体がエラーになってしまいますが、ここでは本質的には (:) の第一引数の a が非線型に消費されることになっているのが原因です。
これを避けるには、GHCの現状のようにデフォルトで線型だと解釈するか、さもなくばリストの非線型版を定義する必要があります。
後者の方針を取ると、線型性で怒られるたびにあらゆるデータ型を別々に定義する必要が出て来てしまい、現実的ではありません。なので、GHC ではデフォルトではフィールドは線型だと解釈するようにしている訳です。

逆に通常の Haskell で困ることはないのでしょうか？つまり、通常の非線型な Haskell の世界でフィールドの線型性が悪さをすることはないのでしょうか？非線型な世界で、線型フィールドから値を一回しか取り出せなくなってしまうように思えます。

結論からいうと、そんなことはありません。なぜかというと、線型フィールドの値の利用回数が問題になるのは、そのデータ型自体が線型に束縛されているときだけだからです。線型関数型が出て来ない非線型な文脈では、あらゆる値は非線型に束縛されています。なので、Linear Haskell ではない通常のHaskellでは線型フィールドから値を何度取り出そうと、取り出さなかろうと何も問題はないのです。

ちなみに、線型フィールドと非線型フィールドを共に持つようなデータ型も GADT 構文を使って定義できます：

data Foo where
  MkFoo :: Int -> LV.Vector Int %1-> Foo

この場合、最初の Int 型のフィールドは非線型、次の LV.Vector Int 型のフィールドは線型になります。
ですから、Foo の値を線型に消費する必要がある場合は、 Vector の値は「きっかり一回」消費する必要がありますが、Int の値については、ちゃんと MkFoo に対するパターンマッチさえしていれば、何もせずに捨てようが何回も使い回したりしようが構いません。

また、上では GADTs と普通の data 宣言を扱いましたが。では newtype はどうか？というと、newtype は GADT sytnax を使っても線型フィールドとしてしか定義できません。

値を消費したり複製したり無限に増やしたりしたい！ - Consumable, Dupable, Movable の階層

これまで、Linear Haskell でのプログラムの書き方について見てきました。なんかエキゾチックには見えるが、文法の面ではまあ概ね問題なさそうです。

これまで fromList などの例で見たように、Linear Haskell では可変性を局所化するために「線型束縛された値を使った計算結果を外に持ち出すには Ur に包まなくてはいけない」という API を採用しています。
これによって Data.Vector.Mutable.Linear で定義されている可変ベクトル Vector a の値は外に直接持ち出せない訳です。しかし、変更は今後しないが配列は参照したい、という場合があるでしょう。こうした場合には、Vector.Mutable.Linear の freeze 関数が使えます：

freeze :: Vector a %1 -> Ur (Vector a)

可変ベクトルが Ur に包まれて漏れているように見えて一瞬ギョッとしますが、左辺は Data.Vector.Mutable.Linear で定義されている可変ベクトル、 右辺は vector パッケージの Data.Vector で定義されている不変ベクトル です。
このように、 linear-base で定義されている純粋なコンテナ型は、外部に持ち出せる不変版への（多くの場合 $O(1)$ の）変換関数を提供していることが常です。

こうした特化された freeze 関数を使う以外に、線型束縛された値を外部に持ち出す方法はないのでしょうか？たとえば、ユニット型 () であったり、即値の数値型 Int や Bool、それらをフィールドにもつデータ型などは何回も作り直すことで外に持ち出せそうです。
これを実現するのが Movable 型クラスです：

class Dupable a => Movable a where
  move :: a %1-> Ur a

上で述べた、Int や Double, Bool などの基本型はインスタンスが用意されています。また、線型版の Genericallyを使えば、Movable のみから再帰的に定義されるようなデータ型に対して Movable を導出することができます。

Movable は、linear-base が提供する値の複製・消費ををサポートする型クラス階層の最上位に位置しています。階層を全て転載すると次のようになります：

class Consumable a where
  consume :: a %1-> ()

class Consumable a => Dupable a where
  dup2 :: a %1-> (a, a)

class Dupable a => Movable a where
  move :: a %1-> Ur a

Consumable はその名の通り 一回消費できる型のクラスで、Rust でいうところの Drop に対応します。
「一回消費」というのは最低限でも冒頭の定義を満たしている必要がありますが、たとえばハンドルであれば close であったり、メモリであれば free であったり、追加的なファイナライザを呼んでもよく、このあたりはライブラリ設計者が意図した型の意味論に依存します。
返値が () なのは、() が消費可能なデータ型の中で最も簡単な型だからですね。単純にデータ構築子としての () に対してパターンマッチしてやればいい。
Consumable に関連する関数で大事なのは、次のlseq関数です：

lseq :: Consumable a => a %1-> b %1-> b

これは、型から推測できる通り、第一引数を consume して第二引数を返すという関数で、だいたい seq のようなものです。
ただし、Linear な文脈にいるので、 a を捨てるのには consume する必要がある、という訳です。

Dupable 型クラスは、複製可能な型のクラスで、Rust でいうところの Copy や Clone に対応します。
dup2 がその気持ちを表していて、値を一個消費するかわりに二つ複製したものを返す、という気持ちになっていますね^[17]。

Movable は先に説明した通りですね。線型文脈から外に持ち出して無限回複製できるようにできる型のクラスです。可変状態を内部に持つ Vector などは、Movableのインスタンスを持たないことが重要です。
ただ、Movableインスタンスがある場合、ConsumableとDupableの導出を効率的に導出することができます。こうした場合、Movable インスタンスさえ書けばあとは自動的によい感じのインスタンスを導出してくれるのが、AsMovable newtypeで、DerivingVia を使うことが想定されています。

Linear Haskell は Linear Haskell だけで完結するものではなく、外の世界と値をやりとりしてはじめて実用できます。そうした時には、Ur や Consumable, Dupable そして Movable を空気のように駆使することが重要になります。

Linear Haskell を使った大規模なプログラムの実際・2023年版

さて、一個の配列の取り回しだけでなんかずいぶんと長々と説明ができてしまいました。Linear HaskellはHaskellの中に築かれた新たなパラダイムの言語の観があり、また現状の実装の都合上からも奇異なみためのコードになりがちなため、初見の人を想定して書くとどうしてもこれくらい長くなりますね。

さて、一個でこれだけ大変でしたが、一般に実際のコードに現れる線型な資源は一つとは限りません。たとえば、前述のCDCLソルバでは CDCLState という巨大な内部状態を引き回しています。
本当は必要な情報は足りないんですが、せいいっぱい簡略化すると次のようになります：

import qualified Generics.Linear as L
import Generics.Linear.TH (deriveGeneric)


type WatchMap = LA.Array IntSet
type Valuation = LUA.UArray Variable

data CDCLState where
  CDCLState ::
    -- | Number of original clauses
    !Int %1 ->
    -- | Level-wise maximum steps
    !(LUV.Vector Step) %1 ->
    -- | Clauses
    !(LV.Vector Clause) %1 ->
    -- | Watches
    !WatchMap %1 ->
    -- | Valuations
    !Valuation %1 ->
    -- | Unsatisfied Clauses
    !(LSet.Set ClauseId) %1 ->
    CDCLState

deriveGeneric ''CDCLState
deriving
  via L.Generically CDCLState
  instance Consumable CDCLState s

-- | ソルバのメインロジック
solveState :: CDCLState %1 -> Ur (SatResult (Model VarId))

それぞれの説明はしませんが、まー沢山の Linear Field から成っているのがわかると思います。solveState 関数は、こうした初期の内部状態を受け取って、最終的な充足可能性判定をするメインロジックです。
これらを取り回すにあたっては以下のことをちゃんとやる必要があります：

それぞれ型の違う線型資源を適切に初期化する
ロジックの中で必要な内部状態だけを取り出し・更新する
内部状態から必要な内部状態だけを取り出して Ur に包み、残りは消費する

3 については……まあ、やるだけなので良いでしょう。1 と 2 をちゃんとやるにはコツが要ります。
ネタバレをすると、何年か待つとかなり楽になりそうなんですが、現時点ではやろうと思えばできる、という感じです。順に見ていきましょう。

複数資源初期化の問題──線型性トークンによる当面の回避策

さて、上で見たように現実のプログラムでは複数の線型資源を同時に割り当てる必要があります。
とりあえず、こんな関数があればよいわけです：

withCDCLState :: CNF VarId -> (CDCLState %1-> Ur b) %1-> Ur b

こんな実装になるでしょうか：

withCDCLState :: CNF VarId -> (CDCLState %1-> Ur b) %1-> Ur b
withCDCLState rawClauses f =
  LUV.fromList [0] $ \steps ->
    LV.fromList (map toClause rawClauses) $ \clauses ->
      LA.fromList (buildWatchMap rawClauses) $ \watchMap ->
        LUA.alloc (numVariables rawClauses) Indefinite $ \vals ->
          LSet.fromList [0.. numClauses rawClauses - 1] $ \unsats ->
            f (CDCLState 0 steps clauses watchMap vals unsats)

numClauses :: CNF VarId -> Int
toClause :: CNF VarId -> Clause
buildWatchMap :: CNF VarId -> [IntSet]
numVariables :: CNF VarId -> Int

前節で説明したように、fromList や alloc などは初期化用のタネ（基になるリストや長さなど）をとり、目標の資源を線型束縛する関数に渡す継続渡しの形を取るのでした：

LV.fromList :: [a] -> (LV.Vector a %1-> Ur b) %1-> Ur b
LA.fromList :: [a] -> (LA.Array a %1-> Ur b) %1-> Ur b -- Array は長さ決め打ち、Vector は growable
-- linear-base で提供されている、線型可変ハッシュセット
LSet.fromList :: Hashable a => [a] -> (LSet.Set a %1-> Ur b) %1-> Ur b 

-- Linear Mutable Vector / Array の Unbxoed 版；linear-base にないので自前実装
LUV.fromList :: U.Unbox a => [a] -> (LUV.Vector a %1-> Ur b) %1-> Ur b
LUA.alloc :: U.Unbox a => Int -> a -> (LUA.UArray a %1-> Ur b) %1-> Ur b

これらを使えば、次のようにしてソルバを呼び出して解かせることができます：

solve :: CNF VarId -> SatResult (Model VarId)
solve cnf = case withCDCLState cnf solveState of
  Ur ans -> ans

ここまでは、ちょっと混み入っていますがまあ問題なさそうです。
そこで、ちょっとした改善を考えてみましょう。
上では命題変数の取る範囲は VarId に決め打ちになっていますが、一般の型を命題変数としてもてる論理式も解きたいな、と思ったとします。
つまり CNF Intとか CNF ArithmeticExpr とかも解けるようにしたいという訳です。
これには、もともとの命題変数の型と VarId との間の二つのマップを作ってやればよさそうです。折角なので、linear-base が提供する可変 HashMap の実装を使っちゃいましょう：

HashMap も例によって継続渡しの初期化関数を提供しています：

-- linear base 初期化関数：
LHM.empty :: Hashable k => Int -> (HashMap k v %1 -> Ur b) %1 -> Ur b
LHM.fromList :: Hashable k => [(k, v)] -> (HashMap k v %1 -> Ur b) %1 -> Ur b

ではこれを使ってみましょう。元の変数から VarId への辞書 toVarId と、逆向きの辞書 fromVarId を作りましょう：

-- 名前の変換などをする便利関数群
buildDics :: 
  CNF v -> 
  HashMap v VarId %1-> 
  HashMap VarId v %1-> 
  (HashMap v VarId, HashMap VarId v)
renameCNF :: HashMap v VarId %1 -> CNF v -> (Ur (CNF VarId), HashMap v VarId)
unrenameModel :: HashMap VarId v %1-> Model VarId -> Ur (Model a)

-- 一般の命題変数の Solve
solveRenamed :: CNF v -> SatResult (Model v)
solveRenamed cnf =
  LHM.empty 256 $ \fromVarId ->  -- v -> VarId
    LHM.empty 256 $ \toVarId ->    -- VarId -> v
      buildDics cnf toVarId fromVarId & \(fromVarId, toVarId) ->
        renameCNF toVarId cnf & \(Ur cnf, toVarId) ->
          withCDCLState cnf $ \state ->
            unrenameModel fromVarId (solveState state)

おおむねよさそうです。ただ、 toVarId はいちど CNF をリネームしたら不要になるので、もっとはやく解放したいですね。
もっといえば、toVarId をアロケートしている二つめの LHM.empty の継続をもっと早く抜けておくと、すぐ toVarId が解放されてよさそうな気がしますね。試してみましょう。

solveRenamed :: CNF v -> SatResult (Model v)
solveRenamed cnf =
  LHM.empty 256 $ \fromVarId ->  -- v -> VarId
    LHM.empty 256 (\toVarId ->    -- VarId -> v
      buildDics cnf toVarId fromVarId & \(fromVarId, toVarId) ->
        renameCNF toVarId cnf & \(Ur cnf, toVarId) ->
          toVarId `lseq` (Ur cnf, fromVarId)
    ) & \(Ur cnf, fromVarId) ->
        withCDCLState cnf $ \state ->
          unrenameModel fromVarId (solveState state)

しかし、これは型検査を通りません！なぜなら、LHM.empty の返値はリークを防ぐために全体が Ur で包まれている必要があるからです。
では Ur に全部包むとどうか、つまり Ur (cnf, fromVarId) としたらどうか、という話になりますが、cnf は非線型に束縛されているのに対し、toVarIdは線型に束縛されているので直接 Ur に放り込めません。
じゃあ fromVarId に move が使えないか……と思うかもしれませんが、これもまた不可能です。なぜなら、toVarId は可変状態を含む HashMap 型を持っており、これが外に漏れないように Movable のインスタンスは定義されていないし、してはいけないからです。

なので、継続渡しと Urをベースとした割り当て関数しかない場合、複数の線型資源を割り当てようとすると、最初の例のように全ての継続を最後の値まで持っていく必要があるのです。これは Sticky End of Scopesと呼ばれ、Linear Haskellが導入された最初から議論されてきた課題でした。

どうにか解決できないでしょうか？要約すれば、これは継続渡しがベースで最後の返値があるていど決め打ちになるために起きる問題です。
それなら、継続渡しではなく即値で資源を返してくれる割り当て関数があればよさそうです。しかし、無条件に返してしまうとせっかく set や get で線型性を強制しても、元となる資源が何度も外から参照できてしまいます。こんな感じに：

-- こんなのがあったとする
unsafeFromList :: [a] -> Vector a

foo = 
  let vec = unsafeFromList [0]
      vec2 = set 0 42 vec
   in get 0 vec & \(Ur i, vec) ->
        get 0 vec2 & \(Ur j, vec2) ->
          vec `lseq` vec2 `lseq` (i == j) -- ???

なぜこれができてしまったのかというと、無制限（非線型）にヤバい資源を導入できてしまったからでした。
継続渡しをやめつつ、線型に資源を導入するにはどうすればいいか？難しい問題に見えますが、じつは取れる手段は一つしかありません。
そもそも、線型な資源は線型関数型の左辺または右辺に現れることによってしか導入されません。ならば、線型にしか導入できないことが既にわかっている別の資源を証拠 として、それと組にして新たな線型資源を割り当てるようにするのはどうでしょうか？
たとえば、Vector は線型にしか導入できないので、次のような関数があればよさそうです：

fromListBesides :: [a] -> Vector b %1-> (Vector a, Vector b)

ここでは Vector b の具体的な値は問題ではありません。重要なのは、Vector b が線型にしか導入できないことを根拠として、その線型性を引き継いで新たに Vector a を安全にアロケートするための証拠になっているということです。
どういうことか？Vector b は fromList などをつかって線型に導入するか、既にある Vector を証拠にして Besides でアロケートするか、どちらかによって導入されています。
これを元まで辿っていけば、いつかは線型矢印 %1-> の左辺に現れた「始祖」の Vector に辿り着くでしょう。この始祖は線型に消費される必要があるので、型検査に一度通れば、そこから fromListBesides の線型矢印を手繰って降りていった先にある Vector b, Vector a も必ずちょうど一回だけ消費されることが保証されます。

これで一応の問題は解決しました。しかし問題は、こうした「線型性の証拠」の組み合わせごとに besides を定義していったのでは、あっという間に組み合わせ爆発が起き、お姉さんは機械の身体になってしまうということです。

vectorBesidesVector :: [a] -> Vector b %1-> (Vector a, Vector b)
vectorBesidesMap :: [a] -> HashMap k v %1-> (Vector a, HashMap k v)
mapBesidesVector :: [(k, v)] -> Vector a %1-> (HashMap k v, Vector a)
...

これはしんどいですね。しかし、「既にある線型性の証拠を使う」というアイデアは良さそうです。
ならばいっそのこと、「継続渡し形式でしか導入できない、線型性の証拠専用の型」を用意すればどうでしょう？
つまり、次のような型とインタフェースを用意するのです：

data Linearly

instance Consumable Linearly
instance Dupable Linearly -- MUST NOT BE MOVABLE!

linearly :: (Linearly %1-> Ur a) %1-> Ur a

fromListL :: [a] -> Linearly %1-> Vector a
allocL :: Int -> a -> Linearly %1-> Array a
emptyHML :: Int -> Linearly %1-> HashMap k v

ポイントは、

Linearly は linearly で %1-> の左辺値としてしか導入できなくなっている
線型文脈下では任意有限個の資源を割り当てられるように、Dupable のインスタンスにする
外に漏れると困るので、Movable には 絶対にしない。

これだけだと原始的なので、次のような補助的な関数・型クラスを用意しましょう：

class HasLinearWitness a where
  linearWitness :: a %1-> (a, Linearly)

instance HasLinearWitness Linearly

besides :: 
  HasLinearWitness a => 
  a %1-> (Linearly %1-> b) %1-> (b, a)

これこそが、正に linear-base の Issue で議論されていた（途中）解決策でした。
Linearly ベースのアロケーション API が提供を使えば、これまでの例は次のように継続渡しではない形で書くことができます：

toCDCLState :: CNF VarId -> Linearly %1-> CDCLState
toCDCLState rawClauses l =
  besides l (LUV.fromListL [0]) & \(steps, l) ->
    besides l (LV.fromListL (map toClause rawClauses)) & \(clauses, l) ->
      besieds l (LA.fromListL (buildWatchMap rawClauses)) & \(watchMap, l) ->
        besides l (LUA.allocL (numVariables rawClauses) Indefinite) & \(vals, l) ->
          LSet.fromListL [0.. numClauses rawClauses - 1] l & \unsats ->
            CDCLState 0 steps clauses watchMap vals unsats

solveRenamed :: CNF v -> SatResult (Model v)
solveRenamed cnf = linearly $ \l ->
  besides l (LHM.emptyL 256) & \(fromVarId, l) ->  -- v -> VarId
    besieds l (LHM.empty 256) & \toVarId ->        -- VarId -> v
      buildDics cnf toVarId fromVarId & \(fromVarId, toVarId) ->
        renameCNF toVarId cnf & \(Ur cnf, toVarId) ->
          toVarId `lseq`
            unrenameModel fromVarId (solveState (toCDCLState cnf))

これは一見最初の solveRenamed に戻っているように見えるかもしれません。
しかし、最初はすべて $ で継続をとっていたのが & で束縛されているだけになっています。
前述の制約によって以下の分は今の GHC でコンパイルは通りませんが、以下のように let を使って書き直してみると一目瞭然でしょう：

solveRenamed :: CNF v -> SatResult (Model v)
solveRenamed cnf = linearly $ \l ->
  let (fromVarId, l) = besides l (LHM.emptyL 256) in
  let toVarId = besieds l (LHM.empty 256) in
  let (fromVarId, toVarId) = buildDics cnf toVarId fromVarId in
  let (Ur cnf, toVarId) = renameCNF toVarId cnf
   in toVarId `lseq` unrenameModel fromVarId (solveState (toCDCLState cnf))

継続はもう最初の linearly にしかなく、残りは逐次的に適用し解放できています。これはかなり綺麗になったのではないでしょうか。

なぜ linear-base には Linearly がないのか

Linearly を使った解決策は、それを複製して引き回す必要があるという点を除けばけっこうよいです。しかし、linear-base にはこの機能はありません。
なぜかというと、上で「途中解決策」と書いたように、後述する Linear Constraints が GHCに実装されれば、より良い解決策が実現できるからです。

とはいえ、Linear Constraints がいつ GHC に入るかは外部の我々にはよくわかりません。Linearly トークンによって線型性を証拠づけるのは現時点では最良の解決策といえますし、できれば使いたいところ……という訳で、私の linear-extra には上のインタフェースが存在しています^[18]。

まだ Hackage にはリリースしてないんですけど、2023 年の Linear Haskell を実用する上では結構必須だと思うので、GitHub repo に依存するなり、コードをコピペするなりして使ってやってください。そのうちリリースします。

Linear State Monad で線型状態を引き回す

さて、これで巨大な線型資源の塊がアロケートできました。あとはこれに対して純粋に変更を加えていけばよいです。
問題は、多くの線型な演算子（配列の読み書きなど）は、線型資源を取って計算結果（もしあれば）と元の線型資源を返すことです。
たとえば、get や set の型を思い出してみましょう：

get :: Int -> Vector a %1-> (Ur a, Vector a)
set :: Int -> a -> Vector a %1-> Vector a

最終結果を取り出すまで、このように状態全体やその一部の結果をスレッディングして引き回しつづける必要があります。
状態のスレッディング……というと、思い付くのはもちろん、State モナドですね！

ただ、我々がよく知る State モナドは次のようなものでしたが……

newtype State s a = State { runState :: s -> (a, s) }

今回我々が必要なのは、この線型版です：

newtype State s a = State { runState :: s %1-> (a, s) }

これも期待通り Monad になりますが……普通のモナドではなく線型モナドになります。線型モナドは、その名の通りLinear Haskellにおけるモナドです。しかし……ここでおしらせなのですが、実は Linear Haskell では Functor の階層は制御関手とデータ関手に分裂します！この呼び名は linear-base が採用している呼び分けで、詳しくは Tweag の次のブログポストで説明されています。

ここでいっている線型モナドは、結論からいうと制御関手としての構造を持つ方です。
どういうことか？Linear Arrow の（実用的な）付けかたを考えると、次の二通りの Functorがあります：

-- Defined in Control.Functor.Linear
class Data.Functor.Linear.Functor f => Functor f where
  f :: (a %1-> b) %1-> f a %1 -> f b

-- Defined in Data.Functor.Linear
class Functor f where
  f :: (a %1-> b) -> f a %1 -> f b

違いはどこかというと、それは渡された fmap 前の関数の重複度です。
「データ関手」はデータ構造としての関手で、リストや Maybe などが該当します。リストや Maybe は要素が一つとは限らず、全く無かったり任意有限個だったりします。これらを全部マップするには、渡された元々の関数は非線型に消費できる必要があります。

一方で、制御関手は制御構造としての関手です。これに該当するのはさきほどの線型 State モナドや、線型な Reader、Stream などが該当します。

Functor と Monad の間に位置する Applicative もデータ版と制御版があり、それぞれ多重度が違います。
しかし、モナドは制御関手としてのものしか用意されていません。これは、データ構造としてのモナドは考えることはできても、実質値を取り出せなくて意味がないからです。
詳細な議論は Tweag の元記事を参照してください。

いずれにせよ、線型な世界には線型な世界の State モナドがあり、これが線型な世界のモナドになっていることがわかりました。
この線型モナドは以下のようなメンバ関数を持ちます：

-- Defined in Control.Functor.Linear
(>>=) :: Monad m => m a %1 -> (a %1 -> m b) %1 -> m b 
(>>) :: Monad m => m () %1 -> m a %1 -> m a
return :: Monad m => a %1 -> m a
join :: Monad m => m (m a) %1 -> m a

では、この State モナドを使ってコードを書けば、これまでの State モナドを使うのと同じように状態を引き回して書けそうです。
しかし、注意すべき点があります。それは、当然のことながら、線型な Monad はbase の Monad とは違う型クラスだという事です。
そもそも型が違います。なので、生の do 式を使うことはできません。

しかし、GHC 9 から導入された QualifiedDo 言語拡張を使うと、Control.Functor.Linear で定義された >>= や >>, return などを使って do 式を再解釈してくれます。こんな具合に。

{-# LANGUAGE QualifiedDo #-}
import qualified Control.Functor.Linear as C
import qualified Data.Vector as V

unrenameModel ::
  (Hashable a) =>
  Model VarId ->
  C.State (LHM.HashMap VarId a) (Ur (Model a))
unrenameModel (Model pos neg) = C.do
  Ur !positive <- renameLits pos
  Ur !negative <- renameLits neg
  C.pure $ Ur Model {..}

renameLits ::
  (Hashable a) =>
  V.Vector VarId ->
  C.State (LHM.HashMap VarId a) (Ur (V.Vector a))

unrenameModel の定義の C.do の部分に注目してください。これ頭の C. を取るとただの do 式になります。QualifiedDo 言語拡張を有効にすると、do キーワードを他の関数やシンボルなどのようにモジュール名で qualify することで、do 式は当該モジュールで定義された関数を使って脱糖されるようになります。ポイントは、型検査は脱糖の後に行われることです。Control.Functor.Linear では、例えば (>>) :: m () %1-> m b -> m b という型が与えられています。これは第一引数が m ()に決め打ちされているという意味で元々のふつうの (>>)、つまり do の束縛なしのセミコロンよりも型が厳しくなっています。これは、矢印が線形であり第一引数の値を捨てる必要があるためです。Consumableに一般化してもいい気がしますが、まあそれは自分で判断して呼んでください、ということなのでしょう。いずれにせよ、線型モナドに対してQualifiedDoを使ってdo内で束縛を伴わない文を書いた場合、その返り値は任意の値ではなく m () になるようにする必要がある、という点には注意してください。

線型モナドが普通のモナドでないことの悲しみは、他の既存のライブラリと直接相互運用できないことです。考えてみれば当たり前で、既存の大半のライブラリは普通のモナドを前提に設計されています。
こうした用途には、UrT変換子を使うと解決できます。
UrT の定義は次の通りです：

newtype UrT m a = UrT (m (Ur a))

基本的な考え方としては、線型モナドは値が複製できないためにふつうのモナドでなくなっているから、その返値を Ur で包ませればふつうのモナドにできるだろう、ということです。
たとえば、上で型だけ書いた renameLits は次のように書くことができます：

renameLits ::
  (Hashable a) =>
  V.Vector VarId ->
  C.State (LHM.HashMap VarId a) (Ur (V.Vector a))
renameLits =
  runUrT
    . traverse
      ( \v ->
          UrT $ C.state $ BiL.first (D.fmap fromJust) . LHM.lookup v
      )

ここで、V.Vector は base の Traversable ですが、linear-base の Traversable（というのもあります）ではありません。なので、UrT を噛ませて Linear Monad をふつうのモナドにしてtraverse に食わせ、最後 runUrT をすることで値を引き戻しているわけです。

こうすると結構な数の外部ライブラリとの協業の途が開けますが、パフォーマンスの点から一点気になるのは Ur の分かならず間接参照が挟まることです。Ur のフィールドは非線型にしないといけないので、newtype は使えないのでした。GHC の最適化機構が頑張ってくれればある程度消えてくれるかもしれませんが、大規模な計算だとちょっと不安なところです。また、モナドの返値が線型に束縛されていてかつ Movable でない場合この UrT を使ったトリックは使えなかったりするので、その場合は地道にグルーコードを書くしかないでしょう。不変な値からなる可変コンテナだけ扱っている場合はほとんど問題ないとは思いますが。

また、Linear な State モナドも、一層のモナドとして使う分には既存のGHCと同じくらい綺麗に最適化で消えてくれますが、複数の線型 StateT 変換子を重ねるとそれなりに速度低下が見られました。
このへんはある程度考えたりプロファイルをとったりしながら実装をしていくべきでしょう。

Linear Optics (Lens)

これで概ねLinear Haskell で大規模な内部状態を扱うのは大丈夫です。一方、いちいち state 関数を呼んでフィールドを書き換えたり、線型関数をスレッディングするのはちょっと手がかかります。こうした時、ふつうの Haskell であれば、lens や zoom、(.=), (%=)、uses などを使って楽をしたいところです。linear-base では、lensに対応する Lienar Optics が提供されており、通常の lensと同じように使うことができます。ただ、現行の linear-base には線型関数型の線型 Functor インスタンスが欠けているので、optics を使おうと思うと自分で定義を追加する必要があります。これはあんまりなので、私の方で Pull Request を作成していて、既に master にマージしていただいているので、次のリリースを待つか、GitHub の linear-base に依存するようにするといいでしょう。

あとは Optics と State の橋渡しですが、これは MonadState のような型クラスがまだ定式化されていない（これはできないのではなく、純粋に人手が足りなくて手が回っていないんだと思う）ので、linear-base にはありません。私が実装しているCDCLソルバでは、結局トップレベルが State または StateT になっているので、それ決め打ちで、こんな類似関数を定義して使っています：

zoom ::
  (Functor m) =>
  Optics.Optic_ (Kleisli (Compose ((,) t) (FUN 'One t))) s s t t ->
  StateT t m a %1 ->
  StateT s m a

(%=) ::
  (Applicative m) =>
  Optics.Optic_ (Kleisli (Compose ((,) t) (FUN 'One t'))) s s t t' ->
  (t %1 -> t') %1 ->
  StateT s m ()

uses ::
  (Applicative m) =>
  Optics.Optic_ (Kleisli (Compose ((,) t) (FUN 'One t))) s s t t ->
  (t %1 -> (a, t)) %1 ->
  StateT s m a
{-# INLINE uses #-}

あとは Lens を定義できればよい。これは、lensなどと同様に、レンズ定義用の関数 lens を使えばできる。こんな感じに：

watchesL :: LinLens.Lens' (CDCLState s) WatchMap
watchesL = LinLens.lens \(CDCLState numOrig ss cs ws vs vids) ->
  (ws, \ws -> CDCLState numOrig ss cs ws vs vids)

これらを使った State の書き方はこんな感じ：

setSatisfied :: ClauseId -> C.State CDCLState ()
{-# INLINE setSatisfied #-}
setSatisfied i = C.do
  Ur lvl <- currentDecideLevel
  setSatisfiedLevel i lvl
  unsatisfiedsL C.%= LSet.delete i

その他のチップス

これまでで扱えなかった、しかし Linear Haskell を書く上で知っとくと便利なバッドノウハウの類いをここにまとめておきます。
Linear Haskell がメジャーになって、GHC が十分かしこくなればこの悲しみは減ると思われるので、みなさんどんどん使って要望を出し、Linear Haskell の輝かしい将来を招来しましょう。

書いている途中で一時的に変数が使われなくなったため、重複度エラーにかき消されて他の型検査の結果がわからない！

GHC のバージョンによっては、重複度のエラーが起きている関数定義全体を範囲として報告するので、どの変数が何の理由でエラーになっているのかわかりづらいことがあります。
重複度検査が行われるのが他の型検査の前だからか、こうなってしまうと HLS で部分式をポイントして型を表示する、というようなデバッグ手段が使えず悲しいことになります。

こういう場合は、とりあえずどっかで問題になっている線型変数を undefined に食わせとくといいです。

どこで重複度エラーが起きているのかわからない！

仕方がないので、こういう時にあよくある間違いを列挙しておきます：

線型変数を二度呼んでいる
- これはがんばって探すしかない。後に説明する方法がよいでしょう。
if の条件式に線型変数がいる／MultiwayIf を使っている
- 理論的な障害はないが、取り敢えず当面上手くうごかないので場当たり的にやる
- とにかくあらゆる条件分岐を case 式で置き換える
let 右辺で線型変数を束縛している
- & とλ抽象ないし Lambda Case で対処
- 線型変数にかんするループを回す場合などは、線型変数を受け取るヘルパ線型関数を型註釈つきで let や where 内で定義すればいい

1 の場合を見付けるには、一旦関数定義をコメントアウトするなどして、本体を「undefined に線型変数をぜんぶ食わせる」で置き換える。
その後、式を徐々に大きくしていって、破ってるところを見付けましょう。

線型なコンテナに対する畳み込みがつらい

Vector や Array は中身については非線型なので、実は工夫するとfoldlパッケージの枠組みに載せることができます。
ポイントは、purely や impurely を使うようにすることで、たとえば次のような関数はハックなしに実装でき、これを purely に食わせれば無事畳み込みができる：

foldArray :: U.Unbox a => (x -> a -> x) -> x -> (x -> b) -> Vector a %1 -> (Ur b, Vector a)

頭の体操に書いてみてください。素直にループを回せばよいだけ。

（普通の `vector` パッケージの）Vector を簡単につくりたい

一回つくってあとは参照するだけ、みたいな Vector を作りたい場合は、linear-base のPolarised Array を使うと楽かつ効率がよいです。Polarised Array は配列を確保するための抽象化で、Push/Pull という二種類の配列を経由することで、cons / snoc / filter などを経つつ、メモリアロケーションは最終的に一回だけしか行わない、ということを実現します。
同様のことは、それこそ vector パッケージのフュージョンを使えば実現できますが、最適化オプションの効き方によっては思ったような効果が出ない場合があります。一方、Polarised Array でを使えば、提供される関数を使っているかぎりアロケーションは一回しか行われないことが保証されます。

Push と Pull は次のような特徴があります：

Push: いつでも実際のメモリに書き出せる状態の配列。単純に値を push したり append したりして配列を作る場合、 $O(1)$ でできる。
Pull: 関数表現されたストリーム。zip や filter など高階関数を使ってストリームが変形できる。

ただ、Pull のインタフェースはちょっとあまり使われていないようで、ドキュメントの vecfilter の例がコンパイルできなかったりします。
とはいえ、Push Array だけでも十分便利に使えます。Push Array はデフォルトでは Boxed Vector にしか書き出せないですが、Monoid を経由する形になっているので自分で Destination Passing Style のアロケータを書けば任意の配列に書き出せます。手前味噌ですが、以下は linear-extra で任意の Vector に書き出せる版の alloc を実装したものです：

謹製のCDCLソルバでは、節集合を Linear Unboxed Vector として初期化する前段階として、元になる Unboxed (Immutable) Vectorを生成するのに Push Array を使っています。

例外安全性について

Lienar Haskell では必ず資源の解放を保証できる、と書きましたが、先に宣言した通りこれは嘘です。Linear Arrow の制約はあくまで「結果がちょうど一回消費されたとき、引数もちょうど一回消費される」でした。つまり、結果が完全に消費されなかった場合引数が消費されるかは保証の限りではありません。つまり、途中で 例外が発生したときはリソースが解放されない場合が有り得ます。

こうした場合は、bracket を使って必ず最後にリソースを解放する RIOモナド（rioパッケージのものとは違います）や、Off-heap allocation 用の Pool などを使うことになります。
ただ、現状の RIO は解放処理の種類がデフォルトでは一つしか対応していなかったり、Pool は単純な双方向リストとして実装されているのでスレッドセーフでないなど、常用していく上では色々機能を追加する必要があります。

線型な関数と非線型の間の変換

現状の GHC はまだ型の上では重複度多相性をある程度サポートしていますが、推論機構が未成熟なこともありライブラリレベルではまだサポートが進んでいません。
特に「線型な関数を非線型な関数を受け取る関数に渡す」というのは、受け取る関数が重複度について多相になっていない限り、ちゃんと渡せません。

以下の例を考えます

mapNonLinear :: (a -> b) -> [a] -> [b]
mapLinear :: (a %1-> b) -> [a] %1-> [b]
succNonLinear :: Int -> Int
succLinear :: Int %1-> Int

のような関数があり、 succ* を map* に渡したかったとします。すると、以下の組み合わせは型が合わなくて怒られます。

mapNonLinear succLinear
mapLinear succNonLinear

1 では 「線型な関数」を「非線型な関数」と見做して渡そうとしていますが、この変換は単純に関数の制約を忘れるだけ安全な筈です。これをする方法は二つあります：

a. succNonLinear を $\eta$ -展開する： mapNonLinear (\x -> succLinear x)
b. Prelude.Linear.forget を使って線型性を忘れる： mapNonLinear (forget succLinear)

2 では逆に 「非線型な関数」を「線型な関数」と見做して渡そうとしていますが、これは 本質的に危険な操作です。
とはいえ、実用上「これはぜったいに線型であることがわかっているのに……」とか、「線型じゃないけど今回実装する用途では線型と思えば十分なのに……」という場合があります。Linear Haskell を使った API を設計する場合などによくでくわすと思います。こうした場合は、この利用は本当に安全なんだという責任を自分ひとりで負う覚悟をした上で、 linear-base の Unsafe.Linearモジュールで提供されている toLinear 関数を Unsafe とqualify した上で使います。

import qualified Unsafe.Linear as Unsafe

safeActually = mapLinear (Unsafe.toLinear succNonLinear)

繰り返しになりますが、これは完全に自己責任です。鼻から悪魔が出てもよいという気持ちで使うか、ちゃんと正当性を証明し（たつもりになっ）て使いましょう。
二つ以上、三つ以上の引数を取る場合は toLinear2 などが使えます。toLinear* の実態はただの関数の引数の数を保存するように特殊化された unsafeCoerce# です。単純に全ての引数を線型と見做すわけではなく、入力についても出力についても各引数の重複度について多相性がある形になっているので、一部について線型だが残りは非線型、みたいな関数にキャストしたりその線型性を付けかえたりする用途にも使えます。いずれ unsafe な操作なので、こちらは覚悟の上で使いましょう。

2023年の Linear Haskell の課題とその未来

というわけで、2023年時点での Linear Haskell の書き味について見てきました。コツを掴めばそれなりに実用できるところまできていますが、まだ痒いところには手が届かない、といったところでしょう。

そういえば、本記事のタイトルは「Haskell は Rust になれるのか？」でした。この問に対する答えを現時点でまとめるのであれば──「まだ、Rust ではない」でしょう。
純粋にあったら便利な機能がまだまだ欠けている部分があったりします。まあ、この辺は自分で補えばいいですね。私はそろそろ Off-heap allocation をしたくなってきて、そうすると可変状態に対する参照カウントポインタや Weak pointer が欲しくなってくるので、私はいま @qnighy さんの「Rust の Arc を読む」シリーズと首っぴきになっています。さらに、今の用途では必要ないですが、せっかくなのでスレッドセーフなカウンタや Arc も実装したくなり、あれ、そうすると、Linear Haskellでピュアなデータ並列をする枠組みが必要じゃん、あれ、Pool これスレッドセーフじゃないじゃん、とてんやわやです。とはいえ、こうした不足は人々が Linear Haskell を使っていってライブラリが充実してくれば解決するでしょう。

ライブラリ機能面ではそれでいいとしましょう。言語機能面ではどうでしょうか？

これまでに見てきた例では、以下のような課題がありました：

複数の線型資源を同時に割り当てるとき、Linearly のようなトークンを引き回す必要がある
関数が線型資源を（形式上）都度消費するため、いちいち引き回す必要がある
線型 State モナドなどを外部ライブラリと組み合わせるには UrTなどで包んでやる必要があるが、Ur のコストが心配

実は……ここでの課題は "Linear Constraints" （又の名を Linearly Qualified Types）機能が GHC に実装されれば一挙に解決します！
……というのはいいすぎで、三つめの UrT については一般的には廃止はできません。State 以外にも線型モナドはあって、RIO や線型版の IO モナドなどは本質的に必要で、外部ライブラリとの協業には究極的には UrT が必要になるでしょう。ここで解決するのは、値を引き回すのに State モナドが必要で UrT が要る、みたいな状況です。

Linear Constraints はいったいなんでしょうか？名前から推察できる通り、線型に消費できる型制約です。

前の節で見た Linearly の例は Linear 制約として以下のように再定式化できます：

linearly :: (Linearly %1=> Ur a) %1-> Ur a

fromList :: Linearly %1=> [a] -> Vector a
empty :: Linearly %1=> Vector a

Linearly の右にある矢印が %1-> ではなく二重矢印 %1=> になっていること、つまり制約に関する矢印であることに注意しましょう。
これにより、次のようにほとんど意識せずに複数の線型資源をつくれるようになります：

toCDCLState :: Linearly %1=> CNF VarId -> CDCLState
toCDCLState rawClauses =
  let steps = LUV.fromListL [0]
      clauses = LV.fromListL (map toClause rawClauses)
      watchMap = LA.fromListL (buildWatchMap rawClauses)
      vals = LUA.allocL (numVariables rawClauses) Indefinite
      unsats = LSet.fromListL [0.. numClauses rawClauses - 1]
   in CDCLState 0 steps clauses watchMap vals unsats

solveRenamed :: CNF v -> SatResult (Model v)
solveRenamed cnf = linearly $ 
  let fromVarId = LHM.empty 256 in
      toVarId = LHM.empty 256 in
      (fromVarId, toVarId) = buildDics cnf toVarId fromVarId in
      (Ur cnf, toVarId) = renameCNF toVarId cnf
   in toVarId `lseq` unrenameModel fromVarId (solveState (toCDCLState cnf))

この裏では、コンパイラが一定の規則に基づいて linearly によって導入された Linearly 制約を適切に複製したり要らなくなったものを捨てたりして、ちゃんと意味が通るようにしてくれています。
ただ、これではまだ buildDics などに渡す HashMap が引き回されています。これは Linear Constraints と RankNTypes と存在型を組み合わせることで解決できます：

data c ∧ t where
  □ :: c => t -> c ∧ t

class Read n
class Write n
type RW n = (Read n, Write n)

fromList :: Linearly %1=> [a] -> ∃ n. (RW n ∧ Vector a n)
get :: Read n %1=> Int -> Vector a n -> (Read n ∧ Ur a)
set :: RW n %1=> Int -> a -> Vector a n -> (RW n ∧ Ur a)

ここで、 $\exists s.\ \mathop{C}[s] \land \mathop{T}[s]$ は未来の GHC がサポートする構文で、型制約 $C[s]$ を満たすなんらかの型変数 $s$ について $T[s]$ の形の型を持つ値をパックしたものです。
これは Dependent Haskell の推進者で Linear Types にも関与しているRichard Eisenberg らの論文に基づくものです。

これに対してパタンマッチをすることで、ちょうど runST のうちがわで RankNTypes による Skolem 変数がするような役割を果す型変数 n と RW n 制約も文脈に導入されます。
というか、ここでは自然に書くために存在型をつかいましたが、存在型がなくてもRankNTypes と継続渡し形式を組み合わせればほぼ同様のことは実現できます。

fromList :: Linearly %1=> [a] -> (forall n. RW n %1=> Vector a n -> Ur b) %1-> Ur b

どちらの場合でも、Vector （や HashMap）は非線型に束縛されているのがポイントです。ですので、solveRenamed の例で満たように内側の継続の中に外側のリソースが囚われる Sticky End of Scopes の問題は発生しません。

話を戻しましょう。存在型ベースの get/set のAPIが使えた場合、一番最初の setWatchVar は次のように書き換えることができます：

setWatchVar :: RW n %=> ClauseId -> WatchVar -> Index -> Clauses n -> (RW n ∧ Clauses n)
setWatchVar cid W1 vid clauses =
  let □(Ur c) = get cid clauses
   in □(set cid c { watched1 = vid } clauses)

clausesの再束縛が消滅しているのに注意してください。余計なコンストラクタ □ に対するマッチなどが必要になっていますが、かなり読み易くなっています。
□がやや邪魔ですが、原論文ではEisenbergらの論文の提案手法を使えばある程度コンパイラに推論させることができるだろうことが示唆されています。

また、これを発展させることで、Rustにおける所有権の貸与のようなことができます。
たとえば、以下のような感じで配列を途中で分割し、それを別々に貸し出す、といったようなことができます：

class Slices n l r

split :: 
  RW n %1=> 
  Vector a n -> Int ->
  ∃ l r. (RW l, RW r, Slices n l r) ∧ Ur (Vector a l, Vector a r)
join :: 
  (Slices n l r, RW l, RW r) %1=> 
  Vector a l -> Vector a r ->
  RW n ∧ Ur (Vector a n)

原論文では、これを使って「Haskell ではできない」とされていた「純粋な in-place quicksort」の実装が紹介されていてかっこいいですね。
Linear Haskell で純粋なデータ並列が実現できれば、これと組み合わせて並列なフーリエ変換を純粋に書けるようになるのではないかと考えています。

また、似たような形で、配列の要素一つだけ可変参照として貸し出すことができます：

lendMut :: 
  RW n %1=> 
  Array a n -> Int -> 
  (forall p. RW p %1=> Ref a p → (RW p ∧ r)) %1->
  (RW n ∧ r)

ここで大事なのは、lendMut が存在型ではなく RankNTypesを使っていることです。
これは、外側で消費されている RW n と内側で提供されている RW p が同時に使えると困るからです。まさにこれは Rust のborrow checker が検査していることですね。
数年前、Linear Haskell の話をしたときに @qnighy さんに「時分割はできるのか？」という質問がありました。

このときに、私はたしか RankNTypes を使った解決案を提案しました：

Linear Constraints による解決策は、まさにこれを発展させた形になっています^[19]。

いずれにせよ、ここまでくるとかなり Rust に近いといえるのではないでしょうか。
という訳で結論。2023年のHaskellはまだ Rust ではないが、近い将来 Rust になれる可能性が大きいということでひとつ。

残念ながら、Linear Constraints を実用するには存在型を上手くあつかう必要があったりと準備が必要なようで、具体的にいつごろ実装される予定なのかは外部の我々にはわかりません。しかし、Tweag はかなり Linear Haskell に本気なようなので、そのうち入る──と期待したいところです。そのためにも、Linear Haskell を今のうちからバンバン使って利用例を積み上げて、Linear Haskell 進化させる需要あるよ！という既成事実をつくっていきたいところですね。やっていきましょう。

あとがきにかえて参考文献

以下、あとがきにかえてLinear Haskell を使うにあたって参考になる文献を紹介します。

ライブラリ

まずは実用上の話ということで、ライブラリから。

linear-base

Tweag製のLinear Haskell を使ったプログラミングを実践する上で必要な base 相当の機能を提供するパッケージ。こいつがないと始まらない。
Optics (Lens), Array, Vector (resizable な array), Polarised Vector (fusion), HashTable, Streaming, Region (RIO), Off-heap allocation など実用上のツールは一通り揃っている
手前味噌ですが、これに足りないなあと思った機能（主に Unboxed や Storable な配列・ベクトル回り）を後から拡張したライブラリをつくってます（まだ全然安定してないのでHackage にリリースはしていない）：

linear-generics

GHC の通常の Generics の、Linear Haskell対応版。linear-base などでも、Consumable, Dupable, Movable などを自動導出するのに用いられています。
自前のデータ型をこれらに対応させるなら使うとかなり楽になります。

text-builder-linear

Bodigrim製。内部で線型型を使うことで、かなり効率的な実装を実現した Strict な Text ビルダ。
バッファを確保しておいて足りなくなったら倍々に拡張していく、他の言語では「よくある」実装。
バッファを直接弄るAPIと、普通のビルダのように継続渡し変換して線型型を使わないAPIがある
- 前者の方が速いが、後者でも十分に速い模様

SPJ の講演

Linear Haskell には SPJ も噛んでいて、とてもわかりやすい講演があります：

Tweag のブログポスト

Linear Haskell は Tweag を主体に開発が進められており、Linear Types 関連のブログポスト群は使い方の雰囲気やお気持ちを知るのにめちゃくちゃ参考になります。

上記から幾つか（ほとんど全部だけど）参考になる例を紹介しましょう。

2023年のLinear Haskell関連：こんにちの Linear Haskell を使ってみるにあたって参考になる記事。
- linear-base の紹介記事。簡単な概要などがまとめられている。
- Destination Passing-style: Linear Haskell を使うと、ピュアかつ自然に Destination-Passing Style が実現できて、フュージョンに頼らずに配列の効率的な初期化ができるよ、という話。
- Tale of Two Functors: 線型型を意識すると、Functor や Monad が複数種類あることに気をつけなくてはならず、なんで？という話。
FFI 関連：FFIで他言語のライブラリを呼び出す時のメモリマネジメントって大変ですけど、Linear Types で頑張りましょうという記事。
未来の Linear Haskell 関連：まだ GHC に入っていない Linear Constraints があると、こんなに便利！という記事。2023年の Linear Haskell に直接はやくにはたちませんが、Token ベースで妥協する参考になったりはする。

原論文

やっぱり最後に参考になるのは原論文です。とはいっても、論文の記法や定式化がぜんぶ GHCにそのまま実装されているわけではないです。
それでも、ここで紹介しきれなかった応用例の紹介もありますし、これからの Linear Haskell の未来を知る上でかなり参考になるので、これらを眺めて夢を広げつつ、自らの手で切り拓いていきましょう！

Retrofitting Linear Types は見た感じ "Linear Haskell" Paper の草稿という感じですね。

"Linearly Qualified Types" 論文は草稿の名前が "Lienar Constraints" で途中から今の題名に変更になったようなので、以前のタイトルで記憶している人も多いでしょう（僕もそうでした）。Rust と化した未来の Linear Haskell の姿がそこにはあります。

Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2017. Linear Haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2, POPL, Article 5 (January 2018), 29 pages. Preprint: arXiv:1710.09756.
Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg. 2022. Linearly qualified types: generic inference for capabilities and uniqueness. Proc. ACM Program. Lang. 6, ICFP, Article 95 (August 2022), 28 pages. Preprint: arXiv:2103.06127.
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2017. Retrofitting Linear Types. 2017. In submission.

といったところで。それではみなさま、Happy Linear Haskelling!

脚注

Rust は線型型ではなくアファイン型だろ、Haskell の記事なのに Rustをタイトルに入れるな、という方──すんません。 ↩︎
Jean-Yves Girard。著名な論理学者。Type: Type を帰結に持つ型システムが、論理体系として矛盾することを示した Girard のパラドックスでも知られています。ところで、Haskell は最初から undefined の存在のために矛盾しているので、GHC の型システムは Type :: Type を公理として採用することで型推論・検査を簡略化する途を取っています。 ↩︎
より厳密に言うのなら、各値が住んでいる型の種（カインド）にとて線型性を区別していると見做せる（はず）です。 ↩︎
線型論理を知っている人向けに書けば、これはぺろぺろキャンディー矢印 $f\colon a \multimap b$ と同じことで、実際 UnicodeSyntax 言語拡張を使えば同じ記号を使って f :: a ⊸ bと書けます。これに近づけるためか、Linear Haskell の原論文や初期のプロトタイプ実装では、a -o b という構文が用いられていました。 ↩︎
これらは厳密には完全に別個の型という訳ではなく、一般の重複度つき関数型を表す FUN m a b カインドの m が One ( $1$ )なのか Many（ $\omega$ ）なのかで区別されています。現在はこの m に関する多相性を GHC は部分的にしかサポートしていないですが、将来のGHCでは ($) や (.) なども多相的になるかもしれません。 ↩︎
後述するように、LienarTypes 拡張の下では、代数的データ型のフィールドは、線型なものと非線型なものが宣言できます。互換性のために、LinearTypes拡張なしで宣言されたフィールドは全てデフォルトで線型なものと解釈されます。 ↩︎
後述する通り、例外を考えるとこれは厳密には嘘になります。が、bracket patternみたいなのを使うことでケアできます。 ↩︎
おねがいしま〜す ↩︎
ghc-typelits-presburger がちゃんと等号と複合項を扱えるようにしたいなどの思惑から、最終的に Haskell で効率的な SMT を書くつもりになっており、GHC 9.0 以降で動けばいい訳だしこの際 Linear Haskell 使ってみるか、となったのでした。 ↩︎
といっても、最小論理だったり更に使う記号を制限した断片を考えたり、部分構造論理を考えたりするとより「原始的」なものはまだまだあるんですが、あんまり煩いことはいわないことにします。 ↩︎
よくある誤解として、「古典論理は True/False の二値論理、直観主義論理は True/False/どちらでもないの三値論理」という言説があります。これは誤りで、何らかの意味で整合性のある三値論理を考えると、Gödel–Dummett 論理というものと厳密に対応しています。これは、直観主義論理に公理図式 $(P \to Q) \vee (Q \to P)$ を付け加えたもので、直観論理より真に強く、古典論理より真に弱い中間論理の例になっています。 ↩︎
実際の実装では、Clause は Unboxed な部分とそうでない部分とに分かれており、literals も（Lienar ではない）Unboxed Vectorに格納しています。 ↩︎
実はこれは、modify_ 関数を使えば一行で
```
LV.modify_ (\c -> c { watched1 = vid }) cid clauses
```
と書けちゃいます。説明の都合上、ここでは get と set を連続的に呼び出す形にしています。 ↩︎
線型な利用を強制するために継続渡し形式になっています。これは任意個のリソースを作成しようと思ったときにちょっと不便です。これを緩和する方法は後ほど述べます。 ↩︎
線型論理を知っている人向けに書けば、Ur a は指数結合子 $!a$ に相当します。 ↩︎
将来的にはどうにかなりそうという含みがあるって？はい。後述する Linear Constraintsですね。 ↩︎
実際には、dup2 に加えて、Dupable の効率的なインスタンスをジェネリックに導出する際に使われる dupR メンバ関数もあり、インスタンスは dup2 か dupR の少なくとも一方を実装すればよいというようになっています：
```
dupR :: a %1-> Replicator a
```
↩︎
これちゃんとやるの結構たいへんで、{-# NOINLINE #-} だけでなく noinline 魔術を使う必要があったり、中身がない Linearly 型が GHC の最適化により無から湧き出してこないようにするのに苦労しました。未だになんでこれで上手くいってるのかよくわかってないので、誰かわかったらおしえてください。 ↩︎
今見返すと、runOnce の型は (forall s. Mut s a %1-> Ur b) %1-> Ur b であるべきですね。 ↩︎