[Caml-list] Polymorphic recursion

["Lukasz Stafiniak" <l_stafiniak@hoga.pl>]

[-- Attachment #1: Type: text/plain, Size: 1650 bytes --]

Hi,

I have recently encountered some very interesting notions (cited below).
Although I've been using OCaml for some time, up to now I didn't know about
the existence of polymorphic records and (their reference to) the problem of
polymorphic recursion. Perhaps a word about it should be stated in the
manual (more evidently)? (I don't even recall to have seen the syntax in the
manual for this.)

With Your help I ventured again to "typecheck my programs before they are
generated" etc. But now I get an error I totally don't understand. (Still it
somehow resembles the problem it posed as an ordinary function.) Could
someone explain? I have attached the file.

Thanks in advance,
Best wishes,
Lukasz

Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>
Re: [Caml-list] Variant parameterized method?
>>>>>>>>>

This precise type is not admissible in the ocaml type system.
In ocaml recursive types must be regular: only 'a foo may occur in the
expansion of 'a foo.

This problem is discussed in an answer to PR#1730 in the caml bug
database.
This can be solved by introducing an explicit wrapper.

<<<<<<<<<

Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>
Re: [Caml-list] does class polymorphism need to be so complicated?
>>>>>>>>>

P.S. Having a lighter syntax for polymorphic methods might be a good
idea.
[...]
An advantage of such a syntax is that it could also be used in normal
"let rec" to provide polymorphic recursion.

<<<<<<<<<<




Uwaga! Do końca sierpnia przedłużyliśmy promocje, do pakietów
wielostanowiskowych dokładamy PenDrive  Sprawdź:
http://www.mks.com.pl/promocja-mobile.html

[-- Attachment #2: typedcode.ml --]
[-- Type: application/octet-stream, Size: 2621 bytes --]


(* this could be e.g.: type 'a annot = 'a code *)
type 'a annot = 'a
;;

type 'a valu =
  | Typeonly | Valu of 'a annot
  | Ord1bool of ('a, bool) ord1
  | Ord1int of ('a, int) ord1
and ('a, 'b) ord1 =
  | Ord1Red of ('b -> 'a) valu
  | Ord2bool of ('a, 'b, bool) ord2
  | Ord2int of ('a, 'b, int) ord2
and ('a, 'b, 'c) ord2 =
  | Ord2Red of ('a, 'c -> 'b) ord1
;;

type typterm =
  | Tbool of bool valu
  | Tint of int valu
;;

type 'a valu_env = {
  eValu : 'a annot list;
  eOrd1bool : ('a, bool) ord1_env option;
  eOrd1int : ('a, int) ord1_env option;
}
and ('a, 'b) ord1_env = {
  eOrd1Red : ('b -> 'a) valu_env option;
  eOrd2bool : ('a, 'b, bool) ord2_env option;
  eOrd2int : ('a, 'b, int) ord2_env option;
}
and ('a, 'b, 'c) ord2_env = {
  eOrd2Red : ('a, 'c -> 'b) ord1_env option;
}
;;

type env = {
  eBool : bool valu_env;
  eInt : int valu_env;
}
;;

type env_put_rec = {
  put_valu : 'a. 'a valu_env option -> 'a valu -> 'a valu_env;
  put_ord1 : 'a 'b. ('a, 'b) ord1_env option -> ('a, 'b) ord1 -> ('a,
  'b)ord1_env;
  put_ord2 : 'a 'b 'c. ('a, 'b, 'c) ord2_env option -> ('a, 'b, 'c)
	       ord2 -> ('a, 'b, 'c) ord2_env;
}
;;

let rec env_put = {
  put_valu =
  begin fun e ->
    let e = match e with
      | Some e -> e
      | None -> {eValu = []; eOrd1bool = None; eOrd1int = None}
    in
    function
      | Typeonly -> failwith "(Valu v) required"
      | Valu v ->
	  {e with eValu = v::e.eValu}
      | Ord1bool tv ->
	    {e with eOrd1bool = Some (env_put.put_ord1 e.eOrd1bool tv)}
      | Ord1int tv ->
	  {e with eOrd1int = Some (env_put.put_ord1 e.eOrd1int tv)}
  end;
  put_ord1 =
  begin fun e ->
    let e = match e with
      | Some e -> e
      | None -> {eOrd1Red = None; eOrd2bool = None; eOrd2int = None}
    in
    function
    | Ord1Red tv ->
	{e with eOrd1Red = Some (env_put.put_valu e.eOrd1Red tv)}
    | Ord2bool tv ->
	{e with eOrd2bool = Some (env_put.put_ord2 e.eOrd2bool tv)}
    | Ord2int tv ->
	{e with eOrd2int = Some (env_put.put_ord2 e.eOrd2int tv)}
  end;
  put_ord2 =
  begin fun e ->
    let e = match e with
      | Some e -> e
      | None -> {eOrd2Red = None}
    in
    function
    | Ord2Red tv ->
	{e with eOrd2Red = Some (env_put.put_ord1 e.eOrd2Red stages tv)}
  end;
}
;;

let env_put env =
  function
    | Tbool tv ->
	let v = env_put.put_valu env tv in
	{eBool = Some v; eInt = None}
    | Tint tv ->
	let v = env_put.put_valu env [Approx(id + env.stagevar,st)] tv in
	{eBool = None; eInt = Some v}
;;

(* similar function env_get, etc. *)