Hello

Here is the latest Caml Weekly News, for the week of June 25 to July 02, 2013.

- Spoc: GPGPU programming with OCaml
- Ocaml on windows
- meetup Paris-OCaml (OUPS) mardi 2 juillet
- Mixing two GADTs
- Request for feedback: A problem with injectivity and GADTs
- Other Caml News

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00156.html

I would like to present you a set of tools for GPGPU programming with OCaml. I developed the SPOC library that enables the detection and use of GPGPU devices with OCaml using Cuda and OpenCL. I also developed a camlp4 syntax extension to handle external Cuda or OpenCL kernels as well as a DSL to express GPGPU kernels from the OCaml code. http://www.algo-prog.info/spoc This work is a big part of my PhD thesis and was partially funded by the opengpu project. I'm currently in the UPMC-LIP6 laboratory where I'm supervised by Pr. E. Chailloux and Pr. J-L Lamotte. SPOC has been presented several times and the slides and the papers references are on our website if you want more information about it. It has currently been tested on multiple architectures and systems, mostly 64-bit Linux and 64-bit OSX systems. It should work with Windows too (I tested it successfully last year with Windows 7...). To be able to use SPOC, you'll need a computer capable of running OCaml (obviously) but also compatible with either OpenCL or Cuda. For Cuda you only need a current proprietary NVidia driver while for OpenCL you need to install the correct OpenCL implementation for your system. SPOC should compile anyway as everything is dynamically linked, but you'll need Cuda/OpenCL eventually to run your programs. SPOC currently lacks a real tutorial, it comes with some examples and I strongly advise anyone interested to look into the slides and papers on the website. By the way, if you are interested and if you are in Paris next week, I will be presenting SPOC etc. during the "OCaml Users in PariS" (OUPS) Meetup next Tuesday (July 2) . I hope to see some of you there and to have some feedback on this work. Mathias SPOC : http://www.algo-prog.info/spoc OpenGPU : http://opengpu.net OUPS : http://www.meetup.com/ocaml-paris/

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00169.html

> I am looking to develop a desktop application which will be distributed > to customers, so for now I think I will need ocaml libs like wxwidget, > batteries, sql lite db library, sockets, networking etc. > Is anyone using omake on windows? Does it have a dependency on Cygwin > like ocamlbuild? LexiFi uses omake on Windows and Linux. It does not depend on Cygwin itself, if you are careful enough to not use any Cygwin tool in the build rules, of course. omake actually implements a decent scripting language (with built-in versions of some useful tools). FWIW, we use a tool ( http://www.lexifi.com/csml ) to interact easily with the .Net framework, allowing our application to access .Net components. For instance, our Windows GUI is based on .Net Windows Forms and we use the .Net driver from Oracle. (For PostgreSQL, we use Markus' ocaml bindings to the native libpq library.)

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-07/msg00000.html

A short message in French, to give the program of the next OCaml-Paris meetup, tomorrow Tuesday, July 2, at 19:30 at IRILL : La prochaine rencontre du Meetup OCaml-Paris (OUPS) aura lieu le mardi 2 juillet, à l'IRILL, comme d'habitude, et devrait mettre l'accent sur des expériences de programmation en OCaml dans divers contexte. Au programme, à partir de 19h30 : - "Les GADT dans la pratique" (Pierre Chambart ou Gabriel Scherer) - "Programmation GPGPU en OCaml" (Mathias Bourgoin) - "Utiliser Js_of_ocaml pour enrichir une page web" (Çagdas Bozman) - "Expériences de contribution à Batteries" (Gabriel Scherer) Comme d'habitude, nous nous retrouverons ensuite pour discuter autour de boissons et de bonnes pizzas, offertes par LexiFi ! Inscrivez-vous nombreux ! http://www.meetup.com/ocaml-paris/events/121412532/

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-07/msg00001.html

Suppose I have the following two GADTs: type _ foo = A : int foo | B : string foo | C : bool foo type _ bar = X : int bar | Y : float bar | Z : string bar In my actual use case, these two GADTs cannot be altered. Suppose I then define the following two functions: let g : type s . s bar -> s = function X -> 42 | Y -> 42.0 | Z -> "42" let get1 : type s . s foo -> s = function A -> int_of_string (g Z) | B -> string_of_float (g Y) | C -> (=) 1 (g X) So far, so good. Now what I'd like to try to do is alter get1 to be of the form: let get2 : type s . s foo -> s = fun attr -> let (f, retr) = match attr with A -> (int_of_string, Z) | B -> (string_of_float, Y) | C -> ((=) 1, X) in f (g retr) Obviously, I need type annotations for f and retr. I'd tried: let get2 : type s . s foo -> s = fun attr -> let x : type t . (t -> s) * t bar = match attr with A -> (int_of_string, Z) | B -> (string_of_float, Y) | C -> ((=) 1, X) in let (f, retr) = x in f (g retr) But I get an error with int_of_string being of type string -> int instead of type t -> s. (Incidentally, the notation I expected to be able to use of [(let ((f, retr) : type t . (t -> s) * t bar)] resulted in a syntax error although looking at 7.13 in the manual, I think that's probably correct?) Is there a type annotation which will allow this to work? Any help (or a statement that this happens to be impossible!) much appreciated...

What you need is an existential quantification ("there exists some t such that x has type (t -> s) * t bar"). You can do this by wrapping the tuple in a third GADT: type 's baz = T: ('t -> 's) * 't bar -> 's baz let get2 : type s . s foo -> s = fun attr -> let x : s baz = match attr with | A -> T (int_of_string, Z) | B -> T (string_of_float, Y) | C -> T ((=) 1, X) in let (T (f, retr)) = x in f (g retr)

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-07/msg00003.html

> The fix is simple enough: we should track injectivity, and assume that abstract > types are not injective by default. > However, this also means that the first type I defined above (using Hashtbl.t) > will be refused. > > How many of you are using GADTs in this way, and how dependent are you on > abstract types ? FWIW, it turns out that we have very recently introduced such a case (and I realized it while synchronizing our version of OCaml with the trunk). We used to have a functor with this signature: module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) : sig module type S = sig type s type t val t: t ttype val eq: (s, t T.t) TypEq.t end val check: 'a ttype -> (module S with type s = 'a) option end ttype is our type representing type structures at runtime. The functors returns a function that checks if a given runtime type represents an instance of an unary abstract type constructor passed in argument to the functor (the functors check that this is indeed an abstract type). In case of success, the function returns the ttype of the type constructor argument. The existential is encoded with a first-class module and the type-equality is encoded in the classical way (('a, 'b) TypEq.t witnesses the equality of 'a and 'b: type (_, _) t = Eq: ('a, 'a) t). A GADT was recently introduced to replace this with a more direct representation: module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) : sig type _ is_t = Is: 'a ttype -> 'a T.t is_t val check: 'a ttype -> 'a is_t option end The problem is that this doesn't work any more (because T.t is not injective). For now, I think I'll use: module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) : sig type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t val is_t: 'a ttype -> 'a is_t option end which is accepted and roughly equivalent (by opening the equality witness, one can retrieve the static equality 'a == 'b T.t).

Nice natural example, and nice workaround. Of course, this is not strictly equivalent. For instance suppose the following function: let f (type a) (tt : a T.t ttype) = match check tt with None -> assert false | Some (Is (tta, Eq)) -> (tta : a ttype) The pattern matching will succeed, but tta will only have type "a ttype" if T.t is injective. The nice part is that this is delayed to the use site, where we may have more information about T.t, so this trick may still be useful after introducing injectivity annotations. Anyway, I suppose that this will work fine for you: check is intended to be called on unknown types, so the missing equality should not be a problem.

Thanks to Alp Mestan, we now include in the Caml Weekly News the links to the recent posts from the ocamlcore planet blog at http://planet.ocaml.org/. News from May and June: http://www.ocamlpro.com/blog/2013/07/01/monthly-06.html Coq received ACM SIGPLAN Programming Languages Software 2013 award: http://coq.inria.fr/coq-received-acm-sigplan-programming-languages-software-2013-award Full Time: Senior Functional Programmer at Bloomberg L.P. in Lexington, NY: http://jobs.github.com/positions/78c69f44-e031-11e2-97c6-4063613e594f Typestate in Mezzo? Starting with list iterators.: http://gallium.inria.fr/blog/typestate-in-mezzo-mutable-list-iterators Flowing faster: lein-gnome: http://scattered-thoughts.net/blog/2013/06/25/flowing-faster-lein-gnome/

If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.

If you also wish to receive it every week by mail, you may subscribe online.