A Few Questions

A Few Questions

[Jonathan T Bryant]

I've been reasearching into a parallel extension to OCaml (based on 
Reppy's CML and the OCaml Event
module).  Mostly it's extending the semantics of channels and using 
CamlP4 to add syntactic constructs
for concurrency, but there are a few extensions I'm having trouble with 
because of OCaml language
"problems", and so I have a few questions.

1) Why can't a functorized module be used as a functor to another 
module?  I don't know if this is
semantically not possible or if I am just doing it wrong.  I've played 
around with the syntax and
reread the manuals, but I can't seem to find a solution.  For example:

module type AModule =
  sig
    type t
  end
module type BModule =
  functor (A : AModule) ->
  sig
    type t
    type s = A.t
  end
module S : sig type t end 
module Make = functor (B : BModule) -> S with type t = B.t  (* This is 
what fails *)
module AImpl =
  struct
    type t = int
  end
module BImpl =
  functor (A : AModule) ->
  struct
    type t = int
    type s = A.t
  end
module X = Make (BImpl (AImpl))

2) Why, in general, are there not first class modules?  I've looked at 
Russo's paper on this and it
shouldn't conflict with static typing or type inference.  Again, for 
example, why isn't this allowed:

val make : ('a -> 'b) -> ('a -> 'c) -> sig type t val x : 'a -> 'b val 
y : 'a -> 'c end
let make a b =
  struct
    type t = int
    let x = a
    let y = b
  end
module X = make (fun x -> x) (fun y -> y)

It doesn't seem like it would be very different from the already 
allowed immediate objects and local
module bindings.

3) Since CML's threads are implemented via continuations, speculative 
computation is allowed because
threads are simply GCed once they are not referenced any more.  Since 
OCaml's threads are implemeted
via system calls, is this still the case or do threads need to be 
manually joined?  I've run into
some instances where I can't create any more threads because the 
"Thread limit" of 1024 has been
reached, but in code where nowhere near that many threads should be 
left active.  Is this limit an
OCaml limit or a system limit?  Does it make a difference whether using 
native code and system
threads vs. bytecode and vmthreads?  Also, what about threads that are 
not referenced anymore but
should still be running (i.e., "background services" and the like)?  Is 
there any way to keep the GC
from collecting them?

4) I've found that in sending functions across sockets, I can only send 
them between copies of the
exact same binary image.  Is it possible to marshal functions to 
different binaries of the same code,
i.e., different platforms?  Again, does native vs. bytecode make a 
difference?

5) One possible extension is a vector type.  Is it possible as is to 
make the type inference
engine "as is" include the size of the underlying array as part of the 
type information or does that
require modifications to the type system?  Adding to the type 
information allows runtime size checks
to be avoided and allows code generation to take advantage of external 
vector processors and/or GPUs.
The ideal setup is vectors that are unboxed arrays of fixed length, 
similar to tuples.

Thanks,
--Jonathan Bryant

Re: [Caml-list] A Few Questions

[skaller]

On Sun, 2006-12-17 at 20:51 -0500, Jonathan T Bryant wrote:

> 3) Since CML's threads are implemented via continuations, speculative 
> computation is allowed because
> threads are simply GCed once they are not referenced any more.  Since 
> OCaml's threads are implemeted
> via system calls, is this still the case or do threads need to be 
> manually joined?  I've run into
> some instances where I can't create any more threads because the 
> "Thread limit" of 1024 has been
> reached, but in code where nowhere near that many threads should be 
> left active.  Is this limit an
> OCaml limit or a system limit?  

system limit.

> Also, what about threads that are 
> not referenced anymore but
> should still be running (i.e., "background services" and the like)?  Is 
> there any way to keep the GC
> from collecting them?

The gc doesn't collect threads in the first place.
It may collect a data structure identifying the thread if it
is unreachable.

Under Posix, if a thread is joinable it will not die until
joined. If it is detached, it will not die until it choses to.
(Assuming you don't kill it).

> 5) One possible extension is a vector type.  Is it possible as is to 
> make the type inference
> engine "as is" include the size of the underlying array as part of the 
> type information or does that
> require modifications to the type system?  

You would not want to do this. Use tuples instead.

Felix has arrays with known length as a data type,
in fact they're precisely tuples. The length type
is an anonymous sum of n units, written just 'n'.

However full manipulation is not possible. For example
you cannot have

	concat: array[t,n] * array[t,m] -> array[t,add(n,m)]


because add(n,m) cannot work with an unconstrained type variable.
In Felix, whilst

	(x:array[t,20]) + (y:array[t,30])

works correctly, you cannot concatenate arrays inside
a routine with polymorphic array bounds, even if the
instantiator would fix the bounds to a constant later.

In Ocaml there's no instantiator in the first place,
so the calculation would have to be done at run time
anyhow and require dependent typing support.

But the existing Array types in Ocaml simply drop the
length information. This avoids the problem at the 
cost of not permitting enforced array bounds checks
based on type.

Note that in theory a subscript to an array of length n
is a value of type n, which is a unit sum, so the subscript
is a value of that unit sum, and such an index never requires
any bounds checking.

oleg showed a cute way to do the dependent typing on
existing arrays, and avoid many unnecessary checks,
in existing Ocaml. Maybe he can post the URL to that again.


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] A Few Questions

[Nathaniel Gray]

On 12/17/06, Jonathan T Bryant <jtbryant@valdosta.edu> wrote:

> 4) I've found that in sending functions across sockets, I can only send
> them between copies of the
> exact same binary image.  Is it possible to marshal functions to
> different binaries of the same code,
> i.e., different platforms?  Again, does native vs. bytecode make a
> difference?

Nope.  From the docs for Marshal.to_channel:

If flags contains Marshal.Closures, functional values will be
marshaled as a position in the code of the program. In this case, the
output of marshaling can only be read back in processes that run
exactly the same program, with exactly the same compiled code. (This
is checked at un-marshaling time, using an MD5 digest of the code
transmitted along with the code position.)

Cheers,
-n8

-- 
>>>-- Nathaniel Gray -- Caltech Computer Science ------>
>>>-- Mojave Project -- http://mojave.cs.caltech.edu -->

Re: A Few Questions

[oleg]

Jonathan T Bryant wrote:
> module type AModule = sig type t end
> module type BModule =
>    functor (A : AModule) ->
>       sig
>        type t
>        type s = A.t
>    end
> module S : sig type t end
> module Make = functor (B : BModule) -> S with type t = B.t 

and indeed the last line is problematic: S is a module (aka structure)
rather than a module type (aka signature). The `with type' applies
only to signatures. You have omitted S's body. In full, one would
write
  module S : sig type t end = struct type t = unit end
What is the meaning of `S with type t = B.t' then? The type `t' in S
signature is already associated with unit; we can't replace it with
another type B.t. Imagine if we could write
	module Foo : sig type t val v : t end =
		struct type t = unit let v = () end
	let module Bar = Foo with type t = int
what is the value of Bar.v then?

Incidentally, OCaml does support higher-order functors (that is,
functors can be both arguments and results of other functors). Also,
module signatures (`module type') may be components of structures.

> why isn't this allowed:
> val make : ('a -> 'b) -> ('a -> 'c) -> 
>    sig type t val x : 'a -> 'b val y : 'a -> 'c end
> let make a b = struct
>     type t = int
>     let x = a
>     let y = b
> end
> module X = make (fun x -> x) (fun y -> y)

Hmm, the following

module Make(X: sig val a : 'a -> 'a val b : 'a -> 'a end) :
  sig type t val x : 'a -> 'a val y : 'a -> 'a end =
  struct
    type t = int
    let x = X.a
    let y = X.b
  end;;
module X = Make(struct let a = fun x -> x let b = fun y -> y end);;

seems quite isomorphic to the desideratum, and is accepted by Ocaml. I
assumed that the signature
   val make : ('a -> 'b) -> ('a -> 'c)
has a typo: there are few interesting functions that have the type of 
'a -> 'b (e.g., let rec loop x = loop x and failwith and
Obj.magic). Certainly fun x -> x is not one of them. So, 
	make (fun x -> x) (fun y -> y)
in your code must raise the type error at least for that reason.

> 4) I've found that in sending functions across sockets,
> I can only send them between copies of the exact same binary image.
> Is it possible to marshal functions to different binaries of the same
> code, i.e., different platforms?  Again, does native vs. bytecode make
> a difference?

Different platforms may have different word sizes, different
alignment. Different version of the bytecode programs may be compiled
by ocamlc that has different sets of primitive operations and
pervasives. Your program may contain
	let foo () = Unix.fork ()
now, we serialize the closure 'foo', ship it over to a network pipe
to a windows machine, deserialize and attempt to execute. What the
result would be?

It is far easier for the programmer to defunctionalize the part of his
code that is intended to be mobile.


> 5) Number-parameterized vectors
Matthias Blume has done exactly that, for SML. His technique is
applicable to OCaml. Although the functions like concatenation of
vectors is not expressible as this requires the type system to do
decimal arithmetics. It is possible in Haskell btw, with the
typechecker indeed doing decimal arithmetics.

    Matthias Blume: 
    No-Longer-Foreign: Teaching an ML compiler to speak C ``natively.'' 
    In BABEL'01: First workshop on multi-language infrastructure and
interoperability, September 2001, Firenze, Italy.
    http://people.cs.uchicago.edu/~blume/pub.html

However, we can achieve essentially the same with the simpler means

  http://pobox.com/~oleg/ftp/ML/eliminating-array-bound-check-literally.ml

Actually, we can achieve something more powerful: elimination of array
bound check even if the array is allocated dynamically and its size is
not known till the run-time: see especially the comment by Alain
Frisch at the end of the above file.