幽霊型による部分型付けの紹介
幽霊型による部分型付けの紹介 これまでは、幽霊型を使って、型レベルの自然数や整数を作る方法を中心に話してきました。 幽霊型がなんだかわからない人は、 幽霊型の紹介 読むとよいでしょう。 今回は、もう少し違ったテーマとして、幽霊型を使った部分型付けの話をしたいと思います。 予定では、今回も含めて 3 種類の方法を紹介するつもりですが、 結論から言うと、今回の方法は変な制限がなく、最も扱いやすい手法です。 基礎知識 部分型って何？ この記事では、便宜上、型は値の集合である、と思うことにしましょう （値の集合だと、一般的な型の定義としては狭すぎますが、あくまで説明の都合です）。 例えば、int 型は整数の集合 $\mathbb{Z}$、nat 型は自然数の集合 $\mathbb{N}$、 という具合に対応します。 集合には、部分集合として包含関係があり、先程の例では $\mathbb{N} \s
幽霊型の紹介
幽霊型の紹介 ときどき、ネットで幽霊型 (phantom type) という単語を見かるようになりました。 私は幽霊型を応用した線形代数演算ライブラリ SLAP (Sized Linear Algebra Package) を開発しており、 幽霊型についてはちょっとだけ詳しいつもりでいます（本物の研究者に比べれば雑魚同然ですが）。 なので、今後何回かに記事を分けて、幽霊型のトリックについて、知っていることを書いていこうと思います。 基本的には、関数型プログラミング言語 OCaml を使って説明しますが、 可能な限り OCaml の独自拡張は使わない方針でいきます。 今日はウォーミングアップも兼ねて、簡単な幽霊型の紹介だけします。 トリッキーなテクニックは次回以降で扱う予定です。 入出力両方のチャンネルに適用可能な seek 関数を作る OCaml のチャンネル型（C で言うところ FILE
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
