Alpha Beta Epsilon

Categories:

【幽霊型トリック集】キェェ!幽霊型でバグを呪い殺すのじゃ!【呪術プログラミング】

この投稿は ML Advent Calendar 2015 の 16 日目の記事です。早速ですが、タイトルの「呪術プログラミング」という用語は単なる釣りです。 こんな専門用語は存在しません。 あと、Advent Calendar に「この記事を読むと呪われる」とか書きましたが、 SNSで拡散すると解呪できます ウソです。呪われないので安心してください。 「幽霊型」というキーワードでググると、幾つかの記事や発表のスライドがヒットしますが、 幽霊型 (phantom type) の有用なテクニックについて広く浅く紹介した記事がないように思えたので、 私が書くことにしました。 この記事では、私が今までに書いた幽霊型に関する記事と、その概要をまとめています。

Categories:

Standard ML の機能だけ使って、幽霊型で部分型付けする (2)

Standard ML の機能だけ使って、幽霊型で部分型付けする (1)」では、 Standard ML の言語機能だけで部分型付けを実現する方法を紹介しましたが、 有界全称型(forall 'a <: t. 'a -> 'a のような型)を実現するために色々な制限が付いていました。 今回紹介する方法も Standard ML の言語機能だけで部分型付けを実現しますが、 有界全称型の実現を完全に諦めて、共変性と反変性の実現に重点を置いています。 部分型について知らない人は、 「幽霊型による部分型付けの紹介」を読むと良いでしょう。

Categories:

Standard ML の機能だけ使って、幽霊型で部分型付けする (1)

幽霊型による部分型付けの紹介記事 では、多相バリアント型とクラス型を幽霊型変数に入れて、 オリジナルの部分型付けをする話について書きました。 実は、多相バリアントやクラスのような OCaml の拡張機能に頼らず、 Standard ML の言語機能だけで部分型付けを実現する方法があります。 この記事では、 Phantom Types and Subtyping [Fluet and Pucella, JFP 2006] の方法を紹介します。

Categories:

幽霊型で引数の値によって戻り値型が変わる関数を実現する

幽霊型 (phantom type) を使ったプログラミングをしていると、 引数のに応じて、戻り値のが変化するような関数を書きたくなります。 ML の型システムの範囲では、引数のに応じて、 戻り値の型が変わる関数は簡単に書けます。 例えば、List.hd : 'a list -> 'a は、 引数の型が int list なら戻り値型は intfloat list なら float のように、 型変数を使うことで、引数の型が変わると、戻り値型が変わる関数を書くことが出来ます。 しかし、例えば、true を受け取ると ('a, z s s) sized_list を返すけど、 false を受け取ると ('a, z) sized_list を返す、などのように、 引数の値に応じて、戻り値の型が変化するような関数は、簡単には書けません。 この記事では、そんな捻くれた関数の書き方を紹介します。

Categories:

幽霊型による部分型付けの紹介

これまでは、幽霊型を使って、型レベルの自然数や整数を作る方法を中心に話してきました。 幽霊型がなんだかわからない人は、 幽霊型の紹介 読むとよいでしょう。 今回は、もう少し違ったテーマとして、幽霊型を使った部分型付けの話をしたいと思います。 予定では、今回も含めて 3 種類の方法を紹介するつもりですが、 結論から言うと、今回の方法は変な制限がなく、最も扱いやすい手法です。