Re: [Caml-list] Subtyping
Jacques Garrigue writes: > type 'a base = {x : 'a; fn : 'a -> unit} > type 'b base_op = {bop: 'a. 'a base -> 'b} > type base_wrapper = {base: 'b. 'b base_op -> 'b} > > let l = > let a = {x = 1; fn = print_int} > and b = {x = 1.2; fn = print_float} in > [{base = fun x -> x.bop a}; {base = fun x -> x.bop b}] > > List.iter (fun w -> w.base {bop = fun r -> r.fn r.x}) l > > As you can see, the result is rather verbose, but this works. > Fortunately, closure and objects are usually enough... > > Jacques Garrigue That is exactly what I ment. I knew closures could have "'a. ..." types but I didn't think of encoding the record and the method to call both as closures. MfG Goswin ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Subtyping
Here is a slightly more usable version, using helper functions to avoid writing intermediate closures by hand. type 'a base = {x : 'a; fn : 'a -> unit} (* 4 next lines are boilerplate, could be auto-generated *) type 'b base_op = {bop: 'a. 'a base -> 'b} type base_wrapper = {base: 'b. 'b base_op -> 'b} let wrap a = {base = fun x -> x.bop a} let apply op w = w.base op let l = [wrap {x = 1; fn = print_int}; wrap {x = 1.2; fn = print_float}];; List.iter (apply {bop = fun r -> r.fn r.x}) l The only thing you cannot abbreviate is the {bop = ...} part, as this is where universality is checked, to ensure that no cross application can be done. Jacques Garrigue > Then what you are asking for is existential types. There is no syntax > for them in ocaml, but they can be encoded through universal types > (interestingly, the dual is not true). > > type 'a base = {x : 'a; fn : 'a -> unit} > type 'b base_op = {bop: 'a. 'a base -> 'b} > type base_wrapper = {base: 'b. 'b base_op -> 'b} > > let l = > let a = {x = 1; fn = print_int} > and b = {x = 1.2; fn = print_float} in > [{base = fun x -> x.bop a}; {base = fun x -> x.bop b}] > > List.iter (fun w -> w.base {bop = fun r -> r.fn r.x}) l > > As you can see, the result is rather verbose, but this works. > Fortunately, closure and objects are usually enough... ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Subtyping
From: Goswin von Brederlow > Small extra question concerning this. Can I get ocaml to recognise a > type like this? > > type base = 'a. { > x : 'a; > fn : 'a -> unit; > } > > List.iter > (fun r -> r.fn r) > [{x = 1; fn = (fun r -> print_int r.x); }; >{x = 1.2; fn = (fun r -> print_float r.x); }] > > The difference to a "'a base" type would be that the 'a is only > infered and fixed inside the record but remains abstract outside of > it. First reaction: but your "base" type is just a closure. But this is certainly not your question. More disturbing: the rest of your code does not agree with base. So I will assume you actually meant List.iter (fun r -> r.fn r.x) [{x = 1; fn = print_int}; {x = 1.2; fn = print_float}] Then what you are asking for is existential types. There is no syntax for them in ocaml, but they can be encoded through universal types (interestingly, the dual is not true). type 'a base = {x : 'a; fn : 'a -> unit} type 'b base_op = {bop: 'a. 'a base -> 'b} type base_wrapper = {base: 'b. 'b base_op -> 'b} let l = let a = {x = 1; fn = print_int} and b = {x = 1.2; fn = print_float} in [{base = fun x -> x.bop a}; {base = fun x -> x.bop b}] List.iter (fun w -> w.base {bop = fun r -> r.fn r.x}) l As you can see, the result is rather verbose, but this works. Fortunately, closure and objects are usually enough... Jacques Garrigue ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Subtyping
Goswin von Brederlow writes: > So what other ways are there of doing this? Records. Idealy I would > like to do this: > > type base = { x : int } > let make_base x = { x = x } > let print_x r = print_int r.x > type foo = { base with y : int } > let make_foo x y = { x = x; y = y } > let _ = > print_x (make_base 0); print_newline (); > print_x (make_foo 0 1); print_newline ();; > > Ocaml has no way of making this work like that, right? Small extra question concerning this. Can I get ocaml to recognise a type like this? type base = 'a. { x : 'a; fn : 'a -> unit; } List.iter (fun r -> r.fn r) [{x = 1; fn = (fun r -> print_int r.x); }; {x = 1.2; fn = (fun r -> print_float r.x); }] The difference to a "'a base" type would be that the 'a is only infered and fixed inside the record but remains abstract outside of it. For that reason this would not be allowed: let cross_call x y = x.fn y The 'a would have to escape the record which wouldn't be allowed. So is there any syntax or trick to get the ocaml typesystem to construct such a type? MfG Goswin ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Subtyping
Peng Zang writes: > On Tuesday 07 April 2009 03:41:32 am David MENTRE wrote: >> Hello, >> >> On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow > wrote: >> > In the last 2 weeks I've been playing around with lots of different >> > ways to do the same thing to get a feel for what style suites me >> > best. If you have improvements or alternative ways of doing the two >> > things below let me know. >> >> Well, if you are learning OCaml, I would advise you to read regular >> OCaml code, e.g. the standard library. You'll learn The Right OCaml >> Style(tm). > > Certainly reading the standard library is good. Useful for learning > techniques, idioms, etc.. I wouldn't say that there is one Right OCaml > Style(tm) though. Actually part of why I like OCaml is that it supports > imperative, object oriented and functional paradigms and you can switch > between them depending on the task. Exactly. And so far I've been kind of stuck with one or the other so I wanted to see how things look using different paradigms in ocaml. > Cheers, > > Peng MfG Goswin ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Subtyping
David MENTRE writes: > Hello, > > On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow wrote: >> In the last 2 weeks I've been playing around with lots of different >> ways to do the same thing to get a feel for what style suites me >> best. If you have improvements or alternative ways of doing the two >> things below let me know. > > Well, if you are learning OCaml, I would advise you to read regular > OCaml code, e.g. the standard library. You'll learn The Right OCaml > Style(tm). I've been using ocaml on and off for years now. Just trying out new things. >> Lets look another thing going in a similar direction. I want to >> have a structure where I can store key value pairs. But just for fun >> lets say I want to store values of different types and the key knows >> the type of value. In short a heterogeneous associative container: > > Well, why don't you just do: > > # type k = Int_k of int | Float_k of int;; > type k = Int_k of int | Float_k of int > # type v = Int_v of int | Float_v of float;; > type v = Int_v of int | Float_v of float > # let h = Hashtbl.create 3;; > val h : ('_a, '_b) Hashtbl.t = > # Hashtbl.add h (Int_k 3) (Int_v 4);; > - : unit = () > # Hashtbl.add h (Float_k 5) (Float_v 0.6);; > - : unit = () That would allow storing a float value under an int key or vice versa. Something that would completly corrupt the on-disk format of my data. One could add runtime checks that prevent this but I would really like to have this ensured by the type system at compile time. And I would like to avoid having to write a private insert functions and public let insert_int k v = insert (Int_k k) (Int_v v) let insert_float k v = insert (Float_k k) (Float_v v) For that the storing data structure would have to know that there are int and float values and I would rather have the storing structure polymorphic. MfG Goswin ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] [OT]: Petition against Softwarepatents
Hello, there is a petition against softwarepatents in europe. Please sign the petition and spread the word! http://www.stopsoftwarepatents.eu/ Ciao, Oliver Bandel ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] camomile vs netstring
Can anyone summarize the trade-offs between the Camomile and Netstring (netconversion) unicode translation libraries? The netconversion documentation (http://projects.camlcity.org/projects/dl/ocamlnet-2.2.9/doc/html-main/Netconversion.html ) mentions that Camomile implements text strings as int arrays, whereas it encodes them as packed native strings... so I'm guessing that Netstring is a win space-wise when random access isn't needed. However, are there other trade-offs to be aware of -- bugs, other performance issues, ease of use? Camomile seems to provide a larger number of conversions, but I have no idea whether these are actually useful, or simply legacy artifacts. I think my unicode needs are fairly simple, but then again, maybe everyone thinks that as they're diving off this cliff. :-) Warren -- Warren Harris war...@metaweb.com Metaweb Technologies http://www.freebase.com - An open database of the world’s information. ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] RE: flexlink + lacaml (lapack)
DESMONS Bertrand wrote: By the way, where can I see whether the file in question is a symbolic link? "ls -l"? or "cmd /c dir" With "cmd /c dir", you should see a file "liblapack.a.lnk" (in /lib). Can you see it? Is there a file "liblapack.a" as well? -- Alain ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] RE: flexlink + lacaml (lapack)
>Can you try passing "-ccopt -cygpath" to ocamlc? Yes, but the error persists... | a...@pc~/UMH/Master 2 | $ ocamlc -ccopt -cygpath -I "C:/Program Files/Objective Caml/lib/site-lib/lacam | l" bigarray.cma lacaml.cma -verbose d.ml | + flexlink -chain mingw -exe -o "camlprog.exe" "-LC:/Program Files/Objective C | aml/lib/site-lib/lacaml" "-LC:\Program Files\Objective Caml\lib" "C:\DOCUME~1\ac | er\LOCALS~1\Temp\camlprim6bb2c7.c" "-llacaml_stubs" "-llapack" "-lblas" "-lbigar | ray" "-lcamlrun" -lws2_32 -cygpath -Lc:/cygwin/lib | ** Fatal error: Error while reading c:/cygwin/lib\liblapack.a: Sys_error("Invali | d argument") | File "d.ml", line 1, characters 0-1: | Error: Error while building custom runtime system By the way, where can I see whether the file in question is a symbolic link? Thank you for your help, Bertrand Desmons ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] flexlink + lacaml (lapack)
DESMONS Bertrand wrote: Hello, Compiling a little program using Lacaml (in a cygwin shell) gives me the error: The library file seems to be a symbolic link. flexlink is a regular Win32 application and does not know about this Cygwin-specific notion. The good news is that it can use the external command cygpath (that comes with Cygwin) to resolve such links (and more generally Cygwin paths). This is the default behavior for the cygwin toolchain, but not for mingw. Can you try passing "-ccopt -cygpath" to ocamlc? Regards, Alain ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] flexlink + lacaml (lapack)
Hello, Compiling a little program using Lacaml (in a cygwin shell) gives me the error: | a...@pc~/UMH/Master 2 | $ ocamlfind ocamlc -package lacaml -linkpkg d.ml | ** Fatal error: Error while reading c:/cygwin/lib\liblapack.a: Sys_error("Invali | d argument") | File "d.ml", line 1, characters 0-1: |Error: Error while building custom runtime system Here is the file d.ml: | open Lacaml.Impl.D | | let f x = add x one | | let () = | let i = 3. in | let n = f i in | print_float n Verbosing the compilation command gives: | a...@pc~/UMH/Master 2 | $ ocamlfind ocamlc -package lacaml -linkpkg -verbose d.ml | Effective set of compiler predicates: pkg_bigarray,pkg_lacaml.core,pkg_lacaml,au | tolink,byte | + ocamlc.opt -verbose -I c:/Program Files/Objective Caml/lib/site-lib/lacaml -cc | opt -I"c:/Program Files/Objective Caml/lib/site-lib/lacaml" -ccopt -L"c:/Program | Files/Objective Caml/lib/site-lib/lacaml" C:/Program Files/Objective Caml/lib\b | igarray.cma c:/Program Files/Objective Caml/lib/site-lib/lacaml\lacaml.cma d.ml | + flexlink -chain mingw -exe -o "camlprog.exe" "-Lc:/Program Files/Objective C | aml/lib/site-lib/lacaml" "-LC:\Program Files\Objective Caml\lib" "C:\DOCUME~1\ac | er\LOCALS~1\Temp\camlprim6b3257.c" "-llacaml_stubs" "-llapack" "-lblas" "-lbigar | ray" "-lcamlrun" -lws2_32 -I"c:/Program Files/Objective Caml/lib/site-lib/lacaml | " -L"c:/Program Files/Objective Caml/lib/site-lib/lacaml" -Lc:/cygwin/lib | ** Fatal error: Error while reading c:/cygwin/lib\liblapack.a: Sys_error("Invali | d argument") | File "d.ml", line 1, characters 0-1: | Error: Error while building custom runtime system | ocamlc.opt returned with exit code 2 The file in question does exist, as Ocaml can read it: Objective Caml version 3.11.0 Findlib has been successfully loaded. Additional directives: #require "package";; to load a package #list;; to list the available packages #camlp4o;;to load camlp4 (standard syntax) #camlp4r;;to load camlp4 (revised syntax) #predicates "p,q,...";; to set these predicates Topfind.reset();; to force that packages will be reloaded #thread;; to enable threads # let input = open_in "C:/cygwin/lib\\liblapack.a";; val input : in_channel = # let str = input_line input;; val str : string = "!liblapack.dll.a\000" # let str = input_line input;; Exception: End_of_file. # close_in input;; - : unit = () # input;; - : in_channel = # So the problem seems to come from flexlink... I have no idea of what happens... It worked when I was with OCaml 3.10.2... Of course, I recompiled all the necessary when passing to 3.11. I'm running Windows XP, and as said above, compiling under Cygwin (but OCaml is the Win32/MinGW one). Thank you for any suggestions, Bertrand Desmons ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] CFP: JFP Special Issue on Generic Programming
OPEN CALL FOR PAPERS JFP Special Issue on Generic Programming Deadline: 1 October 2009 http://www.comlab.ox.ac.uk/ralf.hinze/JFP/cfp.html Scope - Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast to normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, classes, concepts, or even programming paradigms. This special issue aims at documenting state-of-the-art research, new developments and directions for future investigation in the broad field of Generic Programming. It is an outgrowth of the series of Workshops on Generic Programming, which started in 1998 and which continues this year with an ICFP affiliated workshop in Edinburgh. Participants of the workshops are invited to submit a suitably revised and expanded version of their paper to the special issue. The call for papers is, however, open. Other contributions are equally welcome and are, indeed, encouraged. All submitted papers will be subjected to the same quality criteria, meeting the standards of the Journal of Functional Programming. The special issue seeks original contributions on all aspects of generic programming including but not limited to o adaptive object-oriented programming, o aspect-oriented programming, o case studies, o concepts (as in the STL/C++ sense), o component-based programming, o datatype-generic programming, o generic programming with dependent types, o meta-programming, o polytypic programming, and o programming with modules. Submission details -- Manuscripts should be unpublished works and not submitted elsewhere. Revised versions of papers published in conference or workshop proceedings that have not appeared in archival journals are eligible for submission. Deadline for submission: 1 October 2009 Notification of acceptance or rejection: 15 January 2010 Revised version due: 15 March 2010 For submission details, please consult http://www.comlab.ox.ac.uk/ralf.hinze/JFP/cfp.html or see the Journal's web page http://journals.cambridge.org/jfp Guest Editor Ralf Hinze University of Oxford Computing Laboratory Wolfson Building, Parks Road, Oxford OX1 3QD, UK. Telephone: +44 (1865) 610700 Fax: +44 (1865) 283531 Email: ralf.hi...@comlab.ox.ac.uk WWW: http://www.comlab.ox.ac.uk/ralf.hinze/ --- ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Subtyping
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 On Tuesday 07 April 2009 03:41:32 am David MENTRE wrote: > Hello, > > On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow wrote: > > In the last 2 weeks I've been playing around with lots of different > > ways to do the same thing to get a feel for what style suites me > > best. If you have improvements or alternative ways of doing the two > > things below let me know. > > Well, if you are learning OCaml, I would advise you to read regular > OCaml code, e.g. the standard library. You'll learn The Right OCaml > Style(tm). Certainly reading the standard library is good. Useful for learning techniques, idioms, etc.. I wouldn't say that there is one Right OCaml Style(tm) though. Actually part of why I like OCaml is that it supports imperative, object oriented and functional paradigms and you can switch between them depending on the task. Cheers, Peng -BEGIN PGP SIGNATURE- Version: GnuPG v2.0.7 (GNU/Linux) iD8DBQFJ21eifIRcEFL/JewRAptXAJwPec++ykZ6YjmLuUtdfrZw3IrXEwCbBkeB juGHNPOqJds1rDZd8S1BQEQ= =foQf -END PGP SIGNATURE- ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: Re : [Caml-list] ocamlgraph ConcreteBidirectional and Dot
> I have a question related to this: Is there a reason for the absence of a > ConcreteBidirectionalLabeled graph in the API? Simply an historical reason: the module ConcreteBidirectional is an external contribution (by Ted Kremenek), which was only recently added to Ocamlgraph. Anybody can contribute to a ConcreteBidirectionalLabeled module and we'll happily add it to Ocamlgraph. -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re : [Caml-list] ocamlgraph ConcreteBidirectional and Dot
Hi, I have a question related to this: Is there a reason for the absence of a ConcreteBidirectionalLabeled graph in the API? Thanks, Matthieu - Message d'origine > De : Jean-Christophe Filliâtre > À : Pietro Abate > Cc : caml-list@yquem.inria.fr > Envoyé le : Mardi, 7 Avril 2009, 9h35mn 22s > Objet : Re: [Caml-list] ocamlgraph ConcreteBidirectional and Dot > > Hi, > > Sorry for the late answer... > > > I've a small problem with ocamlgraph. > > I want to parse a dot graph into a ConcreteBidirectional. > > > > The problem is that the signature needed for Dot.Parse requires a function > > edge, but I've no mean to specify a label (since it is unlabelled !!)... > > > > The functor for ConcreteBidirectional says E.t = (V.t * V.t), > > but I don't quite understand the type of B.G.E.label ... > > You're right, some type information is missing and there is no way to > instantiate the Dot functor with the current signature of > ConcreteBidirectional. > > One easy patch (if you are compiling ocamlgraph from sources) is to add > the constraint > > ... and type E.label = unit > > to the signature of functor ConcreteBidirectional. I think we'll do that > in the next release of ocamlgraph (and similarly for other unlabeled > graph data structures provided in ocamlgraph). > > Hope this helps, > -- > Jean-Christophe > > ___ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Subtyping
Hello, On Tue, Apr 7, 2009 at 07:48, Goswin von Brederlow wrote: > In the last 2 weeks I've been playing around with lots of different > ways to do the same thing to get a feel for what style suites me > best. If you have improvements or alternative ways of doing the two > things below let me know. Well, if you are learning OCaml, I would advise you to read regular OCaml code, e.g. the standard library. You'll learn The Right OCaml Style(tm). > Lets look another thing going in a similar direction. I want to > have a structure where I can store key value pairs. But just for fun > lets say I want to store values of different types and the key knows > the type of value. In short a heterogeneous associative container: Well, why don't you just do: # type k = Int_k of int | Float_k of int;; type k = Int_k of int | Float_k of int # type v = Int_v of int | Float_v of float;; type v = Int_v of int | Float_v of float # let h = Hashtbl.create 3;; val h : ('_a, '_b) Hashtbl.t = # Hashtbl.add h (Int_k 3) (Int_v 4);; - : unit = () # Hashtbl.add h (Float_k 5) (Float_v 0.6);; - : unit = () Yours, d. ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Call for Papers: PLMMS 2009
The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems PLMMS 2009 Munich, Germany; August 21, 2009 http://plmms09.cse.tamu.edu/ CALL FOR PAPERS The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems will be co-located with TPHOLs 2009. General Information The scope of this workshop is at the intersection of programming languages (PL) and mechanized mathematics systems (MMS). The latter category subsumes present-day computer algebra systems (CAS), interactive proof assistants (PA), and automated theorem provers (ATP), all heading towards fully integrated mechanized mathematical assistants. Areas of interest include all aspects of PL and MMS that meet in the following topics, but not limited to: * Dedicated input languages for MMS: covers all aspects of languages intended for the user to deploy or extend the system, both algorithmic and declarative ones. Typical examples are tactic definition languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, or specialized programming languages built into CA systems. * Mathematical modeling languages used for programming: covers the relation of logical descriptions vs. algorithmic content. For instance the logic of ACL2 extends a version of Lisp, that of Coq is close to Haskell, and some portions of HOL are similar to ML and Haskell, while Maple tries to do both simultaneously. Such mathematical languages offer rich specification capabilities, which are rarely available in regular programming languages. How can programming benefit from mathematical concepts, without limiting mathematics to the computational world view? * Programming languages with mathematical specifications: covers advanced mathematical concepts in programming languages that improve the expressive power of functional specifications, type systems, module systems etc. Programming languages with dependent types are of particular interest here, as is intentionality vs extensionality. * Language elements for program verification: covers specific means built into a language to facilitate correctness proofs using MMS. For example, logical annotations within programs may be turned into verification conditions to be solved in a proof assistant eventually. How need MMS and PL to be improved to make this work conveniently and in a mathematically appealing way? These issues have a very colorful history. Many PL innovations first appeared in either CA or proof systems first, before migrating into more mainstream programming languages. This workshop is an opportunity to present the latest innovations in MMS design that may be relevant to future programming languages, or conversely novel PL principles that improve upon implementation and deployment of MMS. Why are all the languages of mainstream CA systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modeling? How can MMS regain the upper hand on issues of "genericity" and "modularity"? What are the biggest barriers to using a more mainstream language as a host language for a CAS or PA/ATP? PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was a CICM 2008 workshop. Submission Details * Submission deadline: May 11, 2009 (Apia, Samoa time) * Author Notification: June 22, 2009 * Final Papers Due: July 10, 2009 * Workshop: August 21, 2009 Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length is restricted to 10 pages, and the font size 9pt. Each submission must adhere to SIGPLAN's republication policy, as explained on the web. Violation risks summary rejection of the offending submission. Papers are exclusively submitted via EasyChair http://www.easychair.org/conferences?conf=plmms09 We expect that at least one author of each accepted paper attends PLMMS 2009 and presents her or his paper. Accepted papers will appear in the ACM Digital Library. Links * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site * http://tphols.in.tum.de/, the THOPLs 2009 conference web site Program Committee * Clemens Ballarin, aicas GmbH * Gabriel Dos Reis, Texas A&M University (Co-Chair) * Jean-Christophe Filliâtre, CNRS Université Paris Sud * Predrag Janicic, University of Belgrade * Jaakko Järvi, Texas A&M University * Florina Piroi, Johannes Kepler University * Laurent Théry, INRIA Sophia Antipolis (Co-Chair) * Makarius Wenzel, Tec
Re: [Caml-list] ocamlgraph ConcreteBidirectional and Dot
Hi, Sorry for the late answer... > I've a small problem with ocamlgraph. > I want to parse a dot graph into a ConcreteBidirectional. > > The problem is that the signature needed for Dot.Parse requires a function > edge, but I've no mean to specify a label (since it is unlabelled !!)... > > The functor for ConcreteBidirectional says E.t = (V.t * V.t), > but I don't quite understand the type of B.G.E.label ... You're right, some type information is missing and there is no way to instantiate the Dot functor with the current signature of ConcreteBidirectional. One easy patch (if you are compiling ocamlgraph from sources) is to add the constraint ... and type E.label = unit to the signature of functor ConcreteBidirectional. I think we'll do that in the next release of ocamlgraph (and similarly for other unlabeled graph data structures provided in ocamlgraph). Hope this helps, -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs