1 Apr 2011 01:43

### Re: Re: Arithmetic operations

On Thu, Mar 31, 2011 at 8:19 AM, Gabriel Scherer wrote:

but their internal code is naturally their top priority, and the external release model has been rather sporadic for now.

This has certainly been true, but Till has done good work in simplifying the process of generating a release, and we should be able to do releases far more often now.

y

1 Apr 2011 01:46

### Re: Reasoning about categories at compile-time.

```Le Thursday 31 Mar 2011 à 08:02:30 (+0200), Gabriel Scherer a écrit :
>    First, one obvious solution : parse the equations, run a solver, then
>    output "()" if it can deduce the queries from the equations, and "1 =
>    true" otherwise. Why isn't this solution satisfying ?

Because that would mean, in Camlp4, doing a processing of the whole

module X : sig
(* category constraints / proof goals *)
end = struct
(* category axioms *)
end

I want to be able to deal separately with .ml and .mli files. Or with a module
structure and a module signature.

Therefore I need it to be such that it is the type checker that is in
charge of being the solver.

I'd love a 'type system extension' mechanism... this way I could include
the solver in it.

>    With the type system there is one thing that is easy and natural to do
>    : you could encode your arrows as elements with a specific type (eg.
>    for an arrow `f` of source `src` and destination `dst` you would write
>    `(src, f, dst) arrow` with `src, f, dst` abstract types) :
>
>      arrow_f : (foo, f, bar) arrow
>
>    then write both a composition function
>
>      compose : ('a, 'f, 'b) arrow -> ('b, 'g, 'c) arrow -> ('a, ('f, 'g) comp, 'c) arrow
>
>    and terms representing your equational theory:
>
>      assoc : ('a, (('f, 'g) comp, 'h) comp, 'b) arrow -> ('a, ('f, ('g, 'h) comp) comp, 'b)
>
>    and for each equation f o g = h (not that I use `g` and not `'g`)
>
>      witness_fg_h : ('a, (f, g) comp, 'b) arrow -> ('a, h, 'b) arrow
>
>    Then, for each deducible relation, there exist a typed term that is a
>    proof witness of the relation deductibility (you just unify the type of
>    the two arrows that should be equal). If you have a solver for equation
>    deductibility, you can ask him to output the proof witness in this
>    format.

I thought of that, though not as precisely as you're exposing it.

But keeping the .ml / .mli distinction and compiling them separately,
you have a problem: Essentially, the witnesses live in the .ml file, and
the proof witness also lives in the .ml file. In the .mli file, you
simply have to declare the existence of a proof witness term.

However, in order to construct the proof witness, you need to know the
goal that you wish to prove, which means providing to camlp4 some
information that lives in the .mli file.

This would break separate compilation. Or rather separate preprocessing.
You could not preprocess the .ml file before the .mli file. Worse: you
could not do:

module X with syntax extension = struct

...

end

module type S with syntax extension = sig

...

end

let m = (module X : S)

(which is what I want to do, specifically).

>    This does not use the inference system to solve your problem, which is
>    what you asked for. But this is a solid design that is going to still
>    work if you change your language, eg. can still be used on non
>    decidable questions. I think this is a good first step; feel free to
>    improve it by whatever advanced type hackery.

Unfortunately, this doesn't fit the bill. I had this picture in mind
intuitively but not formalised, and I saw the limitation I explained
above. That's what prompted me to ask on the list in the first place.

But thanks for clarifying my hazy thoughts.

What bugs me is that, to put it simply, the category axioms are
generated by Camlp4 in a non-deterministic fashion, dependent on the
outside world. You only have control in user code on the proof goals.

What you propose means linking module struct and module type
syntactically. However, I'd need them decoupled as I'd like in the long
run to do the following:

You have two categories, C1 and C2. You take the set union of both
categories C1 U C2. (Set union of objects, and set unions of arrows).
This gives two OCaml modules. You include both modules into a bigger
module, add some arrows and arrow composition axioms. You then want to
match them against a module signature describing the proof goals.

Do the same thing with first-class modules (OCaml 3.13 doesn't need so
much module signatures as OCaml 3.12 for first-class modules, which goes
in the sense of 'decoupling' preprocessed modules and preprocessed
signatures), and you get an idea of what I'm up to.

That's why I'm looking for a purely type-system encoding of this
problem. Somehow lifting the solver for equational deducibility you
mentionned into the type inference algo itself.

So instead of having arrows as private types, I was thinking of having
arrows as type parameters. And have unification doing the solving.
Unfortunately, if you put equational constraints in the module
signature, they leak into the module implementation (funny to have a
signature leaking in an implementation by the way). Just think of the
simple

module X : sig
val f : 'a -> 'a
end = struct
let f : 'a -> 'b = Obj.magic
end

This is somehow reversed:

module X : sig
val f : 'a -> 'b
end = struct
let f : 'a -> 'a = assert false
end

fails to type-check, which could perhaps be understood as 'given two
types not known to be equal, I fail to conclude that 'a = 'a and 'b =
'a, i.e. I fail to conclude that 'b = 'a. This is tautological, but it's
interesting to see that the axioms are now in the signature and the goal
in the module structure.

I was wondering perhaps naïvely how much truth there is in the above
paragraph, and if it could be used to encode the equational solver into
the unification algo in one way or another.

--
Guillaume Yziquel

--

--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

```
1 Apr 2011 10:12

### invitatie

INSPECTOR RESURSE UMANE - cod COR 342304 - autorizat CNFPA

Inspectorul de resurse umane  este un angajat de baza al oricarei companii, indispensabil desfasurarii oricarei activitati economice, el este cel care asigura gestionarea optima a angajatilor, indiferent de numarul acestora. Evrika vine in sprijinul celor care vor sa profeseze sau sa aprofundeze cunostiintele in acest domeniu prin organizarea cursului de Inspector resurse umane. .

Cursul are un pronuntat caracter practic – aplicativ, iar pregatirea cursantilor se desfasoara cu mijloace si metode moderne: dezbateri, discutii active, exemplificari si studii de caz, pe durata a 56 de ore la pretul de 250 ron. Cursul va incepe pe data de 12 aprilie 2011.

si tematica cursului le gasiti aici

In urma sustinerii examenului final se obtine un Certificat de absolvire  eliberat de Ministerul Muncii Familiei si Egalitatii de Sanse,si Ministerul Educatiei, Cercetarii si Tineretului recunoscut pe piata muncii.

Pentru informatii suplimentare va rugam sa contactati Departamentul Cursuri, tel.: 021.314.90.40, 0767.803.244; email: office <at> evrikagroup.ro.

Daca vreti sa profitati de oportunitatile ce pot aparea apasati SUBSCRIBE, daca nu, apasati UNSUBSCRIBE.

1 Apr 2011 11:25

### Re: Fwd: Hoogle for your language (i.e. F#, Scala, ML, Clean...)

```On 03/20/2011 06:10 PM, Thomas Braibant wrote:
> Hi,
>
> I just found out the following: http://search.ocaml.jp/ which might be
> of interests to the member of this list. It seems to be similar to
> Hoogle, but I wonder what are the relations between them.
But it seems not to work correclty: I ask for 'a -> 'a list

http://search.ocaml.jp/?q=%27a+-%3E+%27a+list

and it returns 'a list -> 'a list functions.

Dawid

--

--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

```
1 Apr 2011 12:15

### Re: Re: Fwd: Hoogle for your language (i.e. F#, Scala, ML, Clean...)

But it seems not to work correclty: I ask for 'a -> 'a list

http://search.ocaml.jp/?q=%27a+-%3E+%27a+list

and it returns 'a list -> 'a list functions.

I'm an author of OCaml API Search.
Thanks for using.

I borrowed searching module from OCamlBrowser http://caml.inria.fr/pub/docs/manual-ocaml/manual028.html.
OCamlBrowser is older than hoogle, so there are some difference.

2 Apr 2011 08:17

Hi All:

2 Apr 2011 08:20

### About batteries 1.30 buiding on win7 plantform

Hi all:
I try to build batteries 1.30 on my win7 PC,but it give me a fatal error like this:

\$ make all
cp -f src/batCamomile-0.7.ml src/batCamomile.ml
test ! -e src/batteries_config.ml || rm src/batteries_config.ml
ocamlbuild syntax.otarget byte.otarget src/batteries_help.cmo META shared.otarge
t
Finished, 0 targets (0 cached) in 00:00:00.
+ ocamlrun mkconf.byte src/batteries_config.mlp src/batteries_config.ml
Fatal error: unknown C primitive `unix_dup'
Command exited with code 2.
Compilation unsuccessful after building 276 targets (275 cached) in 00:00:01.
make: *** [all] Error 10

is it don't support the windows 7?
3 Apr 2011 09:25

### Re: Reasoning about categories at compile-time.

```I would be interested to hear why the problem must be solved with
camlp4 and ocaml, because this looks a lot like an instance of someone
with a hammer looking for some nails to hit.

With kind regards,

Andrej

--

--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

```
3 Apr 2011 23:03

### Re: Reasoning about categories at compile-time.

```Le Sunday 03 Apr 2011 à 09:25:54 (+0200), Andrej Bauer a écrit :
> I would be interested to hear why the problem must be solved with
> camlp4 and ocaml, because this looks a lot like an instance of someone
> with a hammer looking for some nails to hit.

Because it's fun and interesting.

--
Guillaume Yziquel

--

--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

```
4 Apr 2011 14:59

```
You can now try the OCaml toplevel online:

http://ocsigen.org/js_of_ocaml/toplevel/

Your code is executed in the Web browser, not on some remote server.

Technically, the OCaml toplevel and the Js_of_ocaml compiler have been
put together in a single OCaml program, which has then been compiled
to Javascript. The source code is currently available in the darcs
repository of the Js_of_ocaml compiler.

http://ocsigen.org/js_of_ocaml/

Get the source code:
darcs get http://ocsigen.org/darcs/js_of_ocaml/

Contributions (syntax highlighting, history, ...) are welcome!

--
Jerome Vouillon

--

--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

```

Gmane