Alpha Beta Epsilon

Categories:

幽霊型による型レベル自然数の加算・乗算

今回は、OCaml のモジュールプログラミングを応用して、型レベル自然数の加算と乗算を実現します。 今までは、モジュールというと、幽霊型を使ったトリックが型検査器に無視されないように、 実装を隠蔽する目的で使ってきました。 今日紹介するプログラムでは、モジュール上の関数であるファンクターを使って、 かなりトリッキーなことをします。 いわゆるスパゲッティ・コードではなく、もっと純粋に意味不明な部類のコードだと思います。 普通の OCaml プログラミングで、今回紹介するような気色悪いモジュールプログラミングが使われることは、まずありません。

Categories:

幽霊型による型レベル整数と加算・減算

古より(主に関数型プログラミング界隈の人たちの間で)、 幽霊型 (phantom type) と呼ばれる伝統のプログラミング技法が使われてきました。 研究レベルでは随分と昔から使われているのですが、結構トリッキーなので、 実際のソフトウェア開発の現場で見ることは少ないと思います。 でも、幽霊型を使うと、プログラムのバグをコンパイル時に検出できたりします。 使いこなすのには慣れがいるけど、それなりに有用なテクニックなので、 最近、幽霊型の紹介記事を幾つか書いています。 今日は、前回の記事「幽霊型による非空リストと型レベル自然数」の続きで、 型の上で「整数」を実現してみます。

Categories:

幽霊型による非空リストと型レベル自然数

今日は、幽霊型を使って、OCaml の List モジュールの hd 関数と tl 関数を型安全にするお話です。 ご存知の通り、これらの関数は空リストを与えると、例外、つまり実行時エラーを発生させます。 今回は、空リストを与えた時に型エラーが発生するように実装してみたいと思います。 幽霊型の紹介については、前々回の記事で済ませているので、 今日はやや発展的なテクニックである型レベル自然数について紹介します。 OCaml を例に紹介しますが、原理的には Haskell、Scala、Java、C++ などでも同じ事ができるはずです。

Categories:

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

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

Categories:

幽霊型の紹介

ときどき、ネットで幽霊型 (phantom type) という単語を見かるようになりました。 私は幽霊型を応用した線形代数演算ライブラリ SLAP (Sized Linear Algebra Package) を開発しており、 幽霊型についてはちょっとだけ詳しいつもりでいます(本物の研究者に比べれば雑魚同然ですが)。 なので、今後何回かに記事を分けて、幽霊型のトリックについて、知っていることを書いていこうと思います。