ocaml – I want to create a polymorphic open recursion

Question: Question:

When I was writing something like a solution to an expression problem using the Extensible variant types introduced in OCaml 4.02, I wanted a polymorphic open recursion, but I'm having trouble writing it.

module Lang = struct
  type 'a expr = ..
  type 'a expr +=
      Num : int -> int expr
    | App : ('a -> 'b) expr * 'a expr -> 'b expr

  type reval = { f : 'a. 'a expr -> 'a }

  (* open recursion. polymorphicなlet recだと拡張できないので。 *)
  (* evalをレコードにしてあるのは、Appのeval適用で型が異なる適用を二回行うので、forallを付ける必要があったから。 *)
  let open_eval (type a) (eval:reval) (exp:a expr) : a =
    match exp with
      Num i -> i
    | App (f, x) -> eval.f f (eval.f x)
    | _ -> failwith "no match"
end

(* Langのデータと関数の両方の拡張. *)
module Plus = struct
  type 'a Lang.expr += 
      Plus : (int -> int -> int) Lang.expr

  let open_eval (type a) (eval:Lang.reval) (expr:a Lang.expr) : a = 
    match expr with
      Plus -> (+)
    | x -> Lang.open_eval eval x

  let show : type a. a Lang.expr -> string = function
      Plus -> "plus"
    | Lang.App _ -> "app"
    | Lang.Num _ -> "num"
    | _ -> "no match"
end

Up to this point, it will compile. However, after that, I want to fix Plus.open_eval with the fixed point operator fix. How can I write the implementation of fix?
I know that the normal fixed point operator can be applied as in the article below.
http://d.hatena.ne.jp/KeisukeNakano/20060926/1159273362
I may not be able to write it in the first place, but I would appreciate your advice.

Postscript <br /> By the way,

let fix (`M x) y = y Lang.{ f = fun z -> x (`M x) y z }

Then
Error: This field value has type'b Lang.expr->'b which is less general than'a.'a Lang.expr->'a
An error will occur when defining fix. orz

Answer: Answer:

First, let's take a fixed point without being particular about it.

open Lang

let rec fixed =
  fun x -> Plus.open_eval { f = fixed }  x

This is an error.

File "xxx", line 40, characters 36-41:
Error: This field value has type 'b Lang.expr -> 'b
       which is less general than 'a. 'a Lang.expr -> 'a

The reason is that in ML you can't take a polymorphic type inside a value defined by let , here fixed , let , and you can't plunge into a polymorphic field { f = .. } . It is in the same state as adding a question.

To give fixed a polymorphic type internally, you can explicitly specify the polymorphic type of fixed and use polymorphic recursion:

open Lang
open Plus

let rec fixed : 'a . 'a expr -> 'a = (* <= これがミソ *)
  fun x -> Plus.open_eval { f = fixed }  x  (* 内部でも fixed は多相型を持つので reval に突っ込める *)

let () =
  print_int @@ fixed
    (App 
       (App (Plus, (App (App (Plus, Num 21), Num 21))),
        App (App (Plus, Num 21), Num 21)))

84 is output.

So-called fixed point operator

let rec fix f x = f (fix f) x

You have to open_eval to the value ('a eval -> 'a) -> 'a eval -> 'a to get into

let open_eval' = fun f x -> Plus.open_eval {f = f} x   (* うまくいかない… *)

I want a type like open_eval' : 'a. ('b . 'b expr -> 'b) -> 'a expr , but if this is written, the high rank polymorphic encoding by the polymorphic record feel is originally I don't need it, so I think it's impossible.

I think it's okay to give up fix if you realize the title of the question that you want to create a polymorphic open recursion …

Post Views: 5
Scroll to Top