Zenn
👻

「幽霊型」の意味がややこしい

2022/11/13に公開
OCaml
#
phantomtypes
#
typelevelprogrammi
tech

前回の記事で幽霊型について紹介しましたが、もしかしたら「幽霊型って用語の使い方、変じゃない？」と思った人もいるかもしれません (Haskeller とか)。実は「幽霊型」という専門用語が具体的に何を指しているのか、専門家の間でも定義が統一されていません。これは私が卒論を書く時かなり悩んだところでもあります。調べたところ、幾つかの派閥に分かれていて結構ややこしい事になっていました。検索しても有用なサーベイが見つからなかったので、メモも兼ねてここに書いておきます。

前回の記事で定義した型を思い出してみます。

type 'a channel = IC of in_channel | OC of out_channel
type input
type output

'a channel の 'a のように「型定義の右辺に現れない型変数」を「幽霊型変数」と呼ぶことは、間違いないです。しかし、「幽霊型」が何を指すのかについては、以下のような派閥があります。

「幽霊型変数に代入される型」を「幽霊型」と呼ぶ派

この派閥の人たちは、input や output のように、「幽霊型変数に代入される型」を「幽霊型」と呼びます。これらの型は、（今回のように）しばしば値を持たない型として定義されます（次回以降の記事に書きますが、あえて値を持つ型として定義することがあります）。仮に値を持っていても、その型の値が使用されることはないので、値を持つことに重要な意味はありません。まさに、幽霊って感じですね。私もこの派閥に属しています。他にも、Blume の論文

の p.5 の真ん中あたりで

all other types are phantom types without meaningful values;

と述べられています。また、Fluet の論文

においても、p. 2 の真ん中あたりで、

... the types int safe_atom and bool safe_atom do not unify. (Observe that our
use of int and bool as phantom types is arbitrary; we could have used any two types
that do not unify to make the integer versus boolean distinction.)

と言っていることから、幽霊型変数に代入されるような型のことを「幽霊型」と呼んでいることがわかります（ちなみに、'a safe_atom の 'a は幽霊型変数です）。加えて、Kiselyov の論文

においても、「幽霊型」を「幽霊型変数に代入される型」の意味で使っています（p. 8の3.2節第2段落を参照）。

「幽霊型変数を含むような多相型」を「幽霊型」と呼ぶ派

この派閥の人たちは、'a channel のような「幽霊型変数を含むような多相型」を「幽霊型」と呼びます。'a channel 自体は値を持つ型なので、個人的には、何が幽霊なのかよくわかりませんが、存在することは事実です。統計を取ったことがありませんので、私見ではありますが、この派閥はそこそこ多数派です。なにせ、Haskell Wiki の冒頭で

A phantom type is a parametrised type whose parameters do not all appear
on the right-hand side of its definition, ...

と紹介されているくらいです。恐らく、Haskeller はこの派閥に属している人が多いと思われます。また、Leijen の論文

の p.13 の右側の上から2つめの段落の末尾で

Phantom types, polymorphic types whose type parameter is only used
at compile-time ...

と述べられています。

GADT を「幽霊型」と呼ぶ人

何故か、GADT (Generalized Algebraic Data Type) を「幽霊型」と呼ぶ人もいます。確認されている限り、この意味で使う人は、Ralf Hinze とその論文を読んだ人くらいです。昔、査読者に幽霊型は GADT とか言われて混乱しましたことがあります。Hinze は自分の論文の中で一貫して、GADT を幽霊型と呼んでいるようです。以下の論文に登場する first-class phantom type が GADT であり、second-class phantom type が一般的に言われている幽霊型のことです。

論文中で明確に GADT とは述べていないものの、本質的には GADT と同じものと思います。また、以下の論文でも、GADT を幽霊型と呼んでいるようです。

論文の中で「幽霊型」という用語の定義を明確に述べない派

ある意味、一番無難な選択です。査読者や聴衆から「それ幽霊型じゃなくね？」というツッコミを受けることも無いでしょう。「幽霊型、おまえら知ってるよな？」くらいの勢いで書いてるんでしょうか。この派閥には、以下の論文などが属しています。

幽霊型を「幽霊型変数を使ったプログラミング手法」という意味で使っている可能性もあります。論文によっては、phantom type trick とか phantom type technique と書かれることもあります。

そもそも、論文の中に「幽霊型」という単語が登場しない派

幽霊型は、ずいぶんと昔から使われてきたトリックようですが、「幽霊型」という単語が本文に一度も登場しないのに、幽霊型を使ったトリックを披露しちゃってる論文もあります。

既存の幽霊型を扱っている論文の参考文献リストを片っ端から読むという力技でしか、この手の論文は発見できません。少なくとも、検索には引っかからない。

後日談

幽霊型トリックを含む関数型プログラミングについて世界的に有名な Oleg Kiselyov さん（東北大学）に上記の内容を話し、幽霊型の意味について質問してみました。Oleg さん曰く、幽霊型トリックは古くからフォークロアとして用いられていたそうです。最初は幽霊型トリック自体に特に名前が付いておらず、後から名付けたため用語の定義が分かれてしまったのではないか、とのことでした。ちなみに、幽霊型に関する論文としては

  • No-Longer-Foreign: Teaching an ML compiler to speak C "natively" [Blume, EPTCS'01]
  • Phantom types and subtyping [Fluet & Pucella, JFP'06]

の2本が有名と教えて頂きました。

結論

幽霊型を最初に扱った論文を調べて、「幽霊型のオリジナルの意味はコレだ！」みたいに結論づけたいところですが、「幽霊型という単語が登場しない派」には、結構古い論文が含まれていたりして、追跡はかなり大変です。私はそんなに暇ではないので、「幽霊型」という用語の源流を特定することは難しそうです。

現状、幽霊型に関する論文を読むときは、用語の意味として、

  • 幽霊型変数に代入される（しばしば値を持たない）型
  • 幽霊型変数を持つような多相型
  • 幽霊型変数を使うようなプログラミング手法

の3種類の候補を念頭に考えていたほうが良さそうです（ただし、著者に Hinze が含まれているなら、GADT）。

なんだか、曖昧なままですみません。もし、幽霊型を最初に扱った論文について、知っている人がいたら、教えて下さい。

編集履歴

  • 2015/12/16 Hinze の phantom type の解釈について編集
  • 2016/3/28 「後日談」を追加

Discussion