偶数か奇数かを静的に型チェックする

PAIP 本 p.27 の「静的型付けの言語でも偶数を期待する関数に奇数を渡すのをチェックしてくれるわけではない」に関連して、以下のような OCaml モジュールを書いた。

(* oddeven.mli *)

type 'a t constraint 'a = [< `Even | `Odd ]

val zero : [`Even] t
val one : [`Odd] t

val make_even : int -> [`Even] t
val make_odd : int -> [`Odd] t

val to_int : 'a t -> int

val succ : 'a t -> 'a t
val pred : 'a t -> 'a t

val succ_odd : [`Even] t -> [`Odd] t
val pred_odd : [`Even] t -> [`Odd] t

val succ_even : [`Odd] t -> [`Even] t
val pred_even : [`Odd] t -> [`Even] t

val ( +$ ) : 'a t -> 'a t -> [`Even] t
val ( -$ ) : 'a t -> 'a t -> [`Even] t
val ( *$ ) : 'a t -> 'a t -> 'a t
val ( /$ ) : 'a t -> 'a t -> int

val print : Format.formatter -> 'a t -> unit

(* oddeven.ml *)

type 'a t = int constraint 'a = [< `Even | `Odd ]

let zero = 0
let one = 1

let make_even i =
  if i mod 2 = 0 then i
  else raise (Invalid_argument "must be even integer")
let make_odd i =
  if abs (i mod 2) = 1 then i
  else raise (Invalid_argument "must be odd integer")

let to_int i = i

let succ i = i + 2
let pred i = i - 2

let succ_odd i = i + 1
let pred_odd i = i - 1

let succ_even i = i + 1
let pred_even i = i - 1

let ( +$ ) m n = m + n
let ( -$ ) m n = m - n
let ( *$ ) m n = m * n
let ( /$ ) m n = m / n

let print p i = Format.print_string (string_of_int i)

このようにすると、

# #load "oddeven.cmo";;
# open Oddeven;;
# #install_printer print;;
# zero;;
- : [ `Even ] Oddeven.t = 0
# one;;
- : [ `Odd ] Oddeven.t = 1
# let two = make_even 2;;
val two : [ `Even ] Oddeven.t = 2
# let three = succ one;;
val three : [ `Odd ] Oddeven.t = 3
# let four = one +$ three;;
val four : [ `Even ] Oddeven.t = 4
# let five = succ_odd four;;
val five : [ `Odd ] Oddeven.t = 5
# succ_odd five;;
This expression has type [ `Odd ] Oddeven.t but is here used with type
  [ `Even ] Oddeven.t
These two variant types have no intersection

というわけで偶数を期待する succ_odd に奇数を渡したときにコンパイル時エラーとなる。

ただこのモジュールは偶数か奇数かが同じもの同士の演算しか定義していなくて、そうじゃない場合まで考えるとなんか面倒になりそう。

細かいことを考えなければ

val add : 'a t -> 'b t -> int

みたいになるけど、これは全然うれしくなくて、例えば任意の整数に偶数を足しても偶数か奇数かは変わらないということを考慮したければ、

val add_even : 'a t -> [`Even] t -> 'a t

となって、交換法則があるのでさらに、

val even_add : [`Even] t -> 'a t -> 'a t

とか、こうした1つ1つを適宜使い分けていくというのはさすがにどうか。何かうまい方法があるのだろうか。

もう一つ問題は Oddeven.t 型の値のコンストラクタとして make_even と make_odd を用意したけど、これに間違った値が来た場合のエラーは実行時にせざるを得ない。

それは引数がリテラルのようにコンパイル時に決定されている場合でも同様で、

# make_even 7;;
Exception: Invalid_argument "must be even integer".

となる。7 は int のリテラルなのであって Oddeven.t のリテラルじゃないんだからしょうがない。以前も少し書いたけど抽象データ型とリテラルはお互いにうまく溶け合わないってことになるんだろうか。