

OCaml 4.02で導入されたExtensible variant typesを使ってexpression
problemの解のようなものを書いていた際、polymorphicなopen recursionが欲しくなりましたが、書けなくて困っています。

[code]

    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
    
[/code]

ここまではコンパイル通ります。しかし、その後不動点演算子fixによって`fix
Plus.open_eval`したいのですが、fixの実装はどうやって書けばいいのでしょうか？  
通常の不動点演算子は下記の記事のようにかけるのは知っています。  
<http://d.hatena.ne.jp/KeisukeNakano/20060926/1159273362>  
そもそも書けないのかもしれませんが、ご助言ありましたら宜しくお願い申し上げます。

**追記**  
ちなみに、

[code]

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

だと  
Error: This field value has type 'b Lang.expr -> 'b which is less general than
'a. 'a Lang.expr -> 'a  
のようにfix定義時にエラーになります。orz


CC BY-SA 3.0
2015-01-25T19:29:17.853
5270
2015-01-30T01:05:42.273
2015-01-26T04:07:39.907
898
7611
question
ocaml
polymorphicなopen recursionを作りたい


まず、特にこだわらずに不動点を取ってみます。

[code]

    open Lang
    
    let rec fixed =
      fun x -> Plus.open_eval { f = fixed }  x
    
[/code]

これはエラーです。

[code]

    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
    
[/code]

理由は ML では `let` で定義されている値、ここでは `fixed`、 `let` の内側では多相的な型を取れず、多相フィールド `{ f = ..
}` に突っ込めないからです。ご質問の追記と同じ状態です。

内部で `fixed` に多相的な型を持たせるには、`fixed` の多相型を明示して polymorphic recursion を使えばよいです:

[code]

    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)))
    
[/code]

`84` が出力されます。

所謂不動点演算子

[code]

    let rec fix f x = f (fix f) x
    
[/code]

に突っ込むには `open_eval` を `('a eval -> 'a) -> 'a eval -> 'a` という値に変えなければいけませんが、

[code]

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

これは `open_eval' : 'a. ('b . 'b expr -> 'b) -> 'a expr`
のような型が欲しいのですが、これが書ければもともと多相レコードフィールによる高rank多相エンコードは必要ないわけですから、無理っぽいかなあと思います。

Polymorphic な open recursion を作りたい、という質問のタイトルを実現するならば `fix`
はあきらめてもいいんじゃないかと思います…


CC BY-SA 3.0
2015-01-26T04:03:52.630
5301
2015-01-26T04:42:15.373
2015-01-26T04:42:15.373
898
898
5270
answer


普通の fix が使えなくても、open_eval専用の fix が定義できますよ。

[code]

    let open_eval_wrap eval = {f = fun x -> open_eval eval x}
    
    let rec eval_fix (evalf : reval -> reval) : reval =
      {f = fun x -> (evalf (eval_fix evalf)).f x}
    
    let eval x = (eval_fix open_eval_wrap).f x
    
[/code]

それで答えになりますか？

また、邪魔しているのは関数型というcamlspotterのコメントに注目して、lazy
を使った不動点という手もあります。こちらは完全に一般的な形になります。

[code]

    let rec lazy_fix (f : 'a Lazy.t -> 'a) =
      lazy (f (lazy_fix f))
    
[/code]

定義を少し変える必要があります。

[code]

    module Lang = struct
      type 'a expr = ..
      type 'a expr +=
          Num : int -> int expr
        | App : ('a -> 'b) expr * 'a expr -> 'b expr
        | Succ : (int -> int) expr
    
      type reval = { f : 'a. 'a expr -> 'a }
      let run (eval : reval Lazy.t) = (Lazy.force eval).f
    
      let open_eval (type a) eval (exp:a expr) : a =
        match exp with
          Num i -> i
        | App (f, x) -> run eval f (run eval x)
        | Succ -> succ
        | _ -> failwith "no match"
    
      let open_eval_wrap eval = {f = fun x -> open_eval eval x}
    end
    
[/code]

そうすると、不動点の閉じ方はこれで済みます。

[code]

    let eval x = Lang.run (lazy_fix Plus.open_eval_wrap) x
    
[/code]


CC BY-SA 3.0
2015-01-27T02:54:09.750
5392
2015-01-30T01:05:42.273
2015-01-30T01:05:42.273
7847
7847
5270
answer


因みに、OCamlにはファンクターという高階多相性機構があるので、camlspotterの解答もそれを使って一般化できます。

[code]

    module type Lang = sig
      type 'a expr
      type reval = { f : 'a. 'a expr -> 'a }
      val open_eval : reval -> 'a expr -> 'a
    end
    
    module Fix (L : Lang) = struct
      let rec eval : 'a. 'a L.expr -> 'a =
        fun x -> L.open_eval {L.f = eval} x
    end
    
    module Plus' = Fix (struct include Lang include Plus end)
    
[/code]

前の解答に比べてのメリットは、この Lang.expr だけではなく、任意の eval 関数を持った型に対して使えることです。


CC BY-SA 3.0
2015-01-27T03:52:36.193
5397
2015-01-27T03:52:36.193
7847
5270
answer