Zenn
Open8

Paper: 『Destination-passing style programming: a Haskell implementation』

Haskell
hatahata

Destination-passing style 、略して DPS の源流は初期の命令形言語の関数にアドレスをわたすことで、結果をそこに書いてもらうようなメモリ管理方式にある、と書いてある。C言語やGo言語のような関数の引数にポインタを渡してそこに結果のデータセットが入れられている、というよくある関数実装と思って良さそう。

DPS は、それをあくまで関数型スタイルに落とし込んだもの。なので、C言語などの書き込み先のポインタを渡すやり方自体は DPS とは呼ばない。

  • 用語
    • out parameter: 上記のような結果を書き込む用途の引数のことをしばしばそう呼ぶ。[1]
    • arbitary data structures with holes （穴のある任意のデータ構造）: まだ埋められていない、つまりまだ初期化されていない部分をもつデータ構造。
    • destination: それへのポインタ。
脚注

  1. アウトパラメータって一般的な用語？C言語とかの話するときにも普通に使える便利な用語ですね。 ↩︎

hatahata

we say that a destination is consumed when it has already been used to write something in its associated hole. It must not be reused after that point, to ensure immutability and prevent a range of memory errors.

destinationが消費されるのは、そのdestinationが関連付けられたholeに何かを書き込むためにすでに使われたときである。不変性を保証し、さまざまなメモリーエラーを防ぐために、それ以降は再利用してはならない。

In this paper, I design a destination API whose memory safety (write-once model) is ensured through a linear type discipline.

本稿では、線形型の規律によってメモリ安全性（write-once model）が確保されたdestination APIを設計する。

hatahata

Linear type systems （線形型システム？）

Linear type systems are based on Girard’s Linear logic, and introduce the concept of linearity: one can express through types that a function will consume its argument exactly once given the function result is consumed exactly once.

Linear type systemsは、Girardの線形論理に基づいており、線形性の概念を導入している。ある関数がその引数を正確に一度だけ消費し、関数の結果が正確に一度だけ消費されることを型を通して表現することができる。

引用されている論文はこれか。

hatahata

The Haskell programming language is equipped with support for linear types through its main compiler, GHC, since version 9.0.1

Haskellはv9.0.1以降、メインコンパイラであるGHCによってlinear typesをサポートしている。

2021-02-04 なのでわりと最近だけどもう３年前なのか。

GHC 9.0.1 is now available — The Glasgow Haskell Compiler

bgamari - 2021-02-04
The GHC team is very pleased to announce the availability of GHC 9.0.1. Source and binary distributions are available at the usual place.

A first cut of the new LinearTypes language extension, allowing use of linear function syntax and linear record fields.

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

そもそもLinear Typeとはどのような概念なのか、簡単に説明すると、「関数の引数がちょうど1度だけ評価される」、という条件を指定できるもののようだ。

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

GHCの線形型プロトタイプを試すだけ - syocy’s diary

ひとつ気になることがあるとすれば、線形型GHCを主導しているのが Tweag I/O だということだ。 Tweag はGHCを拡張して asterius という Haskell to WebAssembly コンパイラを開発している。 GHCへの線形型の導入が、将来の Haskell によるWebプログラミングを見据えてのものだという可能性はあると思う。 クライアントサイドWeb開発はまさにレイテンシが重要な領域だからだ。

hatahata

But Haskell is also a pure functional language, which means that side effects are usually not safe to produce outside of monadic contexts.

この「Destination-passing style programming」論文自体は GHC の Linear types の実装とは別アプローチで線形性を実装しようという話。