I want to create a polymorphic open recovery.

When I was writing something like an expression problem solution using the Extensible variant types introduced in OCaml 4.02, I wanted a polymorphic open recovery, but I am 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 letrec cannot be expanded. *)
  (*The reason why the eval is used as a record is because the application of the eval of the app has two different types of applications, so it had to be added. *)
  let open_eval(type a)(eval:reval)(exp:a exp):a=
    match exp with
      Numi ->i
    | App(f, x) - > eval.ff(eval.fx)
    | _->failwith "no match"
end

(*Extensions for both Lang data and functions.*)
module Plus=structure
  type'a Lang.expr+= 
      Plus: (int->int->int) Lang.expr

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

  let show —type a.a Lang.expr ->string=function
      Plus->"plus"
    | Lang.App_-> "app"
    | Lang.Num_-> "num"
    | _->"no match"
end

So far, I can compile it.However, I would like to use the fixed point operator fix to fix Plus.open_eval, but how can I write the fix implementation?
I know that the normal fixed point operator is multiplied as shown in the following article.
http://d.hatena.ne.jp/KeisukeNakano/20060926/1159273362
I may not be able to write it in the first place, but I would appreciate it if you could give me any advice.

add
By the way,

let fix(`Mx)y=y Lang.{f=funz->x(`Mx)yz}

Error: This field value has type 'b Lang.expr->'b which is less general than 'a.a Lang.expr->'a
Error when defining fix as shown in .orz

ocaml

2022-09-30 20:30

3 Answers

First of all, I will try to get a fixed point without being particular about it.

open Lang

let rec fixed =
  funx->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 ML does not take a polyphase mold inside the fixed, let, and cannot plunge into the polyphase field {f=...}.This is the same condition as your question.

If you want fixed to have a polyphase type internally, you can use the polymorphic recovery specifying the polyphase type of fixed:

open Lang
open Plus

let rec fixed: 'a.' a expr ->' a = (*<= This is the miso*)
  funx->Plus.open_eval {f=fixed}x (*Even internally, fixed has a polyphase type, so you can insert it into the reval*)

let()=
  print_int@@fixed
    (App 
       (App(Plus, App(Plus, Num21), Num21),
        App(App(Plus,Num21),Num21)))

84 appears.

so-called fixed point operator

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

open_eval must be changed to a value of ('aever->'a')->'aever->'a to enter the , but

let open_eval'=fun fx->Plus.open_eval {f=f}x (*Not working…) *)

I would like a type like open_eval': 'a.('b.'b expr->'b)->'a expr, but if I write this, I don't think it's possible because I don't need high rank multi-phase encoding with multi-phase record fields.

If you want to achieve the title of the question that you want to create a polymorphic open recovery, I think you can give up fix…

2022-09-30 20:30

Even if you can't use a regular fix, you can define a fix exclusively for open_eval.

let open_eval_wrap event={f=fun x->open_eval x}

let reval_fix (eval:reval->reval):reval=
  {f=funx->(evalf(eval_fixevalf))).fx}

let eval x=(eval_fix open_eval_wrap).fx

Is that the answer?

Also, I'm paying attention to the camlspotter's comment that it's a functional type, and there's a way to use lazy as a fixed point.This is a completely common form.

let recovery_fix(f:'a Lazy.t->'a)=
  lazy(f(lazy_fixf))

You need to change the definition a little.

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

  type reval = {f:'a.a expr->'a}
  let run(eval:reval Lazy.t) =(Lazy.force event).f

  let open_eval(type a)eval(exp:a expr):a=
    match exp with
      Numi ->i
    | App(f, x) - > run average (run average x)
    | Succ->succ
    | _->failwith "no match"

  let open_eval_wrapeval={f=funx->open_eval x}
end

This is enough to close the immovable point.

let eval x=Lang.run(lazy_fixPlus.open_eval_wrap)x

2022-09-30 20:30

By the way, OCaml has a high-rise multifunction mechanism called a functor, so you can use it to generalize your answers.

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) = structure
  let receipt: 'a.a.a L.expr->'a=
    funx->L.open_eval{L.f=eval}x
end

module Plus'= Fix (struct include Lang include Plus end)

The advantage over the previous answer is that it can be used not only for Lang.expr but also for types with arbitrary eval functions.

2022-09-30 20:30

If you have any answers or tips

Popular Tags

python x 4647

android x 1593

java x 1494

javascript x 1427

c x 927

c++ x 878

ruby-on-rails x 696

php x 692

python3 x 685

html x 656