理想化Haskellと忖度翻訳 - 檜山正幸のキマイラ飼育記 (はてなBlog)

$\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\In}{\text{ in } } \newcommand{\Iff}{\Leftrightarrow} \newcommand{\rev}{\triangleleft} \require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } }% \newcommand{\Define}{\Keyword{Define } }% \newcommand{\Declare}{\Keyword{Declare } }% \newcommand{\Notation}{\Keyword{Notation } }%$ Haskell風構文の擬似コードで記述された概念をデカルト閉圏で解釈してみます。翻訳の過程でけっこうな“忖度”が要求されます。

内容：

理想化Haskell
デカルト閉圏に対する直訳
忖度翻訳

関連する記事：

Haskellの二重コロン「::」とバインド記号「>>=」の説明

理想化Haskell

ピカリング／ギブンス／ウーは、彼らの論文（下）において、擬似コードとして使うHaskell風構文を理想化Haskell〈an idealization of Haskell〉と呼んでいます。

Title: Profunctor Optics -- Modular Data Accessors
Authors: Matthew Pickering, Jeremy Gibbons, Nicolas Wu
Submitted: 31 Mar 2017
Pages: 51p
URL: https://arxiv.org/abs/1703.10857

この論文内では、実際に理想化Haskellを用いて抽象的概念を記述しています。

Haskell構文は、非常にコンパクトに書けるように工夫されています。が、コンパクト過ぎて可読性がいいとは言えません。冗長でも、情報が省略されてない半形式的構文〈semi-formal syntax〉のほうが読みやすいかも知れません。

もうひとつ、Haskell風構文による記述の問題点は“忖度”が必要なことです。「忖度」という言葉は2017年の流行語大賞に選ばれて有名になりましたが、なんか悪い意味が付着してしまったようです。本来の意味は：

他人の心情を推し量ること、また、推し量って相手に配慮することである。

ここでの「忖度」は本来の意味で、変な意味はありません。

ピカリング／ギブンス／ウー論文から具体例を一個挙げます。

cross ::(a → a') → (b → b') → (a, b) → (a', b')
cross f g (x, y) = (f x, g y)

これはプレーンテキストの擬似コードです。矢印記号はアスキー文字の -> ではなくて一文字矢印記号 → を使っています。矢印をアスキー文字にしてシンタックスハイライト（カラーリング）してみましょう。

cross ::(a -> a') -> (b -> b') -> (a, b) -> (a', b')
cross f g (x, y) = (f x, g y)

たいして色は付きませんね（まー、別にいいけど）。

ピカリング／ギブンス／ウーは、プレーンテキストの擬似コードをほとんどそのままTeX文書内に入れているみたいです。

$\quad cross ::(a \to a') \to (b \to b') \to (a, b) \to (a', b')\\ \quad cross\: f\: g\: (x, y) = (f\: x, g\: y)$

"cross" はローマン体（\mathrm{cross}）にしたほうがいいかな、とか思いますが、それをやりだすと書くのが面倒になるので、全部イタリック体と割り切ってしまうのは良い判断だと思います。

上記の理想化Haskellの短い擬似コードを、冗長な半形式的構文に翻訳して、さらに忖度しながら再解釈するとどうなるかやってみます。

デカルト閉圏に対する直訳

$\cat{C}$ は、集合圏の部分圏として埋め込まれたデカルト閉圏とします。デカルト積、単位対象、指数などのデカルト閉構造は、集合圏のそれをそのまま借用します。圏論の一般的な記法では：

デカルト積〈直積〉： $\times$
単位対象： ${\bf 1} = \{*\}$
指数対象： $[-, -]$

一般的ではない記号として $\in:$ を使います*1。この記号の意味は：

$\quad a\in: A \In \cat{C} :\Iff a: {\bf 1} \to A \In \cat{C}$

デカルト閉圏には評価射（の族）があります。

$\For A, B \in |\cat{C}|\\ \quad \mrm{ev}_{A, B}: [A, B]\times A \to B \In \cat{C}$

$\mrm{ev}$ の中置演算子記号として $\rev$ を使います。

$\For u \in [A, B], a \in A\\ \Notation u \rev a := \mrm{ev}_{A, B}( (u, a) ) \in B$

$u \in: [A, B]$ の場合も同じ記号 $\rev$ を使い、その場合は：

$\For u \in: [A, B], a \in A\\ \Notation u \rev a := \mrm{ev}_{A, B}( (u(*), a) ) \in B$

中置演算子記号を使うと、下付き添字の情報が失われるので、型推論により解決（省略された情報を再現）する必要があります。

Haskell風構文から、デカルト閉圏の記法への翻訳対応表は次のようになります。

Haskell風	デカルト閉圏
( , )	$\times$
()	${\bf 1}, *$
->	$[-, -]$
::	$\in:$
空白	$\rev$

他に冗長な説明的情報を緑色のキーワードを使って追加します。先程の事例と、その直訳を以下に並べて書きます。

原文：

$\quad cross ::(a \to a') \to (b \to b') \to (a, b) \to (a', b')\\ \quad cross\: f\: g\: (x, y) = (f\: x, g\: y)$

翻訳（直訳）：

$\For a, a', b, b' \in |\cat{C}|\\ \Declare cross \in: \big[\, [a, a'] ,\,[\, [b , b'] ,[ a\times b , a'\times b']\,] \,\big] \In \cat{C}\\ \:\\ \For f \in [a, a'], g\in [b, b']\\ \For (x, y) \in a\times b\\ \Define ( (cross \rev f) \rev g )\rev (x, y) := (f\rev x, g\rev y) \:\in a'\times b'$

直訳しただけでは意味（むしろ意図）がハッキリしませんね。

忖度翻訳

忖度翻訳は意訳と同じですが「書いた人が表現したかったことを推し量って再解釈する」ことを強調して「忖度」を付けています。

前節の $cross$ という高階関数は、2つの関数の直積を作る操作を意図しています。そこを“推し量って再解釈する”と、次のような記述が妥当でしょう。

$\For a, a', b, b' \in |\cat{C}|\\ \Declare cross : [a, a'] \times [b , b'] \to [ a\times b , a'\times b'] \In \cat{C}\\ \:\\ \For f \in [a, a'], g\in [b, b']\\ \For (x, y) \in a\times b\\ \Define cross( (f, g) )( (x, y) ) := (f(x), g(y) ) \:\in a'\times b' \\ \:\\ \Notation f\times g := cross( (f, g) )$

最後の行は、記号 $\times$ を関数に対してもオーバーロードする旨の宣言です。オーバーロードされた $\times$ を使って定義を書けば：

$\For f \in [a, a'], g\in [b, b']\\ \For (x, y) \in a\times b\\ \Define (f \times g )( (x, y) ) := (f(x), g(y) ) \:\in a'\times b'$

デカルト閉圏 $\cat{C}$ から出発すれば関数のデカルト積〈直積〉も組み込みなのですが、対象に対する直積と高階関数定義を用いれば「後から関数のデカルト積も定義できるよ」ということが、背後のストーリーです。

コンパクトな記法で大幅な省略をすると、読む側の忖度行為が増えます。他人の意図を推し量るのは難しいので、冗長でも情報豊富な書き方のほうがいいんじゃないか、と僕は思います。いずれにしても、忖度のトレーニングは必要になるのではありますがね。

*1:[追記]今回の説明では $\in:$ は不要で、単に $\in$ だけでもよかったな、と思っています。が、訂正はせずに残しておきます。[/追記]