Re: [Caml-list] design problem

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Pietro Abate <Pietro.Abate@anu.edu.au>

> I've the following code to write types and functions in an extensible
> way, so to re-use my code a bit. Everything seems working fine. 
> 
> I've two questions:
> - Is there a better way of achieving a similar result ? Here I'm using
>   polymorphic variants, but I'm wondering if somebody already cooked
>   something together by using variants and camlp4 extensions...

No idea, but polymorphic variants are supposed to be good at this :-)
If you like modules, you might want to try combining with private row
types and recursive modules (see the paper in publications), but
whether it helps or not depends on the size of your code.

> - At the moment type errors are pretty horrible. How can I coerce these
>   functions to give prettier errors ? I've tried to coerce the function
>   f in the *_aux functions below, but of course this is not possible as
>   it needs to be polymorphic by design ...

You can perfectly write polymorphic type annotations.
Here is your code with some annotations, which gives readable types
after inference.
Note that I removed the catch-all cases in your pattern-matchings, are
they greatly reduce the interest of using polymorphic
variants. However I had to leave one for `Not, as otherwise the
parameter would not be extensible.

I also enclose a version using private row types, which separates
positive and negative cases, so as to remove all catch-all cases.
This is more verbose, but more powerful, and all types are explicit.

Jacques Garrigue

(* my basic data type *)
type 'a termpc =
    [`And of 'a * 'a
    |`Or of 'a * 'a
    |`Not of 'a
    |`Atom of string
    ]
;;

(* a simple normal form function *)
let nnfpc_aux f : [> 'a termpc] termpc -> 'a = function
  |`Not ( `Not x   )  -> f x
  |`Not ( `And(x,y) ) -> `Or  (f (`Not x), f (`Not y) )
  |`Not ( `Or (x,y) ) -> `And (f (`Not x), f (`Not y) )
  |`And (x,y)         -> `And (f x, f y)
  |`Or  (x,y)         -> `Or  (f x, f y)
  |`Not ( `Atom _) as x -> x
  |`Atom _ as x -> x
  |`Not _ -> failwith "impossible pc"

;;

let rec nnfpc t = nnfpc_aux nnfpc t;;

(* extension of the basic data type *)
type 'a termk =
    [`Dia of 'a
    |`Box of 'a
    |'a termpc
    ]
;;

let nnfk_aux f : [> 'a termk] termk -> 'a = function
  |`Not (`Dia x ) -> `Box (f (`Not x))
  |`Not (`Box x ) -> `Dia (f (`Not x))
  |`Dia x         -> `Dia (f x)
  |`Box x         -> `Box (f x)
  |#termpc as x -> nnfpc_aux f x
;;

let rec nnfk t = nnfk_aux nnfk t;;

(* an other extension on top of termk *)
type 'a termlck =
    [`CDia of 'a
    |`CBox of 'a
    |'a termk
    ]
;;

let rec nnflck_aux f : [> 'a termlck] termlck -> 'a = function
  |`Not (`CDia x ) -> `CBox (f (`Not x))
  |`Not (`CBox x ) -> `CDia (f (`Not x))
  |`CDia x         -> `CDia (f x)
  |`CBox x         -> `CBox (f x)
  |#termk as x -> nnfk_aux f x
;;

let rec nnflck t = nnflck_aux nnflck t;;

let a = `Not (`Not (`Not (`Dia (`CDia (`Atom "a")))));;
let b = nnflck a;;


(* Alternative version using private row types *)
module type T = sig
  type term
  val nnf : term -> term
  val nnf_not : term -> term
end

module Fpc(X : T with type term = private [> 'a termpc] as 'a) =
  struct
    type term = X.term termpc
    let nnf : term -> _ = function
      |`Not(`Atom _) as x -> x
      |`Not x     -> X.nnf_not x
      |`And (x,y) -> `And (X.nnf x, X.nnf y)
      |`Or  (x,y) -> `Or  (X.nnf x, X.nnf y)
      |`Atom _ as x -> x
    let nnf_not : term -> _ = function
      |`Not x    -> X.nnf x
      |`And(x,y) -> `Or  (X.nnf_not x, X.nnf_not y)
      |`Or (x,y) -> `And (X.nnf_not x, X.nnf_not y)
      |`Atom _ as x -> `Not x
  end

module rec Pc : T with type term = Pc.term termpc = Fpc(Pc)

module Fk(X : T with type term = private [> 'a termk] as 'a) =
  struct
    type term = X.term termk
    module Pc = Fpc(X)
    let nnf : term -> _ = function
      |`Dia x -> `Dia (X.nnf x)
      |`Box x -> `Box (X.nnf x)
      |#termpc as x -> Pc.nnf x
    let nnf_not : term -> _ = function
      |`Dia x -> `Box (X.nnf_not x)
      |`Box x -> `Dia (X.nnf_not x)
      |#termpc as x -> Pc.nnf_not x
  end

module rec K : T with type term = K.term termk = Fk(K)

module Flck(X : T with type term = private [> 'a termlck] as 'a) =
  struct
    type term = X.term termlck
    module K = Fk(X)
    let nnf_not : term -> _ = function
      |`CDia x -> `CBox (X.nnf_not x)
      |`CBox x -> `CDia (X.nnf_not x)
      |#termk as x -> K.nnf_not x
    let nnf : term -> _ = function
      |`CDia x -> `CDia (X.nnf x)
      |`CBox x -> `CBox (X.nnf x)
      |#termk as x -> K.nnf x
  end

module rec Lck : T with type term = Lck.term termlck = Flck(Lck)

let b = Lck.nnf a