Typing problem

Typing problem

[jean-marc alliot]

We recently found a quite annoying problem with the typing system in
ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other
people might be be interested however.

The problem is summarized in the following code:

First let's define two types:
type t1 = (?l:int -> unit -> unit)
type t = Toto of t1

Then the function:
let f1 g =
  g l:3 ();
  (Toto g);;

This function doesn't compile and the compiler error message is somewhat
cryptic at first sight:
File "toto.ml", line 11, characters 8-9:
This expression has type int -> unit -> 'a but is here used with type
  t1 = ?l:int -> unit -> unit

To make it compile, you have to type explicitly g with:
let f2 (g : t1) =
  g l:3 ();
  (Toto g);;

We would very much like to see this clearly documented in ocaml 2.99
reference manual, as it is a serious change in the behavior of the
typing system. Determinism is lost, as typing f1 would succeed if typing
was done in reverse order (from last line to first line).
Perhaps also a different error message from the compiler would help in
detecting such problems.


P Brisset
JM Alliot

Re: Typing problem

[Pierre Weis]

> We recently found a quite annoying problem with the typing system in
> ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other
> people might be be interested however.
> 
> The problem is summarized in the following code:
> 
> First let's define two types:
> type t1 = (?l:int -> unit -> unit)
> type t = Toto of t1
> 
> Then the function:
> let f1 g =
>   g l:3 ();
>   (Toto g);;
> 
> This function doesn't compile and the compiler error message is somewhat
> cryptic at first sight:
> File "toto.ml", line 11, characters 8-9:
> This expression has type int -> unit -> 'a but is here used with type
>   t1 = ?l:int -> unit -> unit

Thank you very much for pointing out this interesting problem: I'm
sure there is room for improvement here for our new label compiler.

If you use the -modern option of the compiler you would get a much
clearer message, namely:

# let f1 g =
    g l:3 ();
    (Toto g);;
This expression has type l:int -> unit -> 'a but is here used with
type
  t1 = ?l:int -> unit -> unit

This clearly states that the optional status of the label is involved
in the problem.

Hence, a language level fix could simply be to allow the user to write
the question mark with the label as:

let f1 g =
    g ?l:3 ();
    (Toto g);;

Now, in conjontion with the -modern option, this would be perfectly clear to
understand why g l:3 is rejected while g ?l:3 is not.

Unfortunately, this last program is not yet handled properly by the
compiler, since it causes an assertion failure into the typechecker:

# let f1 g =
      g ?l:3 ();
      (Toto g);;
This expression has type ?l:Uncaught exception: File
"typing/printtyp.ml", line 0, characters 6649-6661: Assertion failed

> We would very much like to see this clearly documented in ocaml 2.99
> reference manual, as it is a serious change in the behavior of the
> typing system. Determinism is lost, as typing f1 would succeed if typing
> was done in reverse order (from last line to first line).
> Perhaps also a different error message from the compiler would help in
> detecting such problems.

I don't think that determinism is lost, in the sense that the compiler
always output the same answers! But you're right to mention that this
would be another way to test in which order in which the type-checker
type-checks the sub-expressions of a program.

You're also right in that we always would like better and better error
messages, I would say particularly for the last program I wrote: we
would very much like the compiler not to fail to print the error
report!

No doubt that this erroneous error message will be corrected before
the experimental 2.99 version will turn into a stable 3.0 version of
Objective Caml. Also, may be Jacques could tell us what is his opinion
about the optional labels status in expressions (as in g ?l:3).

Best regards,
-- 
Pierre Weis

INRIA, Projet Cristal, http://pauillac.inria.fr/~weis

Re: Typing problem

[Jacques Garrigue]

From: Jean-Marc Alliot <alliot@recherche.ena.fr>
> We recently found a quite annoying problem with the typing system in
> ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other
> people might be be interested however.
> 
> The problem is summarized in the following code:
> 
> First let's define two types:
> type t1 = (?l:int -> unit -> unit)
> type t = Toto of t1
> 
> Then the function:
> let f1 g =
>   g l:3 ();
>   (Toto g);;
> 
> This function doesn't compile and the compiler error message is somewhat
> cryptic at first sight:
> File "toto.ml", line 11, characters 8-9:
> This expression has type int -> unit -> 'a but is here used with type
>   t1 = ?l:int -> unit -> unit
>
> We would very much like to see this clearly documented in ocaml 2.99
> reference manual, as it is a serious change in the behavior of the
> typing system. Determinism is lost, as typing f1 would succeed if typing
> was done in reverse order (from last line to first line).

Sorry, I overlooked this point the manual.

As Pierre pointed out, what is lost here is not determinism but
completeness. The compiler may fail to type some correct programs, but
when it gives a result this will always be the same type.

To be more precise, ocaml 2.99 added two features to function
application:

* out-of-order parameter passing (with labels)
* optional arguments

Both of these features require type information to be available at
application point. For the first one, this is only required for
efficient compilation, but for the second one type inference cannot be
done without it.

So you have to put a type annotation on g for the program to be
accepted.

# let f1 (g : t1) =
    g l:3 ();
    (Toto g);;
val f1 : t1 -> t = <fun>

The choice here has been to keep backwards compatibility: all programs
that do not use extended application will be typed. That is, by
default the compiler supposes that there are no optional arguments, and
that all arguments are in the right order.

As for the incompleteness problem, we have the theoretical foundation
to solve it. That is, we could modify the type system so as to refuse
the opposite order also, which is somehow wrongly accepted.

# let f1 g = ignore(Toto g); g l:3 ();;
val f1 : t1 -> unit = <fun>

But I'm not sure refusing such cases would help a lot in practice.
This is not done currently because this check would badly slow down
the compiler.

> Perhaps also a different error message from the compiler would help in
> detecting such problems.

The above error message tells almost all the compiler knows. That is,
you mixed an optional and a non-optional argument, which is
illegal. The non-optional label disappears in the printed type because
in classic mode it is irrelevant for unification. I believe the
problem was that you didn't know that such a problem may occur at all.

In this particular case, by analyzing the two incompatible types, we
may discover that they both use the label l:, in its optional an
non-optional forms. So, with quite a bit of work, we could also have a
message:

Optional label ?l: and non-optional label l: are incompatible.

But we must then also think about out-of-order application, omitted
parameters... Which all need a specific treatment.

Do you think this would help a lot?

From: Pierre Weis <Pierre.Weis@inria.fr>
> Hence, a language level fix could simply be to allow the user to write
> the question mark with the label as:
> 
> let f1 g =
>     g ?l:3 ();
>     (Toto g);;
> 
> Now, in conjontion with the -modern option, this would be perfectly clear to
> understand why g l:3 is rejected while g ?l:3 is not.
> 
> Unfortunately, this last program is not yet handled properly by the
> compiler, since it causes an assertion failure into the typechecker:
> 
> # let f1 g =
>       g ?l:3 ();
>       (Toto g);;
> This expression has type ?l:Uncaught exception: File
> "typing/printtyp.ml", line 0, characters 6649-6661: Assertion failed

In fact, this feature is already available in ocaml 2.99. However the
above program is ill-typed, and due to a hole in the type checker,
some invalid type expression makes the pretty printer crash.

With a corrected version of the compiler, you get the following error
message.
# let f1 g =
        g ?l:3 ();
             ^
        (Toto g);;  
This expression has type int but is here used with type 'a option

That is, using a question mark in an application is symmetrical to
abstraction, and you must provide an optional value (of type int
option here). This feature is documented in the reference manual.

# let f1 g =
    g ?l:(Some 3) ();
    (Toto g);;
val f1 : t1 -> t = <fun>

This only solves half of the problem, since you still have to pass all
arguments (included omitted ones), and in the right order.

Regards,

Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Thread feature missing

[Christophe Raffalli]

Have I miss something ? I found that two features (especialy the first)
are missing in the thread library:

- No way to wait for one thread to finish among many (equivalent of
join, but taking a list of threads as argument)

- No way to send a signal to a thread (it would be useful to make a
thread raise an exception from another thread).

I see clearly a solution with some periodical tests. But this is not
elegant.

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI

Re: Thread feature missing

[Gerd Stolpmann]

On Mon, 14 Feb 2000, Christophe Raffalli wrote:
>Have I miss something ? I found that two features (especialy the first)
>are missing in the thread library:
>
>- No way to wait for one thread to finish among many (equivalent of
>join, but taking a list of threads as argument)

This can be solved by a condition variable, provided that the "sub threads"
help the main thread.

let m = Mutex.create() in       (* protects c and t *)
let c = Condition.create() in
let t = ref None in             (* thread ID of the finished thread *)

Before the sub threads finish, they indicate what is happening:

Mutex.lock m;
if t = None then (              (* Signal only when the first thread finishes *)
    t := Some (Thread.self());
    Condition.signal c;
);
Mutex.unlock m;
Thread.exit();

The main thread waits until the signal comes:

Mutex.lock m;
Condition.wait c m;
(* Now it knows that thread t has finished *)
Mutex.unlock m;

>- No way to send a signal to a thread (it would be useful to make a
>thread raise an exception from another thread).

If you mean asynchronous signals: The POSIX thread API has the concept of
"cancellation-safeness". Threads are cancellation-safe if you can safely
cancel them, without leaving memory uninitialized. It is very hard to get
a thread cancellation-safe, because you must catch the "cancel" signal
in almost every function, and CLEAN MEMORY UP. 

I think this is the reason why you do not find a "kill" function in Thread
that works under the native compiler, too. (Raising exceptions is a similar
problem.) As far as I understood execution of O'Caml code is done in a 
relative protected environment; the runtime system sets up artificially that 
only one thread which currently executes O'Caml code runs at a time. It would
be simple to test on some signal if the time slice of a thread begins. The
problem are the pieces of code where this protected environment is left,
which is always done if a system call is going to be performed. As far as I
know the system calls return with an EINTR error code if the timer that
triggers the thread switch times out, and it *might* be possible to
catch this situation, too.

I would predict that the O'Caml developers refuse such a change, because
it adds much complexity to the runtime system. Furthermore, it makes it
harder to get rid of that protected environment in which O'Caml code runs
and which restricts the advantages of multi-threaded programming on 
multiprocessor systems.

Gerd
-- 
----------------------------------------------------------------------------
Gerd Stolpmann      Telefon: +49 6151 997705 (privat)
Viktoriastr. 100             
64293 Darmstadt     EMail:   Gerd.Stolpmann@darmstadt.netsurf.de (privat)
Germany                     
----------------------------------------------------------------------------

Re: Thread feature missing

[Xavier Leroy]

> Have I miss something ? I found that two features (especialy the first)
> are missing in the thread library:

No, you didn't miss anything.  The OCaml thread interface is somehow
constrained to the intersection of what can be implemented on top of
the virtual machine (for bytecode threads) and of what POSIX and Win32
threads provide (for system threads).

> - No way to wait for one thread to finish among many (equivalent of
> join, but taking a list of threads as argument)

This isn't supported directly in POSIX threads.  However, you can
easily program it yourself using e.g. events: allocate a channel, have
each thread send a message on it when it terminates, and wait for a
message on the channel.  The good thing about this method is that you
can put whatever you need in the message (thread ID, return value, etc).

> - No way to send a signal to a thread (it would be useful to make a
> thread raise an exception from another thread).

I agree this would be nice, and can easily be implemented in the case
of bytecode threads.  For POSIX threads, one could try using
cancellation to handle this, but I'm not sure it can be done in a
portable way.  For Win32 threads, I don't know how to do it.

- Xavier Leroy

Re: Thread feature missing

[Christophe Raffalli]

Xavier Leroy wrote:
> > - No way to wait for one thread to finish among many (equivalent of
> > join, but taking a list of threads as argument)
> 
> This isn't supported directly in POSIX threads.  However, you can
> easily program it yourself using e.g. events: allocate a channel, have
> each thread send a message on it when it terminates, and wait for a
> message on the channel.  The good thing about this method is that you
> can put whatever you need in the message (thread ID, return value, etc).
> 
Ok, but if I wait for thread A or B and thread C stops, then I will wake
up and test 
on the channel if it is thread A or B. This means waiting in a loop. If
there are a lot of small threads with short life ... this is not very
good.

I think it is better to have one channel for each thread and wait using
Event.select
that thread A or B send on their respective channel. Am I right ?

I have another little pb which is that Many threads may be waiting for A
to terminate. 
So I could do a loop always sending on the termination channel of A. But
is there a better way ? A kind of broadcast forever a value on a channel
?

Yet another question: What is the size of a thread in both cases:
bytecode and native.
Is 1000 threads reasonable ?
  
> > - No way to send a signal to a thread (it would be useful to make a
> > thread raise an exception from another thread).
> 
> I agree this would be nice, and can easily be implemented in the case
> of bytecode threads.  For POSIX threads, one could try using
> cancellation to handle this, but I'm not sure it can be done in a
> portable way.  For Win32 threads, I don't know how to do it.
> 

I think it is worth a try ! even if the semantic means that after
handling the exception, the thread must terminates and it will never
receive another exception of this kind.

What I mean is that a clean interface to pthread_cleanup_push would be
enough
And probably portable (I do not know for Win32 ?)

>
>

A Last question: How to make the GC collects an inacessible thread ?
The pb is that the definition of inacessible is hard for a thread: it
means
no pointer to the thread (thats easy), but also no more common mutable
variables or channel
: the thread can not interact with the outside world. Moreover, one must
also define the outside world by choosing a main thread ...

All this looks hard, but it is necessary for my application ! In a first
approximation I will have a lot of potentialy dead thread running :-(



-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI

Re: Thread feature missing

[Xavier Leroy]

> I think it is better to have one channel for each thread and wait
> using Event.select that thread A or B send on their respective
> channel. Am I right ?

You can do that too.

> I have another little pb which is that Many threads may be waiting
> for A to terminate.  So I could do a loop always sending on the
> termination channel of A. But is there a better way ? A kind of
> broadcast forever a value on a channel ?

If you need that kind of stuff, you'd better not use the Event module
and design your own "mailbox" mechanism using mutexes and conditions
(as Gerd Stolpmann outlined).

However, I would argue that a design where a thread needs to be joined
by several other threads is broken.  In most threads libraries
(e.g. POSIX threads), you can join a thread at most once.

> Yet another question: What is the size of a thread in both cases:
> bytecode and native.
> Is 1000 threads reasonable ?

With bytecode threads, it's barely reasonable.  Each thread consumes
about 4 K of memory for its initial stack.

With native threads, it's ways too much.  E.g. LinuxThreads (or,
really, the Linux kernel) supports 256 threads for normal users, 512
for the super-user.

Again, I'd argue that a design that calls for thousands of threads is
broken.  See the periodic and lively discussions on
comp.programming.threads on this topic.

Instead of creating lots of short-lived threads, consider having a
reasonable number of worker threads (e.g. 10), started once and for
all, which pick things to do from a queue of requests.

> What I mean is that a clean interface to pthread_cleanup_push would be
> enough
> And probably portable (I do not know for Win32 ?)

No, Win32 has no equivalent of POSIX cancellation handlers.

> A Last question: How to make the GC collects an inacessible thread ?
> The pb is that the definition of inacessible is hard for a thread:
> it means no pointer to the thread (thats easy), but also no more
> common mutable variables or channel : the thread can not interact
> with the outside world. Moreover, one must also define the outside
> world by choosing a main thread ...

I see no way to do this.

> All this looks hard, but it is necessary for my application ! In a first
> approximation I will have a lot of potentialy dead thread running
> :-(

Then consider alternative designs for the application.

- Xavier Leroy

Re: Thread feature missing

[skaller]

Xavier Leroy wrote:

> Again, I'd argue that a design that calls for thousands of threads is
> broken.  See the periodic and lively discussions on
> comp.programming.threads on this topic.

I have an application that _requires_ thousands of 
threads of control. It has nothing to do with the 'design'.
Of course, the threads spend most of the time doing nothing,
and the current implementation uses callbacks not hardware
threads. However, programming in this environment directly
is bad; the programmer wants to write threads.

I was thinking of using the bytecode interpreter threads to
implement this. Is this not feasible? [Hardware threads are
too slow, I need to create 500 threads per second, with
a life of about 5 mins, which means about 20000 active threads:
the overhead of 4K is per thread is small, only ~80Meg]

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net

Some questions about floatting point issues

[jean-marc alliot]

Hi,

We have developped an interval programming library in ML. We use it
mainly for branch and bound optimization.

The problem is that, to write a correct interval library, you have to
use some processor specific features regarding rounding mode (you have
to turn it to rounding towards minus infinity when computing lower
bounds, towards plus infinity when computing upper bound, etc).

I wrote the assembly language routines to do the trick, but I have a few
questions:
1) What is the default mode turned on by ocaml (I suppose it is rounding
towards nearest?)
2) Is this mode often reinforced (before each floatting point operation)
or is it only set once?
3) Is it possible to tell ocamlopt to inline a few lines of assembly
code? Changing the FPU mode is very fast (two "mov", one "and" and one
"or") and it is a pity to suffer the overhead of one function call each
time.

Thanks

Jean-Marc Alliot

Re: Some questions about floatting point issues

[Xavier Leroy]

> The problem is that, to write a correct interval library, you have to
> use some processor specific features regarding rounding mode (you have
> to turn it to rounding towards minus infinity when computing lower
> bounds, towards plus infinity when computing upper bound, etc).
> 
> I wrote the assembly language routines to do the trick, but I have a few
> questions:
> 1) What is the default mode turned on by ocaml (I suppose it is rounding
> towards nearest?)

Caml doesn't change the rounding mode, it leaves whatever mode the C
run-time system sets before starting the Caml program.

(Not quite: on buggy libc's, e.g. libc 5 under Linux, Caml used to
change the mode at start-up to enable NaNs and other IEEE features,
but this is no longer necessary with Linux libc 6.)

> 2) Is this mode often reinforced (before each floatting point operation)
> or is it only set once?

It is never reinforced.  On the x86, float->int conversion changes the
rounding mode temporarily, but restores the original mode on exit.

> 3) Is it possible to tell ocamlopt to inline a few lines of assembly
> code? Changing the FPU mode is very fast (two "mov", one "and" and one
> "or") and it is a pity to suffer the overhead of one function call each
> time.

I agree that an inline asm facility would sometimes be useful, but
there is currently no such thing in Caml.

One little trick: assuming your C function to change mode doesn't
allocate and doesn't raise exceptions, you could declare it as

        external changemode : unit -> unit = "changemode" "noalloc"

The "noalloc" qualifier allows ocamlopt to generate a faster call to
the C routine.

- Xavier Leroy

Typing problem

[Daniel Bünzli]

Hello,

I would like to define the following types.

> type u = [ `U1 | `U2 ]
>
> type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]

t's parameter is used to statically express constraints in other  
parts of the code. My problem is that
the constraint on 'a is downgraded to [`U1] while I would like to be  
able to write

> let param : 'a t -> 'a = function (`A v | `B v) -> v

and get the following typing behaviour.

> let v = param (`A `U1) (* should type *)
> let v = param (`A `U2) (* should type *)
> let v = param (`B `U1) (* should type *)
> let v = param (`B `U2) (* should not type *)

Is it possible to express that in ocaml's type system ?

Regards,

Daniel

Re: Typing problem

[j h woodyatt]

Daniel Bünzli <daniel.buenzli@epfl.ch>
>
> I would like to define the following types.
>
>> type u = [ `U1 | `U2 ]
>> type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]
>
> t's parameter is used to statically express constraints in other  
> parts of the code. My problem is that the constraint on 'a is  
> downgraded to [`U1] while I would like to be able to write
>
>> let param : 'a t -> 'a = function (`A v | `B v) -> v
>
> and get the following typing behaviour.
>
>> let v = param (`A `U1) (* should type *)
>> let v = param (`A `U2) (* should type *)
>> let v = param (`B `U1) (* should type *)
>> let v = param (`B `U2) (* should not type *)
>
> Is it possible to express that in ocaml's type system ?

The short answer is no.  The reason is that 'a is not the same type  
in the `A case as in the `B case.  Type t really has two type  
parameters.  (Well, it can have only one if this contrived example is  
fully representative of your code, as I'll describe below).

type ('a, 'b) t = [ `A of 'a | `B of 'b ]
   constraint 'a = [< u ] constraint 'b = [ `U1 ]

However, 'b is concrete in your example, so-- if it's fully  
representative of your code-- you could just do this, and you would  
still have only one type parameter:

type 'a t = [ `A of 'a | `B of [ `U1 ] ]
   constraint 'a = [< u ]

—
j h woodyatt <jhw@conjury.org>