Hello

Here is the latest OCaml Weekly News, for the week of December 03 to 10, 2013.

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-12/msg00035.html

It is with great sadness that I am writing to inform that Wojciech Daniel Meyer, who was known in the OCaml community, passed away 18th November 2013 at the age of 32.

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-12/msg00053.html

I am at a loss as to the difference between ['a.] syntax and [type a.] syntax of introducing polymorphic recursion. I will provide some examples. (Bear with me, they are automatically generated.) >>> type _ term = | Lit : integer -> integer term | Plus : integer term * integer term -> integer term | IsZero : integer term -> boolean term | If : (*∀'a.*)boolean term * 'a term * 'a term -> 'a term and integer and boolean external plus : (integer -> integer -> integer) = "plus" external is_zero : (integer -> boolean) = "is_zero" external if_then : (boolean -> 'a -> 'a -> 'a) = "if_then" let rec eval : 'a . ('a term -> 'a) = (function Lit i -> i | IsZero x -> is_zero (eval x) | Plus (x, y) -> plus (eval x) (eval y) | If (b, t, e) -> if_then (eval b) (eval t) (eval e)) <<< The above produces: Error: This pattern matches values of type boolean term but a pattern was expected which matches values of type integer term Type boolean is not compatible with type integer but if we replace the corresponding line with: >>> ... let rec eval : type a . (a term -> a) = ... <<< then it compiles fine. Now to a more complex example. According to my understanding (and InvarGenT), the following code should type-check: >>> type _ place = | LocA : a place | LocB : b place and a and b type (_, _) nearby = | Here : (*∀'b.*)'b place * 'b place -> ('b, 'b) nearby | Transitive : (*∀'a, 'b, 'c.*)('a, 'b) nearby * ('b, 'c) nearby -> ('a, 'c) nearby type boolean external is_nearby : (('a, 'b) nearby -> boolean) = "is_nearby" type _ ex1 = | Ex1 : (*∀'a, 'b.*)('b place * ('a, 'b) nearby) -> 'a ex1 external wander : ('a place -> 'a ex1) = "wander" type (_, _) meet = | Same : (*∀'b.*) ('b, 'b) meet | NotSame : (*∀'a, 'b.*) ('a, 'b) meet external compare : ('a place -> 'b place -> ('a, 'b) meet) = "compare" let rec walk : type a b . (a place -> b place -> (a, b) nearby) = (fun x goal -> ((function Same -> Here (x, goal) | NotSame -> let Ex1 ((y, to_y)) = wander x in Transitive (to_y, walk y goal))) (compare x goal)) <<< Here we get Error: This expression has type b place but an expression was expected of type a place Type b is not compatible with type a And when we switch to the ['a.] syntax, we get Error: This definition has type 'a. 'a place -> 'a place -> ('a, 'a) nearby which is less general than 'a 'b. 'a place -> 'b place -> ('a, 'b) nearby Thanks in advance for any thoughts. If you are curious, the source code is: https://github.com/lukstafi/invargent/blob/master/examples/simple_eval.gadt https://github.com/lukstafi/invargent/blob/master/examples/equational_reas.gadt

TL;DR: you should use those "rigid variables" to annotate type variable that will be refined in a GADT pattern matching. The way GADT type variables can be refined with different types in each branches is different and orthogonal to the type unification mechanism. Variables ('a) use type unification on each branch, which fails with the error you observe. Local type constructors (a), and only them, can be refined in GADT clauses, so that type refinement works. The syntax let rec f : type a . a -> ... = fun x -> ... as opposed to let rec f (type a) (x : a) ... = ... combines the GADT-readiness of those weird variables with polymorphic recursion -- which is orthogonal, but in practice they often come together. For more technical details, see "Ambivalent types for type inference with GADTs", by Jacques Garrigue and Didier Rémy, 2013: http://gallium.inria.fr/~remy/gadts/Garrigue-Remy:gadts@short2013.pdf

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/. Mirage 1.0: not just a hallucination!: http://openmirage.org/blog/announcing-mirage10 RWO tidbits: the runtime: https://ocaml.janestreet.com/?q=node/119

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.