Previous week Up Next week

Hello

Here is the latest OCaml Weekly News, for the week of March 17 to 24, 2015.

  1. GADT existential asked
  2. TLS-0.4.0 and X.509-0.3.0
  3. Adding support for OCaml in PythonTeX
  4. Mtime 0.8.0
  5. OPAM 1.2.1
  6. Other OCaml News

GADT existential asked

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-03/msg00105.html

Daniel Bünzli announced:
Is it possible to escape a GADT existential using some kind of witness
the same way a universal type would allow me ? I think the answer is
no, but I'd love to be proven wrong.
      
Milan Stanojević then asked and Daniel Bünzli replied:
> Can you give some hypothetical example code ?
type 'a key = ?
type binding = B : 'a key * 'a -> binding
type dict = binding list  
let lookup : dict -> 'a key -> 'a option = fun d k -> ?

Is it possible to specify a `'a key` type that allows `lookup` (with
the obvious semantics) to be written ? This is trivial to achieve with
a universal type, see http://mlton.org/PropertyList
      
Milan Stanojević then said:
This is doable in OCaml.
Core has one possible implementation.
https://github.com/janestreet/core_kernel/blob/master/lib/type_equal.mli#L171

type 'a key = 'a Type_equal.Id.t

let lookup dict key =
   List.find_map disct ~f:(function
    | B (key', a) ->
      match Type_equal.Id.same_witness key key' with
      | None -> None
      | Some T -> Some a)
;;

You can also check out Univ and Univ_map modules in Core.

Note that Univ was possible in OCaml even before first-class
modules, GADTs and extensible types (which are all used in Type_equal)

https://blogs.janestreet.com/a-universal-type/
      
Daniel Bünzli then replied:
Cool, a new trick. My understanding of this is basically to apply to
types the same idea as Univ by representing them as a first class
module.

However are you sure your example compiles (tried to check, but Core
fails on me in the toplevel) ? Trying the following [1] self-contained
implementation of the idea [1] the compiler still complains about
escaping types.

> Note that Univ was possible in OCaml even before first-class
> modules, GADTs and extensible types (which are all used in Type_equal)

Yes, see http://alan.petitepomme.net/cwn/2010.02.09.html#1 if you are interested how.  

Thanks,

Daniel

[1]

module Key = struct
  type _ t = ..
end

module type W = sig
  type t
  type _ Key.t += Key : t Key.t
end

type 'a witness = (module W with type t = 'a)

let witness () (type s) =
 let module M = struct
   type t = s
   type _ Key.t += Key : t Key.t
 end
 in
 (module M : W with type t = s)

type ('a, 'b) eq = Eq : ('a, 'a) eq

let eq (type r) (type s) (r : r witness) (s : s witness)
  : (r, s) eq option
  =
  let module R = (val r : W with type t = r) in
  let module S = (val s : W with type t = s) in
  match R.Key with
  | S.Key -> Some Eq
  | _ -> None

type 'a key = 'a witness
type binding = B : 'a key * 'a -> binding
type dict = binding list

let lookup : dict -> 'a key -> 'a option = fun d k ->
  let rec find = function
  | [] -> None
  | B (k', v) :: bs ->
      match eq k k' with
      | None -> find bs
      | Some Eq -> Some v
  in
  find d
      
Jeremy Yallop then said:
This needs a locally-abstract type ("type a. ") to allow type
refinement when you match against the GADT

   let lookup : type a. dict -> a key -> a option = fun d k ->

and an additional annotation for the inner function:

  let rec find : dict -> a option = function
      
Much later in the discussion, Jeremy Yallop said and Alain Frisch replied:
> The exn type doesn't support GADT
> constructors (since it doesn't have type parameters)

Note that even if exn doesn't have type parameters, it supports the
GADT syntax to define constructors with existentials:


exception A: 'a * ('a -> string) -> exn;;
      

TLS-0.4.0 and X.509-0.3.0

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-03/msg00118.html

Hannes Mehnert announced:
it is my please to announce new releases of TLS and X.509, both purely
developed in OCaml.  Today OpenSSL announced 14 security issues in
their code base, thus I thought it would be a good day to release our
TLS library :)

The bounty of 10 Bitcoins is still ongoing and not broken (although
~20000 TLS connections were made) -- http://ownme.ipredator.se

NEWS:
TLS
* client authentication (both client and server side)
* server side SNI configuration (see sni.md)
* SCSV server-side downgrade prevention (contributed by Gabriel de
Perthuis @g2p #5)
* remove RC4 ciphers from default config #8
* support for AEAD ciphers, currently CCM #191
* proper bounds checking of handshake fragments #255
* disable application data between CCS and Finished #237
* remove secure renegotiation configuration option #256
* expose epoch in mirage interface, implement 2.3.0 API (error_message)
* error reporting (type failure in engine.mli) #246
* hook into Lwt event loop to feed RNG #254

X.509
* more detailed error messages (type certificate_failure modified)
* no longer Printf.printf debug messages
* error reporting: `Ok of certificate option | `Fail of
certificate_failure
* fingerprint verification can work with None as host (useful for
client authentication where host is not known upfront)
* API reshape: X509 is the only public module, X509.t is the abstract
certificate

Preliminary API documentation (pull requests welcome) is available now
at https://mirleft.github.io/ocaml-x509/ ;
https://mirleft.github.io/ocaml-tls/

The packages are not yet in the opam repository, but waiting for
Travis https://github.com/ocaml/opam-repository/pull/3770
      

Adding support for OCaml in PythonTeX

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-03/msg00083.html

Continuing the thread from last week, Thomas Gazagnaire said and Ashish Agarwal added:
> Maybe something like https://github.com/agarwal/oloop could help?
> 
> (I'm not one the author, and I have no idea what it does exactly)

The goal of oloop is to help authors of blog posts, books, etc.
include OCaml code blocks in their writing, and have the code
automatically evaluated through the toplevel. This is done for example
on OCaml.org, and we wanted to factor out that code and make it more
robust. If it can be extended in any way for other purposes, please
add an issue and/or submit a pull request.
      
Roberto Di Cosmo also said:
Well, an ugly but effective perl script has been used for ages for
doing this...

http://caml.inria.fr/pub/old_caml_site/caml-list-ar/0651.html

Many of us (including me) have a modified version adapted to their
LaTeX style.

If somebody takes the time to revamp all this, and properly package
it, with documentation, etc. , that would be really cool :-)
      

Mtime 0.8.0

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-03/msg00133.html

Daniel Bünzli announced:
It's my pleasure to announce the first release of Mtime, best described as:

 Mtime is an OCaml module to access monotonic wall-clock time. It
 allows to measure time spans without being subject to operating system
 calendar time adjustments.

 Mtime depends only on your platform system library. The optional
 JavaScript support depends on js_of_ocaml. It is distributed
 under the BSD3 license.
  
 Home page: http://erratique.ch/software/mtime
 API docs: http://erratique.ch/software/mtime/doc/Mtime
 Github mirror: https://github.com/dbuenzli/mtime

It should be available shortly in opam.

Best,

Daniel

P.S. Since I'm too tired to fight with build systems and packaging at
the moment jsoo is a hard dep and not a deptopt as it should be. This
will be fixed at some point in the future.

P.P.S. A Windows hacker is welcome for
https://github.com/dbuenzli/mtime/issues/2 as I don't have the time to
solve this right now.
      
Daniel Bünzli then added:
So should v0.8.1 which fixes a stupid arithmetic bug on 32-bit
platforms with a POSIX clock.

Thanks to Stephen Dolan for the report and the fix.
      

OPAM 1.2.1

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2015-03/msg00150.html

Louis Gesbert announced:
We're glad to announce the release of the version 1.2.1 of the OPAM
package manager. This point release features a number of stability
improvements, better processing of package operations, better
messages, and fixes.

See the announcement and get the update at
http://opam.ocaml.org/blog/opam-1-2-1-release/

Thanks to all the contributors, testers and issue reporters!
      

Other OCaml News

From the ocamlcore planet blog:
Thanks to Alp Mestan, we now include in the OCaml Weekly News the links to the
recent posts from the ocamlcore planet blog at http://planet.ocaml.org/.

Mini Cloud/Cluster v2.0:
  https://rwmj.wordpress.com/2015/03/23/mini-cloudcluster-v2-0/

A lighter Core:
  https://blogs.janestreet.com/a-lighter-core/

Part 3: Running your own DNS Resolver with MirageOS:
  http://hh360.user.srcf.net/blog/2015/03/part-3-running-your-own-dns-resolver-with-mirageos/

Namespace archeology:
  http://gallium.inria.fr/blog/namespace-archeology

Binomial Heap:
  http://typeocaml.com/2015/03/17/binomial-heap/

OPAM 1.2.1 Released:
  http://ocaml.org/
      

Old cwn

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.


Alan Schmitt