* Re: [Caml-list] design problem
2006-11-01 5:40 design problem Pietro Abate
@ 2006-11-01 6:53 ` Jacques Garrigue
0 siblings, 0 replies; 2+ messages in thread
From: Jacques Garrigue @ 2006-11-01 6:53 UTC (permalink / raw)
To: Pietro.Abate; +Cc: caml-list
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
^ permalink raw reply [flat|nested] 2+ messages in thread