昨日のつづき

「動的型」(type dynamic)は拡張可能でないといけないので、拡張可能な型の値として、多相バリアントのかわりに例外をつかってみました。これならStandard MLも安心。

ちなみにYが必要なのは、printを拡張可能にするためにはopen recursionが必要で、そのためには自己適用が必要で、そのためには再帰型が必要だからです。

type dyn = exn
type 'a typ = ('a -> dyn) * (dyn -> 'a)
let to_dyn t x = (fst t) x
let of_dyn t x = (snd t) x
type 'a y = Y of ('a y -> 'a -> string)

exception Int of int
let int : int typ =
  (fun i -> Int i),
  (fun (Int i) -> i)
exception Bool of bool
let bool : bool typ =
  (fun b -> Bool b),
  (fun (Bool b) -> b)
exception List of dyn list
let list (a : 'a typ) : 'a list typ =
  (fun xs -> List (List.map (to_dyn a) xs)),
  (fun (List xs) -> List.map (of_dyn a) xs)
let print1 (Y self) = function
  | Int i -> string_of_int i
  | Bool b -> string_of_bool b
  | List xs ->
      let rec prints = function
        | [] -> ""
        | [x] -> self (Y self) x
        | y :: zs -> self (Y self) y ^ "; " ^ prints zs in
      "[" ^ prints xs ^ "]"

(* 後から「拡張」したつもり *)
exception Pair of dyn * dyn
let pair (a : 'a typ) (b : 'b typ) : ('a * 'b) typ =
  (fun (x, y) -> Pair (to_dyn a x, to_dyn b y)),
  (fun (Pair (x, y)) -> (of_dyn a x, of_dyn b y))
let print2 (Y self) = function
  | (Int _ | Bool _ | List _) as x -> print1 (Y self) x
  | Pair (x, y) -> "(" ^ self (Y self) x ^ ", " ^ self (Y self) y ^ ")"

# let t = list (pair int bool) ;;
val t : (int * bool) list typ = (<fun>, <fun>)
# let d = to_dyn t [(1, true); (2, false); (-3, false)] ;;
val d : dyn =
  List
   [Pair (Int 1, Bool true); Pair (Int 2, Bool false);
    Pair (Int (-3), Bool false)]
# print2 (Y print2) d ;;
- : string = "[(1, true); (2, false); (-3, false)]"