[Caml-list] Translation between datatypes with binding

[Caml-list] Translation between datatypes with binding

[Jojgov, G.I.]

Hello,

I am relatively new to the OCAML programming, so my question may be
trivial, but did not find related messages in the list archive and I
would appreciate any tips. 

I am trying to use OCAML as a logical framework to implement two systems
with binding and to define a translation from one to the other. Ideally,
I would like to be able to write code like this


type
	expr1 =
	 SomeValue1 of int |
	 SomeBinder1 of int * (expr1 -> expr1);;
type
	expr2 = 
	 SomeValue2 of string |
	 SomeBinder2 of string * (expr2 -> expr2);;

let rec translate (term:expr1) : expr2 =
	match term with
		SomeValue1 x -> SomeValue2 (string_of_int x) |
		SomeBinder1 (x,body) -> SomeBinder2 ((string_of_int
x),(function (v:expr2) -> (translate (body v))))
;;


(this is a simplified version of the real datatypes and the translation
that I want to use)

Of course, this code is not type-correct because "(function (v:expr2) ->
(translate (body v)))" is not. If expr1 and expr2 could "behave" like
classes I could have defined a common base class, say "expr", and then
redefine the binders as

	...
	 SomeBinder1 of int * (expr -> expr1);;
	...
	 SomeBinder2 of string * (expr -> expr2);;

and then the code would be "type-correct".


My questions are: Is there a natural way to define a function like the
translation function above on datatypes? Is there another way to
implement these structures? I guess the only solution is to use classes,
but I already have some code dealing with the two concrete types and
preferably I would like to reuse the code.


Thanks in advance for your comments,

Georgi


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Translation between datatypes with binding

[Markus Mottl]

On Mon, 05 Jul 2004, Jojgov, G.I. wrote:
> I am trying to use OCAML as a logical framework to implement two systems
> with binding and to define a translation from one to the other. Ideally,
> I would like to be able to write code like this

It may be more convenient to use polymorphic variants here (see
below for example), because you can keep the code more abstract.
Another possibility would be to use type functors.  To make the latter
convenient, this would however require the use of the compiler flag
"-rectypes" so I won't go into details.

Here is my solution using polymorphic variants:

---------------------------------------------------------------------------
let rec trans trans_id inv_trans = function
  | `SomeValue id -> `SomeValue (trans_id id)
  | `SomeBinder (id, body) ->
      let trans_body v = inv_trans (body (trans trans_id inv_trans v)) in
      `SomeBinder (trans_id id, trans_body)

let rec trans_1_2 expr1 = trans string_of_int trans_2_1 expr1
and trans_2_1 expr2 = trans int_of_string trans_1_2 expr2
---------------------------------------------------------------------------

> (this is a simplified version of the real datatypes and the translation
> that I want to use)

It's not correct: you also need a conversion function from expr2 to
expr1 in order to implement translations for higher-order stuff (i.e.
functions like "body").  Objects won't help here either, because they,
too, cannot have a model for the following in the general case (you'd
always be stuck with a finite amount of translations):

  val invert : ('a -> 'b) -> ('b -> 'a)

> My questions are: Is there a natural way to define a function like the
> translation function above on datatypes? Is there another way to
> implement these structures? I guess the only solution is to use classes,
> but I already have some code dealing with the two concrete types and
> preferably I would like to reuse the code.

If you can't do something with algebraic datatypes, you won't be able
to do it with objects either.  If you are not afraid of higher-order
functions, code reuse is also easy with algebraic datatypes.

Regards,
Markus

-- 
Markus Mottl          http://www.oefai.at/~markus          markus@oefai.at

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners