design problem

Pietro Abate
 Jacques Garrigue
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20061101 (06:56) 
From:  Jacques Garrigue <garrigue@m...> 
Subject:  Re: [Camllist] design problem 
From: Pietro Abate <Pietro.Abate@anu.edu.au> > I've the following code to write types and functions in an extensible > way, so to reuse 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 catchall cases in your patternmatchings, 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 catchall 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