[Caml-list] Re: Stricter version of #use ?
Hi John, On 3/25/2009 1:14 AM, Harrison, John R wrote: So with my root.ml and branch.ml files from the first message, it all works exactly as I wanted, a nice early failure with a clear traceback: # #use root.ml;; val x : int = 1 val u : int = 3 Exception: Failure X. Error in included file branch.ml # x;; - : int = 1 # u;; - : int = 3 Yet if I replace the line #use branch.ml;; in root.ml with what I supposed would be equivalent: use_file branch.ml;; then the exception propagates out and I get the rollback that I wanted to avoid: # #use root.ml;; val x : int = 1 val u : int = 3 Exception: Failure X. Error in included file branch.ml Exception: Pervasives.Exit. # x;; - : int = 1 # u;; Unbound value u Any idea why that should be? The execution difference between a toplevel phrase like use_file xxx and a toplevel directive like #use xxx is subtle. The current toplevel implementation always execute a toplevel phrase in a protected environment, i.e. the execution effect of a single toplevel phrase is always all-or-nothing. And this is, AFAIK, hard-wired in the code and I don't know how to tweak it without modifying the toplevel source. On the other hand, the toplevel won't protect the execution of a directive, rather it relies on the directives to protect themselves --- that's why we can still do some little trick without modifying the toplevel source. So in the end, you can't partly keep the execution effect of a toplevel phrase like use_file xxx. Moreover, I can't see how we can avoid this (if we intend to use use_file as a function rather than a directive), no matter how we define use_file. If the use_file fails upon some inside errors, the whole effect of its execution will be aborted due to the protected environment; if we catch the errors ourselves, i.e. the whole execution still returns successfully despite the inside error, then the rest of the code (below use_file xxx) will continue to run. The only solution (without modifying toplevel) is to define use_file as a function always succeeds and returns a flag telling whether the execution is all successful. Then it will be the responsibility of programmers to decide to abort or continue or reset. Something like: val use_file: string - (unit - unit) option it returns either None on full success or Some reset to let the programmers choose whether to abort (raise Exit) or (reset ()). Regards -- Zheng ___ 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] First release of focalize, a development environment for high integrity programs.
On 2009-03-24, at 11:55, David MENTRE wrote: For those interested in such details, FoCaLize seems to be under a BSD-like license (I have not made a detailed review of the code). I would be interested to know if knowledged people (e.g. Debian developers ;-) consider this code Free Software or not. In my (off-topic for this list) opinion, this whole licence business is totally out of control because lawyers have succeeded in scaring everyone witless about it. For example, I don't understand why you would need a detailed review of the code in order to notice that the licence (which you quoted) is an exact copy of the new BSD licence (straight from www.opensource.org, IIRC). Whether you (or the Debian developers, Microsoft management, or whoever else) choose to call it Free is a matter of political opinion and debate on this topic is usually a waste of time. This was my license rant for 2009. Thanks for your attention. -- Damien ___ 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] Question about the -dlambda option of ocamlc/ocamlopt
Alp Mestan a écrit : Hi, I'm currently studying the lambda code generation phase of the standard OCaml compiler. You can take a look at this for an example : http://blog.mestan.fr/2009/03/22/ocaml-and-dlambda-1/ I'm wondering what is 'makeblock' for ? And why is there '/a number' after every variable/function name ? Isn't the name sufficient for identifying variables ? Thanks ! If I recall correctly, makeblock is for block allocation and is used to make empty blocks for everything that does not fit in just one integer. The /a number is used to uniquely identify identifiers. In this example : let x = 1 in let x = 2 in x The /a number allows you to know which let variable is represented by the x at the end. -- Romain Bardou ___ 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] Question about the -dlambda option of ocamlc/ocamlopt
Thanks Romain ! On Wed, Mar 25, 2009 at 10:02 AM, Romain Bardou romain.bar...@lri.frwrote: Alp Mestan a écrit : Hi, I'm currently studying the lambda code generation phase of the standard OCaml compiler. You can take a look at this for an example : http://blog.mestan.fr/2009/03/22/ocaml-and-dlambda-1/ I'm wondering what is 'makeblock' for ? And why is there '/a number' after every variable/function name ? Isn't the name sufficient for identifying variables ? Thanks ! If I recall correctly, makeblock is for block allocation and is used to make empty blocks for everything that does not fit in just one integer. The /a number is used to uniquely identify identifiers. In this example : let x = 1 in let x = 2 in x The /a number allows you to know which let variable is represented by the x at the end. -- Romain Bardou -- Alp Mestan In charge of the C++ section on Developpez.com. ___ 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] in_channel_of_descr questions
Hello, I have some questions concerning in_channel_of_descr: my program has a list of sockets. I need the sockets itself for a select-Loop and an in_channel for the convenient input_line function. At the end, which one should i close? Just the socket, just the channel or both? On Windows I tried to create many in_channels, one for each block I read. Then I get soon an Too many open files in the system error. In win32unix/channels.c I see an _open_osfhandle() call for each in_channel_of_descr. On unix the same program runs fine (as expected). So is there a different approach needed for windows e.g. close just the socket on unix, but close socket and in_channel on windows? (In any case I'll remove the repeated call of in_channel_of_descr...). Thanks for help, Christoph Bauer ___ 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] in_channel_of_descr questions
Hi, On Wed, Mar 25, 2009 at 13:37, Christoph Bauer christoph.ba...@lmsintl.com wrote: Hello, I have some questions concerning in_channel_of_descr: my program has a list of sockets. I need the sockets itself for a select-Loop and an in_channel for the convenient input_line function. At the end, which one should i close? Just the socket, just the channel or both? On unix, you should close either one of them, but not both. The filedescriptor is shared, so closing the socket or the channel will close the file descriptor. On Windows I tried to create many in_channels, one for each block I read. Then I get soon an Too many open files in the system error. In win32unix/channels.c I see an _open_osfhandle() call for each in_channel_of_descr. On unix the same program runs fine (as expected). So is there a different approach needed for windows e.g. close just the socket on unix, but close socket and in_channel on windows? (In any case I'll remove the repeated call of in_channel_of_descr...). yes on windows, you need to close the channel. Calling in_channel_of_descr will indeed call _open_osfhandle() which allocates an integer fd in the C runtime to represent the Win32 handle. If you close the socket and not the channel, this CRT fd stays allocated and you eventually run out of fd. If you close the channel, the CRT fd will be closed, and that will close the Win32 handle too. -- Olivier ___ 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] First release of focalize, a development environment for high integrity programs.
Hello, On Wed, Mar 25, 2009 at 10:02, Damien Doligez damien.doli...@inria.fr wrote: For example, I don't understand why you would need a detailed review of the code in order to notice that the licence (which you quoted) is an exact copy of the new BSD licence (straight from www.opensource.org, IIRC). I already acknowledged that I should have noticed that the license is an exact copy of the new BSD license. However, from past experience, it happens that such software coming from a national or european project with multiple contributors might mix multiple (and even incompatible) licenses for the different part of the code. Thus my question regarding code review. (I'm *not* saying this is the case for Focalize) Whether you (or the Debian developers, Microsoft management, or whoever else) choose to call it Free is a matter of political opinion and debate on this topic is usually a waste of time. I entirely agree (for caml-list@). I'll should have avoided this part of the question. formal tools rant for 2009 Formal verification tools have such a high cost to learn and use them that I personally won't *consider* them if they not Free Software (according to FSF or Debian). It is hard enough to convince colleagues and management of the usefulness of such tools without being annoyed by restriction of use. /rant 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] qt / windows gui
Are there OCaml bindings for QT? Would OCaml + QT be a good option for a Windows app? I don't want to go with F# and do want to keep development on the Mac. Thanks, Joel --- http://linkedin.com/in/joelreymont ___ 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] WMM'09 call for papers
Call for Papers 4rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory Edinburgh, Scotland Co-located with ICFP'09. http://www.cis.upenn.edu/~sweirich/wmm/ Important Dates * Submission deadline: 19 June 2009 * Author Notification: 24 July 2009 * Workshop: 4 September 2009 Workshop Description Researchers in programming languages have long felt the need for tools to help formalize and check their work. With advances in language technology demanding deep understanding of ever larger and more complex languages, this need has become urgent. There are a number of automated proof assistants being developed within the theorem proving community that seem ready or nearly ready to be applied in this domain-yet, despite numerous individual efforts in this direction, the use of proof assistants in programming language research is still not commonplace: the available tools are confusingly diverse, difficult to learn, inadequately documented, and lacking in specific library facilities required for work in programming languages. The goal of this workshop is to bring together researchers who have experience using automated proof assistants for programming language metatheory, and those who are interested in using tool support for formalizing their work. One starting point for discussion will be the obstacles that hinder mechanization (whether they be pragmatic or technical), and what users and developers can do to overcome them. Format The workshop will consist of presentations by the participants, selected from submitted abstracts. It will focus on providing a fruitful environment for interaction and presentation of ongoing work. Participants are invited to submit working notes, source files, and abstracts for distribution to the attendees, but as the workshop has no formal proceedings, contributions may still be submitted for publication elsewhere. (See the SIGPLAN republication policy for more details.) Scope The scope of the workshop includes, but is not limited to: * Tool demonstrations: proof assistants, logical frameworks, visualizers, etc. * Libraries for programming language metatheory. * Formalization techniques, especially with respect to binding issues. * Analysis and comparison of solutions to the POPLmark challenge. * Examples of formalized programming language metatheory. * Proposals for new challenge problems that benchmark programming language work. Submission Guidelines Email submissions to urbanc AT in.tum.de. Submissions should be no longer than two pages in PDF and printable on A4 sized paper. Persons for whom this poses a hardship should contact the program chair. Conference Organization Program Committee * Nick Benton, Microsoft Research Cambridge * Olivier Danvy, University of Aarhus * Daniel Licata, Carnegie Mellon University * Francois Pottier, INRIA Paris-Rocquencourt * Christian Urban, TU Munich (chair) Workshop Organizers * Karl Crary, Carnegie Mellon University * Michael Norrish, National ICT Australia * Stephanie Weirich, University of Pennsylvania Previous Workshops * Victoria, 2008 * Freiburg, 2007 * Portland, 2006 This message was sent using IMP, the Internet Messaging Program. ___ 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] can anyone replicate this camlp4 problem?
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Hi, camlp4 seems to break parsing of object duplication on 3.11. Can anyone
replicate this problem? Is this an known issue? A quick google search did
not reveal anything..
Peng
Objective Caml version 3.11.0
# #use topfind;;
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
# #camlp4o;;
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/dynlink.cma: loaded
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/camlp4: added to search path
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/camlp4/camlp4o.cma: loaded
Camlp4 Parsing version 3.11.0
# class functional_point x y = object
val x = x
val y = y
method get_x = x
method get_y = y
method move dx dy = { x = x + dx; y = y + dy }
end;;
Characters 138-144:
method move dx dy = { x = x + dx; y = y + dy }
^^
Warning S: this expression should have type unit.
Characters 146-156:
method move dx dy = { x = x + dx; y = y + dy }
^^
Error: This expression has type bool but is here used with type int
#
-BEGIN PGP SIGNATURE-
Version: GnuPG v2.0.7 (GNU/Linux)
iD8DBQFJyoxPfIRcEFL/JewRAg8TAKCjoxTmDmfLxVHa7sXq0tGlt2rKDgCgp/C2
nc4vnKWkTvKXeR4Q0z4XB94=
=IwA+
-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: [Caml-list] can anyone replicate this camlp4 problem?
On Mar 25, 2009, at 3:55 PM, Peng Zang wrote:
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Hi, camlp4 seems to break parsing of object duplication on 3.11.
Can anyone
replicate this problem? Is this an known issue? A quick google
search did
not reveal anything..
Yeah. I reported the bug here:
http://caml.inria.fr/mantis/view.php?id=4673
Andres
Peng
Objective Caml version 3.11.0
# #use topfind;;
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
# #camlp4o;;
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/dynlink.cma: loaded
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/camlp4: added to
search path
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/camlp4/camlp4o.cma:
loaded
Camlp4 Parsing version 3.11.0
# class functional_point x y = object
val x = x
val y = y
method get_x = x
method get_y = y
method move dx dy = { x = x + dx; y = y + dy }
end;;
Characters 138-144:
method move dx dy = { x = x + dx; y = y + dy }
^^
Warning S: this expression should have type unit.
Characters 146-156:
method move dx dy = { x = x + dx; y = y + dy }
^^
Error: This expression has type bool but is here used with type int
#
-BEGIN PGP SIGNATURE-
Version: GnuPG v2.0.7 (GNU/Linux)
iD8DBQFJyoxPfIRcEFL/JewRAg8TAKCjoxTmDmfLxVHa7sXq0tGlt2rKDgCgp/C2
nc4vnKWkTvKXeR4Q0z4XB94=
=IwA+
-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
___
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] can anyone replicate this camlp4 problem?
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
I only know of the brute force update which is less than desirable:
class test (x : int) = object
val a = x;
val b = x;
method add (d:int) =
let copy = {} in
let arr : int array = Obj.magic copy in
arr.(2) - arr.(2) + d;
arr.(3) - arr.(3) + d;
copy
method print = Format.printf %d %d a b
end
But my brain is fried and I can't think of a nicer way..
Peng
On Wednesday 25 March 2009 04:15:38 pm Peng Zang wrote:
Thanks, do you know of a good work around?
Peng
On Wednesday 25 March 2009 04:01:24 pm Andres Varon wrote:
On Mar 25, 2009, at 3:55 PM, Peng Zang wrote:
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Hi, camlp4 seems to break parsing of object duplication on 3.11.
Can anyone
replicate this problem? Is this an known issue? A quick google
search did
not reveal anything..
Yeah. I reported the bug here:
http://caml.inria.fr/mantis/view.php?id=4673
Andres
Peng
Objective Caml version 3.11.0
# #use topfind;;
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
# #camlp4o;;
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/dynlink.cma: loaded
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/camlp4: added to
search path
/home/peng/app-data/godi-3.11/lib/ocaml/std-lib/camlp4/camlp4o.cma:
loaded
Camlp4 Parsing version 3.11.0
# class functional_point x y = object
val x = x
val y = y
method get_x = x
method get_y = y
method move dx dy = { x = x + dx; y = y + dy }
end;;
Characters 138-144:
method move dx dy = { x = x + dx; y = y + dy }
^^
Warning S: this expression should have type unit.
Characters 146-156:
method move dx dy = { x = x + dx; y = y + dy }
^^
Error: This expression has type bool but is here used with type int
#
-BEGIN PGP SIGNATURE-
Version: GnuPG v2.0.7 (GNU/Linux)
iD8DBQFJyoxPfIRcEFL/JewRAg8TAKCjoxTmDmfLxVHa7sXq0tGlt2rKDgCgp/C2
nc4vnKWkTvKXeR4Q0z4XB94=
=IwA+
-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
-BEGIN PGP SIGNATURE-
Version: GnuPG v2.0.7 (GNU/Linux)
iD8DBQFJypNGfIRcEFL/JewRAtIOAJ9xEOuh4XNivJkjKZZ1uTYmONGzZQCfQAZH
4UBdyDEFCYNJ6wH4ZG8zpzU=
=twIi
-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
[Caml-list] polymorphic variants and recursive functions
I stumbled upon a little puzzle that I can't quite work out. I'm trying to use polymorphic variants as phantom types and in one particular situation involving a polymorphic type with an invariant type parameter (Lwt.t) the compiler is unhappy with a set of mutually recursive functions. I can appreciate at some level that an invariant type parameter will cause the phantom types to become unsatisfied, but in this particular case my sense is that they should be satisfiable, and feel that I might be overlooking an appropriate coercion. Perhaps someone here can lend a hand... Here's the best I can do at creating a simple example: First, here's the case the works... I would like a family of constructors, including two higher-order ones, 'arr' and 'obj', such that 'arr' can only be constructed from 'obj' instances: let obj (v:[ `V]) : [`O|`V] = `V let arr (v:[ `O]) : [`V]= `V let v0 : [`V]= `V This works as expected: let ok1 = obj v0 let ok2 = arr (obj v0) let ok3 = obj (arr (obj v0)) and fails as expected: let fail1 = arr v0 ^^ This expression has type [ `V ] but is here used with type [ `O ] The first variant type does not allow tag(s) `O I can now use these constructors in conjunction with some mutually- recursive functions (coercions are needed): let rec eval = function | `Arr v - (eval_arr v : [`V]: [ `V]) | `Obj v - (eval_obj v : [`V|`O] : [ `V]) and eval_arr v = arr (eval_obj v) and eval_obj v = obj (eval v) although oddly, the coercions don't seem to affect the final type of eval: val eval : ([ `Arr of 'a | `Obj of 'a ] as 'a) - [ `O | `V ] = fun val eval_arr : ([ `Arr of 'a | `Obj of 'a ] as 'a) - [ `V ] = fun val eval_obj : ([ `Arr of 'a | `Obj of 'a ] as 'a) - [ `O | `V ] = fun Now the case that doesn't work: Introducing 'a Lwt.t into the above: open Lwt let obj (v:[ `V]) : [`O|`V] Lwt.t = return `V let arr (v:[ `O]) : [`V] Lwt.t= return `V let v0 : [`V] Lwt.t= return `V let ok1 = v0 = obj let ok2 = v0 = obj = arr let ok3 = v0 = obj = arr = obj (*let fail1 = v0 = arr*) let rec eval = function | `Arr v - (eval_arr v : [`V] Lwt.t: [ `V] Lwt.t) | `Obj v - (eval_obj v : [`V|`O] Lwt.t : [ `V] Lwt.t) and eval_arr v = eval_obj v = arr and eval_obj v = eval v = obj | `Obj v - (eval_obj v : [`V|`O] Lwt.t : [ `V] Lwt.t) ^^ This expression has type [ `O | `V ] Lwt.t but is here used with type [ `V ] Lwt.t The second variant type does not allow tag(s) `O Any suggestions would be much appreciated, Warren ___ 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] polymorphic variants and recursive functions
On Wed, Mar 25, 2009 at 02:39:28PM -0700, Warren Harris wrote: let rec eval = function | `Arr v - (eval_arr v : [`V] Lwt.t: [ `V] Lwt.t) | `Obj v - (eval_obj v : [`V|`O] Lwt.t : [ `V] Lwt.t) and eval_arr v = eval_obj v = arr and eval_obj v = eval v = obj | `Obj v - (eval_obj v : [`V|`O] Lwt.t : [ `V] Lwt.t) ^^ This expression has type [ `O | `V ] Lwt.t but is here used with type [ `V ] Lwt.t The second variant type does not allow tag(s) `O The Lwt.t type is abstract and invariant since no annotation has been given for the type variable (you'd need it to be type +'a t): # let a : [`O] Lwt.t = return `O;; val a : [ `O ] Lwt.t = abstr # (a : [`O | `V] Lwt.t);; Error: Type [ `O ] Lwt.t is not a subtype of type [ `O | `V ] Lwt.t The first variant type does not allow tag(s) `V In your example, [ `V] Lwt.t in the second line becomes [`V] Lwt.t, (the type variable is not covariant) and you cannot do [`V | `O] Lwt.t : [`V] Lwt.t in the third line. Unfortunately, the type variable is in both variant and contravariant position in the definition of Lwt.t... -- Mauricio Fernandez - http://eigenclass.org ___ 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] Automated Reasoning Workshop 2009 - 2nd Call for Papers
** Please excuse multiple posts and distribute as widely as possible ** CALL FOR PAPERS 2009 Workshop on Automated Reasoning Bridging the Gap between Theory and Practice http://www.csc.liv.ac.uk/~arw09/ 21st - 22nd April 2009 University of Liverpool ** Deadline for submissions of extended abstracts: 31st March 2009 ** Topics -- The workshop will cover the full breadth and diversity of automated reasoning and will include topics such as: * Theorem proving in classical and non-classical logics * Reasoning systems and mechanisms: - Description logics - Equational reasoning, unification - Induction - Constraint Satisfaction - Combining reasoning systems - Specialised decision procedures * Formal methods in software analysis: - Verification - Formal Modelling * Non-classical inference: - Non-monotonic reasoning, abduction - Intuitionistic reasoning * Logic-based knowledge representation: - Ontology specification, - Domain specific reasoning (spatial, temporal, epistemic etc.) * Reasoning for agents (or about agents) * Interactive theorem proving * Implementation issues and empirical results * Applications of automated reasoning Submissions --- We invite the submission of camera-ready, two-page extended abstracts about recent work, work in progress, or a system description. The abstract can describe work that has already been published elsewhere. Anyone wishing to attend but not interested in presenting should send a shorter position statement (1/2 - 1 page). The main objective of the abstracts is to spread information about recent work in our community, and we expect to accept most on-topic submissions, but we may ask for revisions. To prepare your submission, please use the LaTeX style file provided on the workshop web page: http://www.csc.liv.ac.uk/~arw09/arw09_latex.tar Each submission should include thenames and complete addresses (including email) of all authors. Correspondence will be sent to the first author, unless otherwise indicated. Submissions should be sent in in either Postscript or PDF format by email to the workshop organisers at: u.hust...@liverpool.ac.uk Publication --- Abstracts will be published in informal workshop notes and be made available on the internet. Presentations - Each workshop attendee will be allocated a 5-10 minute slot (depending on time constraints), for a short talk to introduce their research. Each attendee will also be allocated space in a poster session, where they can further present and discuss their work. Please prepare posters for the event. Student Grants -- We have a limited number of grants available to PhD students who wish to attend ARW 2009. To indicate your interest please send a short email to the workshop organisers (u.hust...@liverpool.ac.uk) anytime before 10th April 2009. Important Dates --- Abstract submission: 31st March 2009 Notification of acceptance/rejection: 3rd April 2009 Final version due: 10th April 2009 Workshop: 21st - 22nd April 2009 Invited Speakers To be announced shortly. Program Committee - Clare Dixon(University of Liverpool) Jacques Fleuriot (University of Edinburgh) Alexander Bolotov (University of Westminster) Simon Colton (Imperial College London) David Crocker (Escher Technologies) Louise Dennis (University of Liverpool) Roy Dyckhoff (University of St Andrews) Ullrich Hustadt(University of Liverpool) Mateja Jamnik (Univerity of Cambridge) Tom Melham (University of Oxford) Alice Miller (University of Glasgow) Renate A. Schmidt (University of Manchester) Volker Sorge (University of Birmingham) Conference Venue The workshop will take place at the University of Liverpool on 21st and 22nd April 2009. Contact --- Please email Ullrich Hustadt (u.hust...@liverpool.ac.uk) if you have any queries about the 2009 Automated Reasoning Workshop. ___ 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] polymorphic variants and recursive functions (caml: to exclusive)
Mauricio, Thanks for your response... On Mar 25, 2009, at 4:24 PM, Mauricio Fernandez - m...@acm.org wrote: The Lwt.t type is abstract and invariant since no annotation has been given for the type variable (you'd need it to be type +'a t): ... Unfortunately, the type variable is in both variant and contravariant position in the definition of Lwt.t... Just to be sure I understand you... you're saying due to the definition/implementation of Lwt and the fact that the type parameter cannot be declared covariant, that what I'm trying to do with phantom types just can't work in this case. I was afraid of that. :-( Warren ___ 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
