|
|

# Attn: Development Editor, Latest OCaml Weekly News

 From: Alan Schmitt To: "lwn" , "cwn" Subject: Attn: Development Editor, Latest OCaml Weekly News Date: Tue, 10 Dec 2013 14:04:15 +0100 Message-ID: Archive-link: Article

Hello,

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

1) Wojciech Meyer
3) Other Caml News

========================================================================
1) Wojciech Meyer
Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-12/msg000...>
------------------------------------------------------------------------
** Vitaly S. Lugovskiy gave some sad news:

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/msg000...>
------------------------------------------------------------------------

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/example...>
<https://github.com/lukstafi/invargent/blob/master/example...>

** Gabriel Scherer replied:

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) ... = ...
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:

========================================================================
3) 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/>.

Mirage 1.0: not just a hallucination!:
<http://openmirage.org/blog/announcing-mirage10>

RWO tidbits: the runtime:
<https://ocaml.janestreet.com/?q=node/119>

========================================================================
Old cwn
------------------------------------------------------------------------

If you happen to miss a CWN, you can send me a message
(alan.schmitt@polytechnique.org) and I'll mail it to you, or go take a look at
the archive (<http://alan.petitepomme.net/cwn/>) or the RSS feed of the
archives (<http://alan.petitepomme.net/cwn/cwn.rss>). If you also wish
to receive it every week by mail, you may subscribe online at
<http://lists.idyll.org/listinfo/caml-news-weekly/> .

========================================================================