Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es

Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es

[Krishnaswami, Neel]

Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote:
> Neel Krishnaswami wrote:
> 
> > There's no recursion in the module system because that would break
> > the termination guarantee. If you think of modules as records, and
> > functors as lambda abstractions, you can see that the module system
> > defines a simply-typed lambda calculus. As you've noticed with C++, 
> > adding recursion to it would mean you can write nonterminating module
> > expressions. (All this is wonderfully clearly explained in 
> > the paper, "A modular  module system".)
> 
> I'm not sure about "simply-typed". Did the situation change since
> that of http://caml.inria.fr/archives/199907/msg00027.html ?

Wow! I didn't even know that was possible. I thought that typechecking
record subtyping was decidable...?

--
Neel Krishnaswami
neelk@cswcasa.com
-------------------
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] Polymorphic Variants and Number Parameterized Types

[Andreas Rossberg]

"Krishnaswami, Neel" wrote:
> 
> Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote:
> > Neel Krishnaswami wrote:
> >
> > > There's no recursion in the module system because that would break
> > > the termination guarantee. If you think of modules as records, and
> > > functors as lambda abstractions, you can see that the module system
> > > defines a simply-typed lambda calculus. As you've noticed with C++,
> > > adding recursion to it would mean you can write nonterminating module
> > > expressions. (All this is wonderfully clearly explained in
> > > the paper, "A modular  module system".)
> >
> > I'm not sure about "simply-typed". Did the situation change since
> > that of http://caml.inria.fr/archives/199907/msg00027.html ?
> 
> Wow! I didn't even know that was possible. I thought that typechecking
> record subtyping was decidable...?

Well, module types are (a limited form of) dependent types. What
concretely triggers undecidability of subtyping in OCaml is the presence
of abstract module types, at least in combination with the
contravariance of higher-order functors.

Note that Russo showed [1] that you can actually get rid of dependent
typing and interpret ML modules (without nested signatures) as a lambda
calculus with higher-order polymorphism (i.e., definitely not
simply-typed). The basic idea is to view functors as functions
polymorphic over their type arguments. In this setting, adding abstract
signatures would at least require adding polymorphic kinds, I believe.

[1]

@inproceedings{Russo:NonDependentTypes,
  author	= "Claudio Russo",
  title		= "Non-Dependent Types for {Standard} {ML} Modules",
  booktitle	= "International Conference on Principles and
                   Practice of Declarative Programming",
  address	= "Paris, France",
  year		= 1999,
  month		= sep,
}

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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] Polymorphic Variants and Number Parameterized Types

[Francois Pottier]

Hi,

> Note that Russo showed [1] that you can actually get rid of dependent
> typing and interpret ML modules (without nested signatures) as a lambda
> calculus with higher-order polymorphism (i.e., definitely not
> simply-typed). The basic idea is to view functors as functions
> polymorphic over their type arguments.

This interesting idea was also developed by Mark Jones:

  @InProceedings{jones-96,
    author       = "Mark P. Jones",
    title        = "Using Parameterized Signatures to Express Modular
		   Structure",
    booktitle    = "Proceedings of the 23rd {ACM} Symposium on Principles
		   of Programming Languages",
    publisher    = "ACM Press",
    month        = jan,
    year         = "1996",
    address      = "St. Petersburg Beach, Florida",
    note         = "\url{http://www.cse.ogi.edu/~mpj/pubs/paramsig.html}",
  }

as well as (in a couple of much more technical papers) by Zhong Shao.

> In this setting, adding abstract signatures would at least require adding
> polymorphic kinds, I believe.

What do you mean? In this encoding, modules are only records, so module types
are ordinary types, and there is no distinction between ordinary abstract
types (introduced by explicit polymorphic abstraction) and ``abstract
signatures''. There is, as far as I can tell, no need for kind polymorphism.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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] Polymorphic Variants and Number Parameterized Types

[Andreas Rossberg]

Hi François,

> > Note that Russo showed [1] that you can actually get rid of dependent
> > typing and interpret ML modules (without nested signatures) as a lambda
> > calculus with higher-order polymorphism (i.e., definitely not
> > simply-typed). The basic idea is to view functors as functions
> > polymorphic over their type arguments.
> 
> This interesting idea was also developed by Mark Jones:

IIRC, he does not consider generative functors, though.

> > In this setting, adding abstract signatures would at least require adding
> > polymorphic kinds, I believe.
> 
> What do you mean? In this encoding, modules are only records, so module types
> are ordinary types, and there is no distinction between ordinary abstract
> types (introduced by explicit polymorphic abstraction) and ``abstract
> signatures''. There is, as far as I can tell, no need for kind polymorphism.

Well, if you have a functor like

	F : functor(X : sig module type S  module Y:S end) -> ...

then it would be polymorphic in an unknown number of types. To capture
this, you had to make the functor polymorphic in the kind carrying the
record of abstract types bound in S (i.e. you would also need record
kinds). Something along the lines of:

	F : forall k. forall S:*. forall ts:k. {Y:S} -> ...

The application

	F (struct module type S = sig type t type u val x : t end 
	          module Y = struct type t = int
	                            type u = bool
	                            val x = 7 end
	   end)

corresponds to something like

	F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}}

I'm being sketchy here, of course, since I haven't thought about it in
real depth. It probably gets even messier when you go higher-order:
consider signatures projected from an applicative functor, for example.
In that case you might even need quantifiers on the kind level to encode
it. Also, the kind k should be restricted to record kinds, so you want
some subkinding discipline (or row polymorphism on the kind level? ;-).

Well, and somewhere in that mess we must have taken the step into the
realms of undecidable subtyping (because if it encodes OCaml modules it
must be undecidable).

Cheers,

	- Andreas
-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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] Polymorphic Variants and Number Parameterized Types

[Francois Pottier]

Hi Andreas,

On Mon, Apr 29, 2002 at 06:48:11PM +0200, Andreas Rossberg wrote:
> 
> Well, if you have a functor like
> 
> 	F : functor(X : sig module type S  module Y:S end) -> ...
> 
> then it would be polymorphic in an unknown number of types.

Perhaps our views differ. What I gathered from Jones' and Russo's
papers was that modules do not contain types. So, the module type
S cannot be a component of X; rather, the type of the functor F
will be universally quantified over S. This leads me to something
like:

  F : forall S. functor (X : S) -> ...

where the distinction between X and Y is eliminated, because it
becomes superfluous. In fact, the `functor' syntax and the name
X are just sugar, since a functor is a function. So I would really
write

  F : forall S. S -> ...

> The application
> 
> 	F (struct module type S = sig type t type u val x : t end 
> 	          module Y = struct type t = int
> 	                            type u = bool
> 	                            val x = 7 end
> 	   end)
> 
> corresponds to something like
> 
> 	F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}}

I would simply apply

  F { x : int } { x = 7 }

or, perhaps (if abstraction is desired)

  F (exists t,u.{ x : t }) (pack { x = 7 } as exists t,u.{ x : t })

So, in this example, we seem to need neither higher kinds nor
kind polymorphism. But perhaps my encoding doesn't have the
features you'd wish?

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

[Caml-list] Modules and typing

[John Max Skaller]

.. I ask a dumb question, and some very interesting stuff
I don't understand is exchanged

So here's another one :-)

Previously, I saw a reference to a paper, but I've lost it, and it may
be relevant to me. In Ocaml, a type in a module

   type t = int (* for example *)

can be hidden by binding a type in a signature

  type t

to it. That works, it seems to me, because all types have the same
size (usually a pointer) so the abstract type has enough information
for the code generator to do the right thing.

If one is using expanded types, the basic type system is inadequate,
somehow the concrete type has to be 'attached' to the abstract one,
so that the type checker uses the abstract one, and the code
generator the concrete one, and manipulations in between preserve
the link. In the Felix type system, I have such a type combinator,
and functions to extract the two parts...

Unfortunately, I don't have a proper calculus for dealing with
these type pairs. I seem to recall someone mentioned a paper
in which types were considered as functors (??) for just this purpose,
and some calculus developed. Does anyone recall the mention
of the paper or happen to have a URL for it?

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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

[Caml-list] Encoding "abstract" signatures

[Andreas Rossberg]

Francois Pottier <francois.pottier@inria.fr> wrote:
>
> On Mon, Apr 29, 2002 at 06:48:11PM +0200, Andreas Rossberg wrote:
> >
> > Well, if you have a functor like
> >
> >  F : functor(X : sig module type S  module Y:S end) -> ...
> >
> > then it would be polymorphic in an unknown number of types.
>
> Perhaps our views differ. What I gathered from Jones' and Russo's
> papers was that modules do not contain types.

Yes. But Russo describes how you can encode ML module types in such a
setting (Jones was not interested in that, AFAIR). As long as you don't have
nested signatures you can recover the full expressiveness of functors
(including generativity) by just using universal and existential
quantification.

(For other readers: the module type

    functor(X : sig type t val x : t end) -> sig type u val y : u end

can be encoded as

    forall t. {x:t} -> exists u. {y:u}

Well, with OCaml's applicative functors you had to lift the existential
quantifier, but you get the idea.)

What I was saying is that this encoding does not easily extend to the full
OCaml module system, because abstract signatures pose a problem: the number
of quantifiers you have to generate in the encoding is not fixed. I
reckonned some more complex kind system and kind polymorphism might enable
you to recover their expressiveness. But I am not at all sure (see below).

> So, the module type
> S cannot be a component of X; rather, the type of the functor F
> will be universally quantified over S. This leads me to something
> like:
>
>   F : forall S. functor (X : S) -> ...
>
> where the distinction between X and Y is eliminated, because it
> becomes superfluous. In fact, the `functor' syntax and the name
> X are just sugar, since a functor is a function. So I would really
> write
>
>   F : forall S. S -> ...
>
> > The application
> >
> >  F (struct module type S = sig type t type u val x : t end
> >            module Y = struct type t = int
> >                              type u = bool
> >                              val x = 7 end
> >     end)
> >
> > corresponds to something like
> >
> >  F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}}
>
> I would simply apply
>
>   F { x : int } { x = 7 }
>
> or, perhaps (if abstraction is desired)
>
>   F (exists t,u.{ x : t }) (pack { x = 7 } as exists t,u.{ x : t })
>
> So, in this example, we seem to need neither higher kinds nor
> kind polymorphism. But perhaps my encoding doesn't have the
> features you'd wish?

How do you express

    functor F (X : sig module type T end) (Y : X.T) = (Y : X.T)

without parameterizing over the set of existentially quantified variables
somehow? I had in mind something like (again assuming non-applicative
functors, because they are much simpler):

    LAMBDA k. Lambda S:(k->*). Lambda ts:k. lambda Y:S(ts).
        pack Y as exists ts:k.S(ts)

(Oops, I got the kind of S wrong in my previous posting).

But as I said I did not think about it much, so I have no idea whether this
really scales. In particular, when you nest signatures you might hit the
same problem of an unfixed number of quantifiers, but for kinds. In fact, I
am pretty certain it does not fly, because nested signatures essentially
give you Type:Type, i.e. you'd most likely need an infinite hierarchy of
universes...

    - Andreas
-------------------
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] Modules and typing

[Francois Pottier]

Hi,

On Tue, Apr 30, 2002 at 08:04:49PM +1000, John Max Skaller wrote:

> That works, it seems to me, because all types have the same
> size (usually a pointer) so the abstract type has enough information
> for the code generator to do the right thing.

This is correct. This problem arises not only with abstract types, but more
generally, in any programming language that has polymorphism. The most common
solutions to the data representation issue are

 + adopt a uniform representation (e.g. everything-is-a-pointer), as in O'Caml

 + require that abstract types are pointer types, as in Modula-3 (?) and, more
   recently, Cyclone

 + pass type information around at runtime, as in the TIL/ML compiler

 + adopt two representations, a uniform (boxed) one and a specialized (unboxed)
   ones, and insert coercions in your code to switch between the two, as in one
   of Xavier Leroy's papers

 + adopt specialized representations only, duplicating polymorphic functions
   if they have to be used at several types whose representations differ

As far as I can tell, you are interested in exploring the last option.
Then, you essentially need to annotate type variables (and abstract types)
with a kind, that is, with enough information to determine its concrete
representation. A kind could be, for instance, a size (e.g. 1 or 2 words)
and a register type (integer or floating-point). Then, code that depends
on a type variable (or on an abstract type) can be compiled, provided its
kind is known. In the case of abstract types, the kind would probably need
to be mentioned in a module's interface.

In the case of polymorphic functions, it is possible to perform kind
specialization automatically, that is, a function such as

  let f x = x

can be first given a kind- and type-polymorphic specification:

  val f: forall k. forall 'a : k. 'a -> 'a

then specialized for several kinds k1, k2, etc.

  val f1 : forall 'a : k1 -> 'a
  val f2 : forall 'a : k2 -> 'a

Each of these functions can then be compiled, since the kind of 'a
determines the calling conventions for the function (e.g. which
register the parameter x is found in).

I am aware that I am not directly answering your question, but I hope
these ideas help. It seems that it's easier to reason in terms of kinds
than in terms of (abstract type, concrete type) pairs -- indeed, the
whole point of abstraction is that the concrete type is usually not
known, unless you're doing whole-program compilation.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

[Caml-list] Re: Encoding "abstract" signatures

[Francois Pottier]

Andreas,

On Tue, Apr 30, 2002 at 12:34:26PM +0200, Andreas Rossberg wrote:
> 
> How do you express
> 
>     functor F (X : sig module type T end) (Y : X.T) = (Y : X.T)
> 
> without parameterizing over the set of existentially quantified variables
> somehow? I had in mind something like (again assuming non-applicative
> functors, because they are much simpler):
> 
>     LAMBDA k. Lambda S:(k->*). Lambda ts:k. lambda Y:S(ts).
>         pack Y as exists ts:k.S(ts)

You make the functor F polymorphic in the number of type components
defined by the signature S. As far as I understand, this is made
necessary by the desire to hide these types in the functor's result
(i.e. the pack operation).

It seems to me that it is simpler to suppress the pack operation,
i.e. to return Y instead of (pack Y as ...). Then, instead of
quantifying separately over S and ts, you only need to quantify
over S(ts), that is, T, as follows:

  val F : forall T. T -> T

I must say I don't know exactly what is lost with this simplification;
is there a loss of abstraction? The answer isn't obvious to me. But it
seems to offer a simple understanding of the above O'Caml specification.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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] Modules and typing

[John Max Skaller]

Francois Pottier wrote

>
>This is correct. This problem arises not only with abstract types, but more
>generally, in any programming language that has polymorphism. The most common
>solutions to the data representation issue are
>
> + adopt a uniform representation (e.g. everything-is-a-pointer), as in O'Caml
>
> + require that abstract types are pointer types, as in Modula-3 (?) and, more
>   recently, Cyclone
>
> + pass type information around at runtime, as in the TIL/ML compiler
>
> + adopt two representations, a uniform (boxed) one and a specialized (unboxed)
>   ones, and insert coercions in your code to switch between the two, as in one
>   of Xavier Leroy's papers
>
> + adopt specialized representations only, duplicating polymorphic functions
>   if they have to be used at several types whose representations differ
>
>As far as I can tell, you are interested in exploring the last option.
>
Yes. More precisely, in finding a hybrid system which permits
superior performance without losing too much generality.
I support pointers, so it should be possible
for a single specialisation of a polymorphic function
to be use where all the type variable are under a pointer.

I currently expand products, but sum types use tagged pointers.
And as you might guess from previous postings .. I have a problem
with type recursion where the term under the fixpoint binder
is a product (since that may lead to an infinitely large data structure).
The equi-recursive (tree) model doesn't work here.

>
>Then, you essentially need to annotate type variables (and abstract types)
>with a kind, that is, with enough information to determine its concrete
>representation. A kind could be, for instance, a size (e.g. 1 or 2 words)
>and a register type (integer or floating-point). 
>
The actual model is: the kind is another type. Primitive types are
annotated with the C++ type that represents them, the programmer writes:

    type int = "long";

to say that the Felix type "int" is represented by the C++ type "long".
Other kinds (in your terminology) are determined by binding
modules with signatures like:

    interface X { type t; }
    module Y { type t = int; }
    Z = Y : X;

where the "kind" of the abstract type X.t is bound to Y.t = int, and the 
type
system carries the annotation so that the type of Z.t is (Y.t, int).
I have two functions:

    lift (x,y) |-> x
    drop (x,y) |-> y

The difficulty is I need a calculus. For example:

    (x,y) -> (a,b)  reduces to  (x->a, y->b)

In other words, I need to know how to carry the kind annotations around
during reductions on the types: this is simplified, since the annotations
themselves are types .. (at least, I hope that simplifies it).

>Then, code that depends
>on a type variable (or on an abstract type) can be compiled, provided its
>kind is known. In the case of abstract types, the kind would probably need
>to be mentioned in a module's interface.
>
In the current model, as illustrated above, modules don't have interfaces
per se: instead, you have to bind an interface to a module, and *that*
creates the type/kind pair.

>
>I am aware that I am not directly answering your question,
>
heh .. a complete answer would require you to write the
code for me  .. I'm looking for a way to manage the problem ..

> but I hope
>these ideas help. It seems that it's easier to reason in terms of kinds
>than in terms of (abstract type, concrete type) pairs -- indeed, the
>whole point of abstraction is that the concrete type is usually not
>known, unless you're doing whole-program compilation.
>
Yes. Because I use types for kinds, I think I have been confusing
them: that representation is useful, since the same calculus can be
used for both, but it confuses reasoning, and your model provides
a way to decouple them.

My situation is even more confused because Iintroduced
modules after the basic system was already running, and so there
are terms for both plain and annotated types, and the code
handles all the combinations separately .. I should remove
plain type terms, and annotate them all.. but I don't want
to break working code, so I need to be sure the operations
on annotated types are right first ... which I'm not, because
I don't yet have a coherent theory. Anyhow thanks!

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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] Modules and typing

[Noel Welsh]

--- John Max Skaller <skaller@ozemail.com.au> wrote:
> Francois Pottier wrote
> 
> > + adopt specialized representations only,
> duplicating polymorphic functions
> >   if they have to be used at several types whose
> representations differ
> >
> >As far as I can tell, you are interested in
> exploring the last option.
> >
> Yes.

I believe MLTon does this, at the cost of no separate
compilation.

Noel

__________________________________________________
Do You Yahoo!?
Yahoo! Health - your guide to health and wellness
http://health.yahoo.com
-------------------
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] Re: Encoding "abstract" signatures

[Andreas Rossberg]

François,

Francois Pottier <francois.pottier@inria.fr> wrote:
>
> > How do you express
> >
> >     functor F (X : sig module type T end) (Y : X.T) = (Y : X.T)
> >
> > without parameterizing over the set of existentially quantified
variables
> > somehow? I had in mind something like (again assuming non-applicative
> > functors, because they are much simpler):
> >
> >     LAMBDA k. Lambda S:(k->*). Lambda ts:k. lambda Y:S(ts).
> >         pack Y as exists ts:k.S(ts)
>
> You make the functor F polymorphic in the number of type components
> defined by the signature S. As far as I understand, this is made
> necessary by the desire to hide these types in the functor's result
> (i.e. the pack operation).

This is just one reason. More generally, it's the need for a coherent
encoding in the higher-order setting we face. If we say that type

    functor(X : sig type t val x : t end) -> ...

maps to something like

    forall t. t -> ...

then consequently

    functor(Y : sig module type T end) -> ... -> functor(X : Y.T) -> ...

must map to some type that yields the above as the result of some sequence
of applications. We need to be polymorphic in the form of the quantification
to achieve that. So even by ignoring type abstraction you cannot avoid the
problem.

But if you replace "type" by "module type" in the above argument signature
you see why there actually cannot be an encoding with the desired
properties: the encoding of the latter type also had to contain quantifiers
for all potential *kind arguments* induced by applying an argument with
nested signatures. There is no fixed point for the level of abstractions we
had to do, unless we allowed for dependent types at some level.

> I must say I don't know exactly what is lost with this simplification;
> is there a loss of abstraction? The answer isn't obvious to me.

Well, besides the aforementioned problems, you don't represent type
abstraction at all (which, I would argue, is a central feature) - the
functor in question would not differ from

    functor F (X : sig module type T end) (Y : X.T) = Y

Or was your question about abstraction in some other sense?

    - Andreas
-------------------
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] Modules and typing

[Francois Pottier]

Hello,

Noel Welsh wrote:

> > adopt specialized representations only,
> > duplicating polymorphic functions
> > if they have to be used at several types whose
> > representations differ
> 
> I believe MLTon does this, at the cost of no separate
> compilation.

MLton does a bit more than that, really. It specializes *all* polymorphic
code, so that, after the transformation, the program can be typed in a
monomorphic type discipline. My suggestion, on the other hand, was to
duplicate polymorphic code only on a ``per-kind'' basis; for instance, if
all product types are of kind POINTER and (unboxed) integers are of kind
INT, then a polymorphic function (say, the identity) that is used at types
(say) int * int, float * float and int would only be compiled twice. I
believe this would severely limit the ``code size explosion'' problem
that is sometimes feared when doing monomorphization.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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] Re: Encoding "abstract" signatures

[Francois Pottier]

On Wed, May 01, 2002 at 03:19:29PM +0200, Andreas Rossberg wrote:
> 
> This is just one reason. More generally, it's the need for a coherent
> encoding in the higher-order setting we face. If we say that type
> 
>     functor(X : sig type t val x : t end) -> ...
> 
> maps to something like
> 
>     forall t. t -> ...
> 
> then consequently
> 
>     functor(Y : sig module type T end) -> functor(X : Y.T) -> ...
> 
> must map to some type that yields the above as the result of some sequence
> of applications.

Oh, I see what you mean. It's a good point. But still I think I can encode
the second functor as

      forall T. () -> T -> ...

(where (), the empty structure type, corresponds to Y and T corresponds to X)
which, when applied to an empty structure, yields

     forall T. T -> ...

as expected (provided the ``forall'' quantifier doesn't get in the way of
application, i.e. polymorphic instantiation and abstraction are transparent,
as in ML).

> Well, besides the aforementioned problems, you don't represent type
> abstraction at all (which, I would argue, is a central feature) - the
> functor in question would not differ from
> 
>     functor F (X : sig module type T end) (Y : X.T) = Y

Indeed it wouldn't. But I fail to see the point; if Y's type is X.T,
there is no difference between Y and (Y : X.T), is there? The two
functors in question have the same type in O'Caml.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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] Re: Encoding "abstract" signatures

[Andreas Rossberg]

Hi François,

Francois Pottier wrote:
> 
> > This is just one reason. More generally, it's the need for a coherent
> > encoding in the higher-order setting we face. If we say that type
> >
> >     functor(X : sig type t val x : t end) -> ...
> >
> > maps to something like
> >
> >     forall t. t -> ...
> >
> > then consequently
> >
> >     functor(Y : sig module type T end) -> functor(X : Y.T) -> ...
> >
> > must map to some type that yields the above as the result of some sequence
> > of applications.
> 
> Oh, I see what you mean. It's a good point. But still I think I can encode
> the second functor as
> 
>       forall T. () -> T -> ...
> 
> (where (), the empty structure type, corresponds to Y and T corresponds to X)
> which, when applied to an empty structure, yields
> 
>      forall T. T -> ...
> 
> as expected (provided the ``forall'' quantifier doesn't get in the way of
> application, i.e. polymorphic instantiation and abstraction are transparent,
> as in ML).

OK, consider applying

	module type T = sig type t type u val x : t * u end

Then, in the encoding, application should yield the result type

	forall t,u. t * u -> ...

So you cannot simply `reuse' T's quantifier. Also note that in general
the quantifier(s) in question might be buried deep inside the RHS of the
arrow, even in contravariant position. (Moreover, it is not obvious to
me whether we could use implicit type application, because polymorphism
is first-class (a field or argument of functor type would be
polymorphic)).

> > functor in question would not differ from
> >
> >     functor F (X : sig module type T end) (Y : X.T) = Y
> 
> Indeed it wouldn't. But I fail to see the point; if Y's type is X.T,
> there is no difference between Y and (Y : X.T), is there? The two
> functors in question have the same type in O'Caml.

Ah, yes, you are right, I forgot about that. Actually, I see that as an
unfortunate limitation of OCaml's module typing: it has to forget some
sharing because it lacks proper singleton types (and thus loses
principality). Ideally, the type of the above variant of F should be

	functor(X : sig module type T end) -> functor(Y : X.T) -> that Y

where I write "that Y" for the singleton type inhabited by Y only (a
subtype of X.T). That functor is essentially the polymorphic identity
functor, while the other variation was a polymorphic eta-expansion of
the abstraction operator.

But in fact, what that means is that in OCaml both functors must be
represented by a type with an existential quantifier. Otherwise you
would not witness any difference between module expressions

	M

and

	F (struct module type T = ABSTRACT_SIG_OF_M end) (M)

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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] Re: Encoding "abstract" signatures

[Francois Pottier]

Andreas,

> So you cannot simply `reuse' T's quantifier.

You're right -- it seems difficult to obtain a compositional encoding of
O'Caml's module system. We would need, in the target system, one universal
quantification over a type of record kind to be somehow equivalent to a series
of universal quantifications over types of base kind. I guess that's what you
were saying from the very start, but it took me a while to see the problem.
It would be interesting to devise a type system that has this property. Didier
Rémy noticed the need for such a feature back in 1994 when writing `Dynamic
typing in polymorphic languages' (see section 4.2 of the SRC tech report). I
don't think he has a polished solution, though.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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] Re: Encoding "abstract" signatures

[Andreas Rossberg]

François,

> It would be interesting to devise a type system that has this property. Didier
> Rémy noticed the need for such a feature back in 1994 when writing `Dynamic
> typing in polymorphic languages' (see section 4.2 of the SRC tech report).

Ah, indeed, he is discussing something quite similar. Interesting.

But I strongly suspect that even a system like that wouldn't be enough
to encode OCaml's modules. Consider that higher-order type again:

    functor(Y : sig module type T end) -> functor(X : Y.T) -> ...

The idea was representing this as

    Forall k. forall T:(k->*). forall ts:k. T(ts) -> ...  (*)

But that is still not good enough, because we might apply

    T = sig module type U module type V end

The result had to be something like

    Forall k1. Forall k2. forall U:(k1->*). forall V:(k2->*). ...

so (*) is not an appropriate encoding -- application may also result in
an indefinite number of kind quantifiers. We might try to tackle that by
introducing another universe of "hyperkinds" and repeat the same trick.
But unfortunately, that just pushes the problem to yet another level --
no finite number of additional universes will help, because what OCaml
provides with nested abstract signatures is essentially Type:Type.

So I conjecture that it is impossible to faithfully encode OCaml's
modules into a non-dependent system (which comes to no surprise taking
into account that it is known to be undecidable).

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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] Polymorphic Variants and Number Parameterized Types

[Brian Rogoff]

On Mon, 29 Apr 2002 Nadji.Gauthier@lip6.fr wrote:
> > use variants. Also, I'm willing to bet that you uncovered a bug in the
> > type checker (with the "variables can't be generalized" only when in
> > the compiler). Have you filed a bug report yet?
>
> I haven't. And since I don't fully understand PV typing,
> I prefer not to bother the developers (I fear the
> "this is a feature not a bug" reply :))

Sure, but it is also possible you found a problem and we all could benefit
from its removal.

> But I understand that there may be error when source
> is compiled when there aren't in the interpreter, ex:
>   let x = ref []
> When compiled, this gives :
>   The type of this expression, '_a list ref,
>   contains type variables that cannot be generalized
> And this is perfectly fair (think of 2 different modules
> accessing x, there may be a type clash).

That's right.

> I think the same thing happenned
> in my previous mail but I haven't managed to isolate the problem yet.

I played a bit with your example, and while I haven't isolated the
problem, I found that there is no problem with the reported expression.
The problem only happened when the f_ngt5 (or whatever you called it)
was included and disappeared when it was removed. So it seems like a
genuine bug.

-- Brian
-------------------
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] Polymorphic Variants and Number Parameterized Types

[Nadji.Gauthier]

> use variants. Also, I'm willing to bet that you uncovered a bug in the   
> type checker (with the "variables can't be generalized" only when in     
> the compiler). Have you filed a bug report yet?

I haven't. And since I don't fully understand PV typing,
I prefer not to bother the developers (I fear the
"this is a feature not a bug" reply :))
But I understand that there may be error when source
is compiled when there aren't in the interpreter, ex:
  let x = ref []
When compiled, this gives :
  The type of this expression, '_a list ref,
  contains type variables that cannot be generalized
And this is perfectly fair (think of 2 different modules
accessing x, there may be a type clash).
I think the same thing happenned
in my previous mail but I haven't managed to isolate the problem yet.

Nadji
-------------------
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] Polymorphic Variants and Number Parameterized Types

[John Max Skaller]

Brian Rogoff wrote:

>> Of course, C++ is ahead here, it already admits generics parameterised
>>by both types and integers ..  <Ducks for cover ... >
>>
>
>I don't think C++ or Ada generics (which also parameterize over values)
>help you much there. Besides, ML uses the module system to parameterize
>over values.
>
Yeah, you're right.  Although, there aren't many types that can use that 
information.
(No fixed lenth arrays for example).

Hmmm... beginnners question on module system .. can you recurse on it?
I'm guessing not, since there are neither specialisations nor overloading,
there's be no way to stop the recursion. ..??

[In C++, you can recurse on an integer parameter, using a 
specialisation/overload
to terminate the recursion... its a turing complete functional programming
language .. slightly messy though :]

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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] Polymorphic Variants and Number Parameterized Types

[Brian Rogoff]

On Sat, 27 Apr 2002, John Max Skaller wrote:
> Nadji.Gauthier@lip6.fr wrote:
>
> >*disclaimer*
> >This is a long mail, that probably only polymorphic
> >variant adepts and static typing fanatics (like me) will like.
> >Moreover I strongly doubt that it could be very useful.
> >*end of disclaimer*

Nice tricks Nadji! I didn't have time to try out everything you showed,
but I think that trick is more powerful than the other one, which doesn't
use variants. Also, I'm willing to bet that you uncovered a bug in the
type checker (with the "variables can't be generalized" only when in
the compiler). Have you filed a bug report yet?

> There is one importance of such demonstrations: they act as a proof
> that adding integer constants to the static type systems is
> 'safe and sound'.

I think if you're going to take the conclusion that all of these tricks
are worthwhile, you'll want a language with dependent types. In the
general case, you may get undecidable typing (like Cayenne, which is
very very cool) but there are also restricted systems like Xi's DeCaml
which may be useful.

>  Of course, C++ is ahead here, it already admits generics parameterised
> by both types and integers ..  <Ducks for cover ... >

It could be useful when modeling electronic components to have the
bitwidth of a component as part of a type, and to be able to say stuff
in the type system about how that width changes as we build components.
There was a neat posting in c.l.f. recently about such a trick using
(non-"standard" features of) Haskell.

I don't think C++ or Ada generics (which also parameterize over values)
help you much there. Besides, ML uses the module system to parameterize
over values.

-- Brian
-------------------
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] Polymorphic Variants and Number Parameterized Types

[John Max Skaller]

Nadji.Gauthier@lip6.fr wrote:

>*disclaimer*
>This is a long mail, that probably only polymorphic
>variant adepts and static typing fanatics (like me) will like.
>Moreover I strongly doubt that it could be very useful.
>*end of disclaimer*
>
There is one importance of such demonstrations: they act as a proof
that adding integer constants to the static type systems is
'safe and sound'.

 Of course, C++ is ahead here, it already admits generics parameterised
by both types and integers ..  <Ducks for cover ... >

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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

[Caml-list] Polymorphic Variants and Number Parameterized Types

[Nadji.Gauthier]

*disclaimer*
This is a long mail, that probably only polymorphic
variant adepts and static typing fanatics (like me) will like.
Moreover I strongly doubt that it could be very useful.
*end of disclaimer*

Hi list,

recently there was a very interesting mail about encoding 
natural numbers as types for static checking of array sizes,
list length etc..., cf
http://caml.inria.fr/archives/200109/msg00097.html

The trick was to use phantom types, and cps style to have a nice
type - number visual correspondance. For practice (and with
difficulty ...), I implemented a version with polymorphic variants,
but no cps (yet) :

module Dim : sig 
  type 'a dec

  val dec : [`U] dec
  val to_int : 'a dec -> int

  type 'a digit = 
    [`D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of 'a |
     `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ]

  val d0 : ([< 'a digit ] as 'd) dec -> [`D0 of 'd] dec
  val d1 : 'a dec -> [`D1 of 'a] dec
  val d2 : 'a dec -> [`D2 of 'a] dec
  val d3 : 'a dec -> [`D3 of 'a] dec
  val d4 : 'a dec -> [`D4 of 'a] dec
  val d5 : 'a dec -> [`D5 of 'a] dec
  val d6 : 'a dec -> [`D6 of 'a] dec
  val d7 : 'a dec -> [`D7 of 'a] dec
  val d8 : 'a dec -> [`D8 of 'a] dec
  val d9 : 'a dec -> [`D9 of 'a] dec
end = 
struct
  type 'a digit =
    [ `D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of 'a 
    | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of
'a ]
  type 'a dec = int

  let dec = 0
  let to_int x = x

  let mkd n = fun d -> d * 10 + n
  let d0, d1, d2, d3, d4, d5, d6, d7, d8, d9 =
    mkd 0, mkd 1, mkd 2, mkd 3, mkd 4, mkd 5, mkd 6, mkd 7, mkd 8, mkd 9
end

Then,

# open Dim;;
# let x120 = (d0 (d2 (d1 dec)));;
val x120 : [ `D0 of [ `D2 of [ `D1 of [ `U]]]] Dim.dec = <abstr>
# to_int x120;;
- : int = 120
# let x32 = (d2 (d3 dec));;
val x32 : [ `D2 of [ `D3 of [ `U]]] Dim.dec = <abstr>
# x120 = x32;;
         ^^^
This expression has type [ `D2 of [ `D3 of [ `U]]] Dim.dec
but is here used with type [ `D0 of [ `D2 of [ `D1 of [ `U]]]] Dim.dec

... type error :)
As you can see the number the type encodes is reversed ('cause lack of
cps).

Now it seems to me that it's a little more expressive this way.
For example, we can define a function that will only accept numbers
(or work on array size or list size) greater than zero :

# let f_nz (x:[< 'a digit ] dec) = to_int x;;
val f_nz : [< 'a Dim.digit] Dim.dec -> int = <fun>
# let x0 = dec and x1 = (d1 dec);;
val x0 : [ `U] Dim.dec = <abstr>
val x1 : [ `D1 of [ `U]] Dim.dec = <abstr>
# f_nz x1;;
- : int = 1
# f_nz x32;;
- : int = 32
# f_nz x0;;
       ^^
This expression has type [ `U] Dim.dec but is here used with type
  ([< 'b Dim.digit] as 'a) Dim.dec
Type [ `U] is not compatible with type
  'a =
    [< `D0 of 'b
     | `D1 of 'b
     | `D2 of 'b
     | `D3 of 'b
     | `D4 of 'b
     | `D5 of 'b
     | `D6 of 'b
     | `D7 of 'b
     | `D8 of 'b
     | `D9 of 'b] 

... type error again :)
But we can go further, and allow f to work only with numbers greater than
or equal to 5 for example :

# type 'a atleast5 = [ `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9
of 'a ]
and 'a atmost4 = [`D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of
'a ];;
*identical signature skipped*
# let f_atleast5 (x:[< 
		  | [< 'a digit ] atmost4 
		  | [< `U | 'a digit ] atleast5 
		  ] dec) = to_int x
*big type annotation skipped*
# f_atleast5 x32;;
- : int = 32
# f_atleast5 x120;;
- : int = 120
# f_atleast5 x1;;
Toplevel input:
# f_atleast5 x1;;
             ^^
This expression has type [ `D1 of [ `U]] Dim.dec but is here used with
type
  [< `D1 of [< 'b Dim.digit] as 'a] Dim.dec
*rest of big type error skipped*

... type error again, yeah :)
The idea is to encode (in the function signature) some kind of
deterministic finite automaton from the last digit of the number, which
decides if the type is valid (= if the number is in the desired
range). You can read the type of f_atleast5 as :
- let n be the number encoded in the type of x
- if the last digit of n is <= 4, then n must be at least 2 digits long (=
we don't allow the unit `U to terminate the type) to be >= 5
- if the last digit is >= 5, n is >= 5 (= we allow anything to terminate
the type)

For fun, lets work with a parameter statically known to encode a number
greater than 25 :
# type 'a atleast2 =
    [ `D2 of 'a | `D3 of 'a | `D4 of 'a 
    | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ]
  and 'a atleast3 =
    [ `D3 of 'a | `D4 of 'a 
    | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ]
   and 'a atmost2 = [`D0 of 'a | `D1 of 'a | `D2 of 'a ]
   and 'a atmost1 = [`D0 of 'a | `D1 of 'a ];;
*identical signature skipped*
# let f_atleast25 
    (x:[< 
       | [< [< 'a digit] atmost2 | [< `U | 'b digit ] atleast3 ] atmost4
       | [< [< 'a digit] atmost1 | [< `U | 'b digit ] atleast2 ] atleast5
       ] dec) = to_int x;;
*very big type annotation skipped*
# f_atleast25 x32;;
- : int = 32
# f_atleast25 x120;;
- : int = 120
# f_atleast25 x1;;
              ^^
This expression has type [ `D1 of [ `U]] Dim.dec but is here used with
type *very big type skipped*

Again, the type of f_atleast25 may be read :
- let n be the number encoded in the type of x, 
  with last digits XYZ (that is n >= X * 100 + Y * 10 + Z). Y and Z
  must exist but X may not exist.
- if Z <= 4 then
  - if Y <= 2 then X exists <-> n >= 25
  - if Y >= 3 then true <-> n >= 25
- if Z >= 5 then
  - if Y <= 1 then X exists <-> n >= 25
  - if Y >= 2 then true <-> n >= 25
In the same way we can encode that n should be less than something,
or between something and another, or any finite disjunction and 
conjunction of intervals as the language of DFA is closed under those
operations.
The function f_atleast120_andlessthan246 is of course left as an exercice
to the masochist reader :)

Now the questions to the courageous people that are still here :
I think the function f_atleast5 and f_atleast25 are impossible
to express with the previous solution wich involved 10 different
abstract types in Dim signature, am i right ?
When I concatenate all the Ocaml code I gave (except the 
direct calls to the f_* ) in a single file
and I compile, it's fine. But when I add :

# let _ = f_atleast5 x32 
I get :
The type of this expression, [ `D2 of [ `D3 of [ `U]]] Dim.dec,
contains type variables that cannot be generalized

Can someone explain this ?

Thanks for your attention :) ,
Ocaml really is a wonderful programming language.

Bye,
Nadji

PS: If you think my mail was off-topic let me know so I won't bother you
...
PPS: Lots of people have some very nice tricks with typing, maybe
it would be a good thing to add a section somewhere in the FAQ or the doc
for those "typing pearls". These can be very useful to get an intuition
of the limits of static typing. For example, some people posted very nice
things
about dynamic typing trick (Daniel De Rauglaude I think), memo class for
objects (Jacques Garrigue I think), of course Xavier Leroy has a bunch
of them etc ...
-------------------
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