TweagがHaskellで層を表現、貼り合わせ操作を明示的に

Arnaud SpiwackはHaskellで層を表現したいと考えていたが、教科書的な定義には実用上の問題があった。篩は同じマッチング情報の冗長な表現を多数含んでおり、その依存的な引き戻し構成はHaskellにとって依存型付けが過剰であった。明白なアプローチ、すなわち定義を文字通りに翻訳することは、不正な状態を表現可能にしてしまい、プログラムを無関係なデータで埋め尽くすことになる。

彼はまず算術式を題材に具体的な例を構築した。前層は式に沿って値を引き戻すことができたが、望ましい条件分岐操作には、ブール被覆上の2つの分岐を貼り合わせる層が必要であった。そこで実装では貼り合わせを明示的な型クラス操作とし、それを一般化して、型付きのCoverとGenの族がどの部品を組み立てられるかを記述するSiteとした。

型付きサイトは引き戻し篩の負担を取り除く。glueは任意の射で動作でき、生成子は実際の射として表現される必要がない。積、指数、米田埋め込み、余積、再帰的リストは同じ流儀で定義できる。Sheafifyは貼り合わせ操作を早期に評価するのではなく保存することで自由層構成として機能し、PFunは指数に必要な分散性を担う。

その成果はデモンストレーション用リポジトリと、この抽象的なアイデアのHaskell的な実装であり、数学的な細部がすべて消えると主張するものではない。Spiwackは不動点を明示的に未解決のまま残しているが、このプロジェクトは言語にとって緩すぎた定義を型付きの操作的な構成要素へと変換し、残された未知を正確なものにしている。

被覆を型として表現し、明示的に貼り合わせる

文字通りの篩は冗長なマッチング族の値をエンコードし、本来あり得ないはずの状態を許してしまう。

指数に必要な引き戻し篩は、Haskell実装が快適に表現できる範囲を超えた依存型付けを要求する。

型付き被覆と生成子は、有効な貼り合わせインターフェースを小さく保ちつつ、無関係な表現を取り除く。

Sheafifyは貼り合わせの構文を保存し、操作を早期に実行することなく余積や再帰的リストのような自由構成を可能にする。

不動点を明示的な未解決の境界とすることで、実装がまだ知らないことを解いたふりをするのを防ぐ。

形式的な定義が不正な状態と不可能な依存型付けを生み出す場合には、有効な被覆を型にエンコードし、実行可能な貼り合わせ操作のみを公開する。構成のためには自由構成を保つ。

このプロジェクトは、具体的および抽象的なSite/Sheafインスタンスを備えたデモンストレーション用リポジトリを生み出し、さらにこのエンコーディングが表現できることとできないことの境界を明確にした。不動点は未解決のままであるが、型付き被覆のアプローチにより、篩依存の機構の全重量を持ち込むことなく、層の操作をHaskellで利用できるようになった。