型をさらに拡張するーーRefinement Typesについて

本日の料理

パン粉でカツ丼の味になるレシピをためしたところだが、世界はそれほど甘くないことを実感させられた。

本文

「型」といえば普通何を考えるだろうか。大抵の場合、「型」というものは、Integerであったり、あるいはStringといったようなものを想像するだろう。例えば、Typed Racketの場合、引数で受けとったIntegerをそのまま返すとした場合、次のような定義ができる。

(: simple-integer : (-> Integer Integer))
(define (simple-integer x) x)

さて、このように型付けされた場合、型チェックのシステムとしては、引数として入ってくるxがIntegerかどうかにしか興味がない。その値が具体的にどのような形を取るか、ということに関しては、関数の内部においての責務ということになっている。

しかし、ここでちょっと立ちどまってみよう。型というのは、なんらかの要素がIntegerに属しているかどうかをチェックするものである。もうすこし考えるならば、何らかの型が「そこに属しているかどうか」をさらに絞りこむ形の型があってもいいのではないか。

Dive to Typed Racket

実際、RacketにはPositive-Integerというものが用意されている。実際に、そのコードを見てみると次のようになる。このコードは、著者環境のUbuntuだと/usr/racket/share/pkgs/typed-racket-lib/types/のnumeric-tower.rktに収録されている:

(define/decl -PosIntNotFixnum
  (make-Base 'Positive-Integer-Not-Fixnum
             #'(and/c exact-integer? positive? (not/c fixnum?))
             (lambda (x) (and (exact-integer? x)
                              (positive? x)
                              (not (portable-fixnum? x))))))

なんとなく、どういう風に型を付けているのかに関してはわかると思う。このように、型というものを「ある値xに対して、それがその型に属しているかどうか」というものを表現するためのものであるとするならば、Positive-Integerのような型はあっていい筈である。

ちょっと調べた感じだと、このような型を新しく定義する方法を見つけられなかったため、今回については割愛したいと思うが、余裕が出てきたら、このあたりについても調べたいと思う。

型を拡張する

さて、このようなアプローチは論文で提出されている。具体的に読みたければ、Occurrence Typing Modulo Theoriesという論文が2015年に公開されている。この論文には導出規則なども掲載されているが、著者の力では読みとくことができなかったため、理解できたところだけを、自分なりの理解で説明しようと思う。

前にも述べたように、「型」がある値がその型に属しているかどうかをチェックする門番みたいな役割であるとするならば、(乱暴に言ってしまうと)表面的な「数字」とか、あるいは「文字列」であるといったような表現だけでは不十分である。

先程も述べたように、例えばPositive-Integerであるならば、負の整数に関しては排除されるべきだろう。そのように考えるとするならば、次のような表現だってできるはずだ(以下の例は論文によるものである)

(: max : [x : Int ] [y : Int] ~>
  (Refine [z : Int ]
     (and (>= z x) (>= z y))))
(define (max x y) (if (> x y) x y))

このように、型に属するであろう任意の要素を取ってきて、それに当てはまるかどうかをチェックすることによって、より厳密な型によるチェックが行える。この場合であるならば、「Int型に属するx、及びyは、必ずzというより上位の数を所持している」ということになる(考えてみればわかるように、もし、xやyに、上位のzの数が存在しないと仮定すると、関数定義において、(> x y)という比較は成りたたない)

だた、一方で私見ではあるが、このような型は、型による値のチェックロジックが、型に寄っているのではないか、という点で、少々やりすぎなのではないかという気もしなくはない。

Liquid Haskell

とはいえ、このようなアイデア自体はどうも珍しいものではなく、先行研究として、Microsoft Researchが研究していた、F*(F starと読む)であったり、あるいはLiquid Haskellといったように、型に対して、そこに属する要素 を取りあつかえるようにするという試みは行なわれている。

実際、Haskellの上においても、このようなRefinement Typesというのを提案している。詳しくは、このサイトおよび、Refinement Types For Haskellの論文を参考にしてもらいたい。Introductionを読めば、どのような型付けをしたいのかがわかるはずだ。

type Pos = {v:Int | v > 0 }
type Nat = {v:Int | v <= 0 }

今までの議論は、入力におけるチェックに中心を置いてきた。然し、型システムに関しては、もう一つの役割がある。それは、出力において、確かにそのような出力が保証されているかどうか、ということである。例えば、単純に数字を増やすような関数を定義することを考えてみよう。

inc :: z:Int -> {v:Int | v > z }
inc z = z + 1

若干、論文のコードを変更させてもらった。ポイントは、入力されたIntの数が、その値を返すさいに、任意のInt型よりも上になっていることを保証するということである。

まとめ

型というと、どうしても例のIntegerやStringといったような、ある入力が属している型のことを想像しがちなのである。

型というものを、「ある要素xが属する集合」として捉えた場合、その「集合」だけを取りあつかうのは、確かに考えてみれば、不十分にも思える。「何らかの集合」が存在する場合、空集合を除くならば、「それに属する要素」というのも同様に存在している筈である。とすると、型において、その要素を検証するという方法は、それほど不自然ではない筈だ。

今回は、そのあたりについて、ちょっと面白い論文を見つけたので、概要をメモしてみた。もちろん、これが正確な説明であるという自信は全くない。もっと詳しい人がいれば、説明して頂けることを祈っている。