Racket 6.11で篩型(refinement type)と依存関数型(dependent function type)が安定機能に

Racket 6.11では、Typed Racketに篩(ふるい)型(refinement type)と依存関数型(dependent function type)が追加されている。

篩型は、その型の要素が保持すると想定される述語に関連付けられた型である。篩型を記述する一般的な構文は“(Refine [v : t] p)”で、述語pを満足する型tのすべての値vの型を表す。

篩型の基本的な例は次のようになる。これは戻り値が少なくとも各入力値と同じ大きさであることを保証する関数型である。

(-> ([x : Integer] [y : Integer]) (Refine [z : Integer] (and (>= z x) (>= z y))))

Racketでは篩型の述語部でプログラム用語を参照できるので、篩型の生成はそれら用語の値に依存する。次の例のように、整数値42のみを含む篩型を定義することも可能だ。

> (ann 42 (Refine [n : Integer] (<= n 42)))

依存関数型は篩型と同様の構文を使用して、引数間あるいは引数と関数範囲との依存関係を記述することができる。依存関係の循環は許されない。次の例は、範囲外条件を排除したベクトルの要素にアクセスする関数を定義する方法を示すものだ。

(: safe-ref1 (All (A) (-> ([v : (Vectorof A)]
                           [n : (v) (Refine [i : Natural]
                                (< i (vector-length v)))])
                            A)))

関数シグネチャの前提条件を使用して、同じ効果を得ることもできる。

(: safe-ref2 (All (A) (-> ([v : (Vectorof A)]
                           [n : Natural])
                          #:pre (v n) (< n (vector-length v))
                          A)))

InfoQとの会話で、Typed Racketの作者でメンテナであるSam Tobin-Hochstadt氏は、次のように説明している。

Typed Racketに依存型を持たせることで、他の大部分の言語では表現できないようなプログラムのプロパティのチェックが可能になります。この新しい情報を使うことで実現可能なプログラムの改善については、まだ検討を始めたばかりなのですが、篩型と依存型を使うことで、より高速で信頼性の高いソフトウェアがTyped Racketで可能になればと思っています。

篩型と依存関数はいずれも、Racketの前バージョンでは試験的機能として用意されていた。今回からはデフォルトで使用可能になったが、定期的にスナップショットビルドにアップデートして、最新のフィックスを入手するように推奨されている。また、Racket 6.11の依存型の使用方法について詳しく知りたいのであれば、Tobin-Hochstadt氏の指導の下でAndrew Kent氏が中心となって作成したイントロダクション資料を忘れてはならない。

依存型は、より表現力に富んだ型を定義可能にする型システムの機能であり、コンパイル時により多くのバグを検出するために使用できる。依存型をサポートする言語にはIdris、Coq、F*などがある他、Haskellでも実装が勧められている。