```
Gabriel has given an excellent explanation, it is hard to add
anything. Yet I will still try.
> module F : sig
> type ('f, 'r) t
> val z : ('r, 'r) t
> val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t
> end = struct
> type ('f, 'r) t =
> | Z : ('r, 'r) t
> | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t
> let z = Z
> let (//) t f = S (t, f)
> end
Perhaps it will be easier to work out the types if we don't use
GADTs. They are not necessary in your example (and not needed for
the typed printf either).
Here is the adjusted code
module F : sig
type ('f, 'r) t
val z : ('r, 'r) t
val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t
val bind : 'f -> ('f, 'r) t -> 'r
end = struct
type ('f, 'r) t = 'f -> 'r
let z = fun x -> x
(* the type annotations are all optional. They are given to show
which subexpressions have which types, and let the compiler confirm
that.
Alas, attaching type annotations requires too many parentheses
*)
let (//) : type a r f. (f, a -> r) t -> (unit -> a) -> (f, r) t =
fun t th ->
fun (f:f) -> ((((t f):(a->r)) (th () : a)) : r)
let bind f t = t f
end
let exp1 = F.(z // (fun () -> Int32.zero) // (fun () -> ""));;
(*
val exp1 : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr>
*)
Just for reference, here is the implementation for the opposite order,
suggested by Gabriel.
module G : sig
type ('f, 'r) t
val z : ('r, 'r) t
val (//) : ('f, 'r) t -> (unit -> 'a) -> ('a -> 'f, 'r) t
val bind : 'f -> ('f, 'r) t -> 'r
end = struct
type ('f, 'r) t = {e: 'w. ('r -> 'w) -> ('f -> 'w)}
let z = {e = fun x -> x}
(* the type annotations are all optional. They are given to show
which subexpressions have which types, and let the compiler confirm
that
Alas, attaching type annotations requires too many parentheses
*)
let (//) : type a r f. (f, r) t -> (unit -> a) -> (a->f, r) t =
fun t th ->
{e = fun (type w) (k:(r->w)) -> fun (af:a->f) ->
((((t.e k):(f -> w)) ((af (th ())):f)):w)}
let bind f t = t.e (fun x -> x) f
end
let test = G.(z // (fun () -> 3l) // (fun () -> "foo"));;
(* val test : (string -> int32 -> '_weak2, '_weak2) G.t = <abstr> *)
;;
```

[-- Attachment #1: Type: text/plain, Size: 10489 bytes --] > (You could try to write conversion functions between those two definitions > to convince yourself that they are morally equivalent, > but this is actually a difficult exercise.) type (_, _) t1 = | Z : ('f, 'f) t1 | S : (('f, 'a -> 'r) t1 * (unit -> 'a)) -> ('f, 'r) t1 type (_, _) t2 = | Z : ('r, 'r) t2 | S : ('f, 'r) t2 * (unit -> 'a) -> ('a -> 'f, 'r) t2 t2 is t1 "upside down" (and conversely). To go from t1 to t2 is thus a "reverse" operation. Just like for lists, writing "reverse" directly is difficult, but one can use an auxiliary function let rec rev_append : type a b c. (b, c) t2 -> (a, b) t1 -> (a, c) t2 On Fri, Sep 20, 2019 at 10:35 AM Gabriel Scherer <gabriel.scherer@gmail.com> wrote: > There is a direct relation between how type evolve during GADT typing and > how queries evolve during logic/relational programming. It can help to > think of a GADT declaration as the set of rules of a Prolog program. (I you > have never looked at Prolog, here is an occasion to learn something new). > That does *not* mean that GADTs let you do prolog-style programming in > types (the compiler will not automatically search for a proof, the user has > to write it down explicitly as a GADT term, so this work is not done > implicitly, as with type-class search for example), but it does give a way > to think about GADT declarations. > > Your declaration (notice that I renamed the Z variable, for a good reason > that will appear clear below): > > type (_, _) t = > | Z : ('f, 'f) t > | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t > > becomes > > t F F. > t F R :- t F (A -> R), (unit -> A). > > In any case, your declaration has the following effect: > - by the Z rule, all types of the form > ('a1 -> 'a2 -> ... -> 'an -> 'r, 'a -> 'a2 -> ... -> 'an -> 'r) t > are inhabited > - by the S rule, you can "hide" an element on the right > (and you have to provide a thunk for it) > , moving from > ('a1 -> ... -> 'an -> r, 'ak -> 'a{k+1} -> .. -> 'an -> r) t > to > ('a1 -> ... -> 'an -> r, 'a{k+1} -> .. -> 'an -> r) t > > If you do this repeatedly you end up on what you want: ('a1 -> .. -> 'an > -> r, r) t. > > The way you write about it, it sounds like you had the following > *different* definition in mind > > type (_, _) t = > | Z : ('r, 'r) t > | S : ('f, 'r) t * (unit -> 'a) -> ('a -> 'f, 'r) t > > let test = S (S (Z, (fun () -> 3l)), (fun () -> "foo")) > > corresponding to the following Prolog program that I do find easier to > think about: > > t R R. > t (A -> F) R :- t F R, (unit -> A). > > It turns out that with this other definition, the first implementation > that you had written actually type-check fines. > > (You could try to write conversion functions between those two definitions > to convince yourself that they are morally equivalent, but this is actually > a difficult exercise.) > > On Fri, Sep 20, 2019 at 10:11 AM Malcolm Matalka <mmatalka@gmail.com> > wrote: > >> >> Gabriel Scherer <gabriel.scherer@gmail.com> writes: >> >> > Note: the reason why you get _weak type variables (which are not >> > polymorphic, just not-inferred-yet) is that the type-checker cannot >> detect >> > that (z // (fun () -> ...)) is a value: it would have to unfold the >> call to >> > (//) for this, which it doesn't do in general, and here certainly could >> not >> > do given that its definition is hidden behind an abstraction boundary. >> > I would recommend experimenting *without* the module interface and the >> > auxiliary function, with the constructors directly, you would get >> slightly >> > better types. >> > >> > # S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));; >> > - : (int32 -> string -> 'a, 'a) t = S (S (Z, <fun>), <fun>) >> > >> > Historically we have used module interfaces to implement "phantom >> types" -- >> > because the type information there is only present in the interface, >> not in >> > the definition. With GADTs, the type constraints are built into the >> > definition itself, which is precisely what makes them more powerful; no >> > need for an abstract interface on top. >> > >> > The first part of your question is about understanding how the >> > type-inference work (how variables are manipulated by the type-checker >> and >> > then "propagated back up"). This sounds like a difficult way to >> understand >> > GADTs: you want to learn the typing rules *and* the type-inference >> > algorithm at once. But only the first part is necessary to use the >> feature >> > productively (with a few tips on when to use annotations, which are >> easy to >> > explain and in fact explained in the manual: >> > http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html ). So >> instead of >> > asking: "how did the compiler get this type?", I would ask: "why is this >> > the right type"? I think you could convince yourself that (1) it is a >> > correct type and (2) any other valid type would be a specialization of >> this >> > type, there is no simpler solution. >> > >> > The second part: you wrote: >> > >> > let rec bind : type f r. f -> (f, r) t -> r = fun f -> function >> > | Z -> >> > f >> > | S (t, v) -> >> > bind (f (v ())) t >> > >> > Let's focus on the second clause: >> > >> > | S (t, v) -> >> > bind (f (v ())) t >> > >> > we know that (f : f) holds, and that the pattern-matching is on a value >> of >> > type (f, r) t, and we must return r. >> > When pattern-matching on S (t, v), we learn extra type information from >> the >> > typing rule of S: >> > >> > | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t >> > >> > if r has type (f, r) t, then (t, v) has type ((f, a -> r) t * (unit -> >> a)) >> > for *some* unknown/existential type a. So within the branch we have >> > >> > bind : type f r. f -> (f, r) t -> r >> > f : (f, a -> r) t >> > v : unit -> a >> > expected return type: r >> > >> > f does *not* have a function type here, so your idea of applying (f (v >> ())) >> > cannot work (v does have a function type, so (v ()) is valid). >> > >> > The only thing you can do on f is call (bind) recursively (with what >> > arguments?), and then you will get an (a -> r) as result. >> > >> > Do you see how to write a correct program from there? >> >> Ah-ha! I was close but my thinking was at the "wrong level" (I'm not >> sure how to put it). The working implementation of bind is: >> >> let rec bind : type f r. f -> (f, r) t -> r = fun f -> function >> | Z -> >> f >> | S (t, v) -> >> let f' = bind f t in >> f' (v ()) >> >> And now I see why you wanted me to look at it not through the module >> interface. Looking at how the recursion would work, of course the >> most-nested S will have the function corresponding to the first >> parameter of the function. I was thinking that I would consume the >> parameters on the way down, but it's actually on the way up. >> >> I am still working out in my head the answer to "why is this the right >> type", I think it has to slosh around in there a bit before it truly >> makes sense to me. >> >> Thank you! >> >> > >> > >> > >> > On Fri, Sep 20, 2019 at 5:42 AM Malcolm Matalka <mmatalka@gmail.com> >> wrote: >> > >> >> I have been using GADTs to make type-safe versions of APIs that are >> kind >> >> of like printf. I've been using this pattern by rote and now I'm >> >> getting to trying to understand how it works. >> >> >> >> I have the following code: >> >> >> >> module F : sig >> >> type ('f, 'r) t >> >> >> >> val z : ('r, 'r) t >> >> val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t >> >> end = struct >> >> type ('f, 'r) t = >> >> | Z : ('r, 'r) t >> >> | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t >> >> >> >> let z = Z >> >> let (//) t f = S (t, f) >> >> end >> >> >> >> And the following usage: >> >> >> >> utop # F.(z // (fun () -> Int32.zero) // (fun () -> ""));; >> >> - : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr> >> >> >> >> I understand how 'r is '_weak1 (I think), but I'm still trying to >> figure >> >> out how 'f gets its type by applying (//). I think I have an >> >> explanation below, and I'm hoping someone can say if it's correct >> and/or >> >> simplify it. >> >> >> >> Explanation: >> >> >> >> The constructor Z says that 'f and 'r, are the same (Z : ('r, 'r) t). >> >> The constructor S says that the (_, _) t that it takes has some type >> 'f, >> >> but that the second type variable must be of the form 'a -> 'r, sort of >> >> deconstructing pattern match on the type (if that makes sense). And if >> >> that (_, _) t is a Z, where we have stated the two type variables have >> >> the same value, that means 'f must also be ('a -> 'r). So for the >> >> first application of (//) it makes sense. If we apply (//) again, the >> >> first parameter has the type (int32 -> '_weak1, '_weak1) t, but that >> >> must actually mean '_weak1 in this case is string -> '_weak, and then >> >> this is where things become jumbled in my head. If the passed in (_, >> _) >> >> t must be (string -> '_weak), and the inner type actually must be >> (int32 >> >> -> '_weak), then, the inner inner type must be ('_weak), the type of 'r >> >> at Z must be (string -> int32 -> '_weak), and since 'r, and 'f are the >> >> same type for Z, 'f must also be (string -> int32 -> '_weak), and that >> >> knowledge propagates back up? But that doesn't feel quite right to me, >> >> either. >> >> >> >> With the help of reading other code, I've figured out how to make a >> >> function that uses a type like this that works like kprintf, however >> >> where I'm going in this case is that I want to take a function that >> >> matches 'f and apply it to the result of my functions. >> >> >> >> Something like: >> >> >> >> let rec bind : type f r. f -> (f, r) t -> r = fun f -> function >> >> | Z -> >> >> f >> >> | S (t, v) -> >> >> bind (f (v ())) t >> >> >> >> However, this does not compile given: >> >> >> >> Error: This expression has type f >> >> This is not a function; it cannot be applied. >> >> >> >> My understanding was if I have Z, and an input that has the type f, >> then >> >> that is just the return type since at Z, f and r are the same type. >> And >> >> than at S, I can peel away the type of f by applying the function f and >> >> then recursively calling. But my understanding is missing something. >> >> >> >> Does this make sense? >> >> >> >> What am I not understanding? >> >> >> >> Thank you, >> >> /Malcolm >> >> >> >> [-- Attachment #2: Type: text/html, Size: 13875 bytes --]

[-- Attachment #1: Type: text/plain, Size: 9450 bytes --] There is a direct relation between how type evolve during GADT typing and how queries evolve during logic/relational programming. It can help to think of a GADT declaration as the set of rules of a Prolog program. (I you have never looked at Prolog, here is an occasion to learn something new). That does *not* mean that GADTs let you do prolog-style programming in types (the compiler will not automatically search for a proof, the user has to write it down explicitly as a GADT term, so this work is not done implicitly, as with type-class search for example), but it does give a way to think about GADT declarations. Your declaration (notice that I renamed the Z variable, for a good reason that will appear clear below): type (_, _) t = | Z : ('f, 'f) t | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t becomes t F F. t F R :- t F (A -> R), (unit -> A). In any case, your declaration has the following effect: - by the Z rule, all types of the form ('a1 -> 'a2 -> ... -> 'an -> 'r, 'a -> 'a2 -> ... -> 'an -> 'r) t are inhabited - by the S rule, you can "hide" an element on the right (and you have to provide a thunk for it) , moving from ('a1 -> ... -> 'an -> r, 'ak -> 'a{k+1} -> .. -> 'an -> r) t to ('a1 -> ... -> 'an -> r, 'a{k+1} -> .. -> 'an -> r) t If you do this repeatedly you end up on what you want: ('a1 -> .. -> 'an -> r, r) t. The way you write about it, it sounds like you had the following *different* definition in mind type (_, _) t = | Z : ('r, 'r) t | S : ('f, 'r) t * (unit -> 'a) -> ('a -> 'f, 'r) t let test = S (S (Z, (fun () -> 3l)), (fun () -> "foo")) corresponding to the following Prolog program that I do find easier to think about: t R R. t (A -> F) R :- t F R, (unit -> A). It turns out that with this other definition, the first implementation that you had written actually type-check fines. (You could try to write conversion functions between those two definitions to convince yourself that they are morally equivalent, but this is actually a difficult exercise.) On Fri, Sep 20, 2019 at 10:11 AM Malcolm Matalka <mmatalka@gmail.com> wrote: > > Gabriel Scherer <gabriel.scherer@gmail.com> writes: > > > Note: the reason why you get _weak type variables (which are not > > polymorphic, just not-inferred-yet) is that the type-checker cannot > detect > > that (z // (fun () -> ...)) is a value: it would have to unfold the call > to > > (//) for this, which it doesn't do in general, and here certainly could > not > > do given that its definition is hidden behind an abstraction boundary. > > I would recommend experimenting *without* the module interface and the > > auxiliary function, with the constructors directly, you would get > slightly > > better types. > > > > # S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));; > > - : (int32 -> string -> 'a, 'a) t = S (S (Z, <fun>), <fun>) > > > > Historically we have used module interfaces to implement "phantom types" > -- > > because the type information there is only present in the interface, not > in > > the definition. With GADTs, the type constraints are built into the > > definition itself, which is precisely what makes them more powerful; no > > need for an abstract interface on top. > > > > The first part of your question is about understanding how the > > type-inference work (how variables are manipulated by the type-checker > and > > then "propagated back up"). This sounds like a difficult way to > understand > > GADTs: you want to learn the typing rules *and* the type-inference > > algorithm at once. But only the first part is necessary to use the > feature > > productively (with a few tips on when to use annotations, which are easy > to > > explain and in fact explained in the manual: > > http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html ). So instead > of > > asking: "how did the compiler get this type?", I would ask: "why is this > > the right type"? I think you could convince yourself that (1) it is a > > correct type and (2) any other valid type would be a specialization of > this > > type, there is no simpler solution. > > > > The second part: you wrote: > > > > let rec bind : type f r. f -> (f, r) t -> r = fun f -> function > > | Z -> > > f > > | S (t, v) -> > > bind (f (v ())) t > > > > Let's focus on the second clause: > > > > | S (t, v) -> > > bind (f (v ())) t > > > > we know that (f : f) holds, and that the pattern-matching is on a value > of > > type (f, r) t, and we must return r. > > When pattern-matching on S (t, v), we learn extra type information from > the > > typing rule of S: > > > > | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t > > > > if r has type (f, r) t, then (t, v) has type ((f, a -> r) t * (unit -> > a)) > > for *some* unknown/existential type a. So within the branch we have > > > > bind : type f r. f -> (f, r) t -> r > > f : (f, a -> r) t > > v : unit -> a > > expected return type: r > > > > f does *not* have a function type here, so your idea of applying (f (v > ())) > > cannot work (v does have a function type, so (v ()) is valid). > > > > The only thing you can do on f is call (bind) recursively (with what > > arguments?), and then you will get an (a -> r) as result. > > > > Do you see how to write a correct program from there? > > Ah-ha! I was close but my thinking was at the "wrong level" (I'm not > sure how to put it). The working implementation of bind is: > > let rec bind : type f r. f -> (f, r) t -> r = fun f -> function > | Z -> > f > | S (t, v) -> > let f' = bind f t in > f' (v ()) > > And now I see why you wanted me to look at it not through the module > interface. Looking at how the recursion would work, of course the > most-nested S will have the function corresponding to the first > parameter of the function. I was thinking that I would consume the > parameters on the way down, but it's actually on the way up. > > I am still working out in my head the answer to "why is this the right > type", I think it has to slosh around in there a bit before it truly > makes sense to me. > > Thank you! > > > > > > > > > On Fri, Sep 20, 2019 at 5:42 AM Malcolm Matalka <mmatalka@gmail.com> > wrote: > > > >> I have been using GADTs to make type-safe versions of APIs that are kind > >> of like printf. I've been using this pattern by rote and now I'm > >> getting to trying to understand how it works. > >> > >> I have the following code: > >> > >> module F : sig > >> type ('f, 'r) t > >> > >> val z : ('r, 'r) t > >> val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t > >> end = struct > >> type ('f, 'r) t = > >> | Z : ('r, 'r) t > >> | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t > >> > >> let z = Z > >> let (//) t f = S (t, f) > >> end > >> > >> And the following usage: > >> > >> utop # F.(z // (fun () -> Int32.zero) // (fun () -> ""));; > >> - : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr> > >> > >> I understand how 'r is '_weak1 (I think), but I'm still trying to figure > >> out how 'f gets its type by applying (//). I think I have an > >> explanation below, and I'm hoping someone can say if it's correct and/or > >> simplify it. > >> > >> Explanation: > >> > >> The constructor Z says that 'f and 'r, are the same (Z : ('r, 'r) t). > >> The constructor S says that the (_, _) t that it takes has some type 'f, > >> but that the second type variable must be of the form 'a -> 'r, sort of > >> deconstructing pattern match on the type (if that makes sense). And if > >> that (_, _) t is a Z, where we have stated the two type variables have > >> the same value, that means 'f must also be ('a -> 'r). So for the > >> first application of (//) it makes sense. If we apply (//) again, the > >> first parameter has the type (int32 -> '_weak1, '_weak1) t, but that > >> must actually mean '_weak1 in this case is string -> '_weak, and then > >> this is where things become jumbled in my head. If the passed in (_, _) > >> t must be (string -> '_weak), and the inner type actually must be (int32 > >> -> '_weak), then, the inner inner type must be ('_weak), the type of 'r > >> at Z must be (string -> int32 -> '_weak), and since 'r, and 'f are the > >> same type for Z, 'f must also be (string -> int32 -> '_weak), and that > >> knowledge propagates back up? But that doesn't feel quite right to me, > >> either. > >> > >> With the help of reading other code, I've figured out how to make a > >> function that uses a type like this that works like kprintf, however > >> where I'm going in this case is that I want to take a function that > >> matches 'f and apply it to the result of my functions. > >> > >> Something like: > >> > >> let rec bind : type f r. f -> (f, r) t -> r = fun f -> function > >> | Z -> > >> f > >> | S (t, v) -> > >> bind (f (v ())) t > >> > >> However, this does not compile given: > >> > >> Error: This expression has type f > >> This is not a function; it cannot be applied. > >> > >> My understanding was if I have Z, and an input that has the type f, then > >> that is just the return type since at Z, f and r are the same type. And > >> than at S, I can peel away the type of f by applying the function f and > >> then recursively calling. But my understanding is missing something. > >> > >> Does this make sense? > >> > >> What am I not understanding? > >> > >> Thank you, > >> /Malcolm > >> > > [-- Attachment #2: Type: text/html, Size: 12567 bytes --]

Gabriel Scherer <gabriel.scherer@gmail.com> writes: > Note: the reason why you get _weak type variables (which are not > polymorphic, just not-inferred-yet) is that the type-checker cannot detect > that (z // (fun () -> ...)) is a value: it would have to unfold the call to > (//) for this, which it doesn't do in general, and here certainly could not > do given that its definition is hidden behind an abstraction boundary. > I would recommend experimenting *without* the module interface and the > auxiliary function, with the constructors directly, you would get slightly > better types. > > # S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));; > - : (int32 -> string -> 'a, 'a) t = S (S (Z, <fun>), <fun>) > > Historically we have used module interfaces to implement "phantom types" -- > because the type information there is only present in the interface, not in > the definition. With GADTs, the type constraints are built into the > definition itself, which is precisely what makes them more powerful; no > need for an abstract interface on top. > > The first part of your question is about understanding how the > type-inference work (how variables are manipulated by the type-checker and > then "propagated back up"). This sounds like a difficult way to understand > GADTs: you want to learn the typing rules *and* the type-inference > algorithm at once. But only the first part is necessary to use the feature > productively (with a few tips on when to use annotations, which are easy to > explain and in fact explained in the manual: > http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html ). So instead of > asking: "how did the compiler get this type?", I would ask: "why is this > the right type"? I think you could convince yourself that (1) it is a > correct type and (2) any other valid type would be a specialization of this > type, there is no simpler solution. > > The second part: you wrote: > > let rec bind : type f r. f -> (f, r) t -> r = fun f -> function > | Z -> > f > | S (t, v) -> > bind (f (v ())) t > > Let's focus on the second clause: > > | S (t, v) -> > bind (f (v ())) t > > we know that (f : f) holds, and that the pattern-matching is on a value of > type (f, r) t, and we must return r. > When pattern-matching on S (t, v), we learn extra type information from the > typing rule of S: > > | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t > > if r has type (f, r) t, then (t, v) has type ((f, a -> r) t * (unit -> a)) > for *some* unknown/existential type a. So within the branch we have > > bind : type f r. f -> (f, r) t -> r > f : (f, a -> r) t > v : unit -> a > expected return type: r > > f does *not* have a function type here, so your idea of applying (f (v ())) > cannot work (v does have a function type, so (v ()) is valid). > > The only thing you can do on f is call (bind) recursively (with what > arguments?), and then you will get an (a -> r) as result. > > Do you see how to write a correct program from there? Ah-ha! I was close but my thinking was at the "wrong level" (I'm not sure how to put it). The working implementation of bind is: let rec bind : type f r. f -> (f, r) t -> r = fun f -> function | Z -> f | S (t, v) -> let f' = bind f t in f' (v ()) And now I see why you wanted me to look at it not through the module interface. Looking at how the recursion would work, of course the most-nested S will have the function corresponding to the first parameter of the function. I was thinking that I would consume the parameters on the way down, but it's actually on the way up. I am still working out in my head the answer to "why is this the right type", I think it has to slosh around in there a bit before it truly makes sense to me. Thank you! > > > > On Fri, Sep 20, 2019 at 5:42 AM Malcolm Matalka <mmatalka@gmail.com> wrote: > >> I have been using GADTs to make type-safe versions of APIs that are kind >> of like printf. I've been using this pattern by rote and now I'm >> getting to trying to understand how it works. >> >> I have the following code: >> >> module F : sig >> type ('f, 'r) t >> >> val z : ('r, 'r) t >> val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t >> end = struct >> type ('f, 'r) t = >> | Z : ('r, 'r) t >> | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t >> >> let z = Z >> let (//) t f = S (t, f) >> end >> >> And the following usage: >> >> utop # F.(z // (fun () -> Int32.zero) // (fun () -> ""));; >> - : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr> >> >> I understand how 'r is '_weak1 (I think), but I'm still trying to figure >> out how 'f gets its type by applying (//). I think I have an >> explanation below, and I'm hoping someone can say if it's correct and/or >> simplify it. >> >> Explanation: >> >> The constructor Z says that 'f and 'r, are the same (Z : ('r, 'r) t). >> The constructor S says that the (_, _) t that it takes has some type 'f, >> but that the second type variable must be of the form 'a -> 'r, sort of >> deconstructing pattern match on the type (if that makes sense). And if >> that (_, _) t is a Z, where we have stated the two type variables have >> the same value, that means 'f must also be ('a -> 'r). So for the >> first application of (//) it makes sense. If we apply (//) again, the >> first parameter has the type (int32 -> '_weak1, '_weak1) t, but that >> must actually mean '_weak1 in this case is string -> '_weak, and then >> this is where things become jumbled in my head. If the passed in (_, _) >> t must be (string -> '_weak), and the inner type actually must be (int32 >> -> '_weak), then, the inner inner type must be ('_weak), the type of 'r >> at Z must be (string -> int32 -> '_weak), and since 'r, and 'f are the >> same type for Z, 'f must also be (string -> int32 -> '_weak), and that >> knowledge propagates back up? But that doesn't feel quite right to me, >> either. >> >> With the help of reading other code, I've figured out how to make a >> function that uses a type like this that works like kprintf, however >> where I'm going in this case is that I want to take a function that >> matches 'f and apply it to the result of my functions. >> >> Something like: >> >> let rec bind : type f r. f -> (f, r) t -> r = fun f -> function >> | Z -> >> f >> | S (t, v) -> >> bind (f (v ())) t >> >> However, this does not compile given: >> >> Error: This expression has type f >> This is not a function; it cannot be applied. >> >> My understanding was if I have Z, and an input that has the type f, then >> that is just the return type since at Z, f and r are the same type. And >> than at S, I can peel away the type of f by applying the function f and >> then recursively calling. But my understanding is missing something. >> >> Does this make sense? >> >> What am I not understanding? >> >> Thank you, >> /Malcolm >>

[-- Attachment #1: Type: text/plain, Size: 5898 bytes --] Note: the reason why you get _weak type variables (which are not polymorphic, just not-inferred-yet) is that the type-checker cannot detect that (z // (fun () -> ...)) is a value: it would have to unfold the call to (//) for this, which it doesn't do in general, and here certainly could not do given that its definition is hidden behind an abstraction boundary. I would recommend experimenting *without* the module interface and the auxiliary function, with the constructors directly, you would get slightly better types. # S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));; - : (int32 -> string -> 'a, 'a) t = S (S (Z, <fun>), <fun>) Historically we have used module interfaces to implement "phantom types" -- because the type information there is only present in the interface, not in the definition. With GADTs, the type constraints are built into the definition itself, which is precisely what makes them more powerful; no need for an abstract interface on top. The first part of your question is about understanding how the type-inference work (how variables are manipulated by the type-checker and then "propagated back up"). This sounds like a difficult way to understand GADTs: you want to learn the typing rules *and* the type-inference algorithm at once. But only the first part is necessary to use the feature productively (with a few tips on when to use annotations, which are easy to explain and in fact explained in the manual: http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html ). So instead of asking: "how did the compiler get this type?", I would ask: "why is this the right type"? I think you could convince yourself that (1) it is a correct type and (2) any other valid type would be a specialization of this type, there is no simpler solution. The second part: you wrote: let rec bind : type f r. f -> (f, r) t -> r = fun f -> function | Z -> f | S (t, v) -> bind (f (v ())) t Let's focus on the second clause: | S (t, v) -> bind (f (v ())) t we know that (f : f) holds, and that the pattern-matching is on a value of type (f, r) t, and we must return r. When pattern-matching on S (t, v), we learn extra type information from the typing rule of S: | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t if r has type (f, r) t, then (t, v) has type ((f, a -> r) t * (unit -> a)) for *some* unknown/existential type a. So within the branch we have bind : type f r. f -> (f, r) t -> r f : (f, a -> r) t v : unit -> a expected return type: r f does *not* have a function type here, so your idea of applying (f (v ())) cannot work (v does have a function type, so (v ()) is valid). The only thing you can do on f is call (bind) recursively (with what arguments?), and then you will get an (a -> r) as result. Do you see how to write a correct program from there? On Fri, Sep 20, 2019 at 5:42 AM Malcolm Matalka <mmatalka@gmail.com> wrote: > I have been using GADTs to make type-safe versions of APIs that are kind > of like printf. I've been using this pattern by rote and now I'm > getting to trying to understand how it works. > > I have the following code: > > module F : sig > type ('f, 'r) t > > val z : ('r, 'r) t > val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t > end = struct > type ('f, 'r) t = > | Z : ('r, 'r) t > | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t > > let z = Z > let (//) t f = S (t, f) > end > > And the following usage: > > utop # F.(z // (fun () -> Int32.zero) // (fun () -> ""));; > - : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr> > > I understand how 'r is '_weak1 (I think), but I'm still trying to figure > out how 'f gets its type by applying (//). I think I have an > explanation below, and I'm hoping someone can say if it's correct and/or > simplify it. > > Explanation: > > The constructor Z says that 'f and 'r, are the same (Z : ('r, 'r) t). > The constructor S says that the (_, _) t that it takes has some type 'f, > but that the second type variable must be of the form 'a -> 'r, sort of > deconstructing pattern match on the type (if that makes sense). And if > that (_, _) t is a Z, where we have stated the two type variables have > the same value, that means 'f must also be ('a -> 'r). So for the > first application of (//) it makes sense. If we apply (//) again, the > first parameter has the type (int32 -> '_weak1, '_weak1) t, but that > must actually mean '_weak1 in this case is string -> '_weak, and then > this is where things become jumbled in my head. If the passed in (_, _) > t must be (string -> '_weak), and the inner type actually must be (int32 > -> '_weak), then, the inner inner type must be ('_weak), the type of 'r > at Z must be (string -> int32 -> '_weak), and since 'r, and 'f are the > same type for Z, 'f must also be (string -> int32 -> '_weak), and that > knowledge propagates back up? But that doesn't feel quite right to me, > either. > > With the help of reading other code, I've figured out how to make a > function that uses a type like this that works like kprintf, however > where I'm going in this case is that I want to take a function that > matches 'f and apply it to the result of my functions. > > Something like: > > let rec bind : type f r. f -> (f, r) t -> r = fun f -> function > | Z -> > f > | S (t, v) -> > bind (f (v ())) t > > However, this does not compile given: > > Error: This expression has type f > This is not a function; it cannot be applied. > > My understanding was if I have Z, and an input that has the type f, then > that is just the return type since at Z, f and r are the same type. And > than at S, I can peel away the type of f by applying the function f and > then recursively calling. But my understanding is missing something. > > Does this make sense? > > What am I not understanding? > > Thank you, > /Malcolm > [-- Attachment #2: Type: text/html, Size: 7529 bytes --]

I have been using GADTs to make type-safe versions of APIs that are kind of like printf. I've been using this pattern by rote and now I'm getting to trying to understand how it works. I have the following code: module F : sig type ('f, 'r) t val z : ('r, 'r) t val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t end = struct type ('f, 'r) t = | Z : ('r, 'r) t | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t let z = Z let (//) t f = S (t, f) end And the following usage: utop # F.(z // (fun () -> Int32.zero) // (fun () -> ""));; - : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr> I understand how 'r is '_weak1 (I think), but I'm still trying to figure out how 'f gets its type by applying (//). I think I have an explanation below, and I'm hoping someone can say if it's correct and/or simplify it. Explanation: The constructor Z says that 'f and 'r, are the same (Z : ('r, 'r) t). The constructor S says that the (_, _) t that it takes has some type 'f, but that the second type variable must be of the form 'a -> 'r, sort of deconstructing pattern match on the type (if that makes sense). And if that (_, _) t is a Z, where we have stated the two type variables have the same value, that means 'f must also be ('a -> 'r). So for the first application of (//) it makes sense. If we apply (//) again, the first parameter has the type (int32 -> '_weak1, '_weak1) t, but that must actually mean '_weak1 in this case is string -> '_weak, and then this is where things become jumbled in my head. If the passed in (_, _) t must be (string -> '_weak), and the inner type actually must be (int32 -> '_weak), then, the inner inner type must be ('_weak), the type of 'r at Z must be (string -> int32 -> '_weak), and since 'r, and 'f are the same type for Z, 'f must also be (string -> int32 -> '_weak), and that knowledge propagates back up? But that doesn't feel quite right to me, either. With the help of reading other code, I've figured out how to make a function that uses a type like this that works like kprintf, however where I'm going in this case is that I want to take a function that matches 'f and apply it to the result of my functions. Something like: let rec bind : type f r. f -> (f, r) t -> r = fun f -> function | Z -> f | S (t, v) -> bind (f (v ())) t However, this does not compile given: Error: This expression has type f This is not a function; it cannot be applied. My understanding was if I have Z, and an input that has the type f, then that is just the return type since at Z, f and r are the same type. And than at S, I can peel away the type of f by applying the function f and then recursively calling. But my understanding is missing something. Does this make sense? What am I not understanding? Thank you, /Malcolm

Bonjour à tous, (Bravo pour la 4.0.9!) OCamlPro lance un cycle de formations régulières à OCaml, en français, dans ses locaux parisiens (métro Alésia). La première session aura lieu début novembre 2019, avec 2 formations: (1) Formation débutant : passer à OCaml (5-6 novembre) (2) Formation expert : approfondir sa maîtrise du langage (7-8 novembre). La formation "expert" sera l'occasion pour des programmeurs OCaml ayant déjà une certaine expérience de mieux comprendre les possibilités avancées du typage (objets, GADT), de découvrir en détail le fonctionnement du GC et d'écrire du code optimisable par le compilateur. Ces formations sont aussi une occasion de venir chez OCamlPro discuter avec les lead développeurs et contributeurs d'OPAM et Flambda. Des formations en anglais peuvent aussi être organisées sur demande. N'hésitez pas à faire circuler. Liens : http://www.ocamlpro.com/fr/formation-passer-a-ocaml/ http://www.ocamlpro.com/fr/formation-expert-ocaml/ http://www.ocamlpro.com/fr/formations/ Inscription : http://www.ocamlpro.com/forms/preinscriptions-formation-ocaml/ Muriel NB : C'est aussi un bon complément à l'excellent MOOC OCaml de l'Université Paris-Diderot et à la plate-forme learn-OCaml financée par la Fondation OCaml :-) https://www.fun-mooc.fr/courses/course-v1:parisdiderot+56002+session04/about http://ocaml.foundation/learn-ocaml ********* Dear all, In our endeavour to encourage professional programmers to understand and use OCaml, OCamlPro will be giving 2 training sessions, in French, in our Paris offices: (1) OCaml Beginner course for professional programmers (5-6 Nov) (2) OCaml Expertise (7-8 Nov). The "Expert" OCaml course is for already experienced OCaml programmers to better understand advanced type system possibilities (objects, GADTs), discover GC internals, write "compiler-optimizable" code. These sessions are also an opportunity to come discuss with our OPAM & Flambda lead developers and core contributors in Paris. Training in English can also be organized, on-demand. Do not hesitate pass the word. Links: http://www.ocamlpro.com/training-ocamlpro/ http://www.ocamlpro.com/course-ocaml-development/ http://www.ocamlpro.com/course-ocaml-expert/ Register link: http://www.ocamlpro.com/forms/preinscriptions-formation-ocaml/ Cheers, Muriel PS: Note that this complements the excellent OCaml MOOC from Université Paris-Diderot and the learn-OCaml platform of the OCaml Software Foundation. -- Muriel OCamlPro's latest blog posts: http://www.ocamlpro.com/2019/09/13/updated-cheat-sheets-ocaml-language-and-ocaml-standard-library/ by Thomas http://www.ocamlpro.com/2019/08/30/ocamlpros-compiler-team-work-update/ by Vincent & Pierre http://www.ocamlpro.com/2019/07/11/opam-2-0-5-release/ by Raja & Louis More on OCamlPro: The French software company OCamlPro was created in 2011 to promote OCaml in the industry. Today we harness our OCaml expertise and formal methods know-how to design, prototype, and build high quality software in demanding projects for our clients. Our team of PhD-level engineers also contributes open source development tools for OCaml, helping to improve the efficiency and usability of the OCaml compiler and tools. We love to share our knowledge and teach vocational training courses. As a long-standing supporter of the OCaml language, we have always been committed to helping spread OCaml's adoption and increase the accessibility of OCaml to beginners and students.

Dear OCaml users, We have the pleasure of celebrating the birth of James Waddell Alexander II by announcing the release of OCaml version 4.09.0 . Some of the highlights of this new 4.09 release are: - New optimisations, in particular for affine functions in matches, for instance type t = A | B | C let affine = function | A -> 4 | B -> 3 | C -> 2 - The `graphics` library was moved out of the compiler distribution. - The `vmthread` library was removed. - Support for compiler plugins was removed. - Many bug fixes. The full list of change can be found in the changelog below. It is available as a set of OPAM switches, and as a source download here: https://caml.inria.fr/pub/distrib/ocaml-4.09/ Happy hacking, — Florian "octachron" Angeletti, for the OCaml team. OCaml 4.09.0 (18 Sep 2019) -------------------------------------- (Changes that can break existing programs are marked with a "*") ### Runtime system: * #1725, #2279: Deprecate Obj.set_tag and Obj.truncate (Stephen Dolan, review by Gabriel Scherer, Damien Doligez and Xavier Leroy) * #2240: Constify "identifier" in struct custom_operations (Cedric Cellier, review by Xavier Leroy) * #2293: Constify "caml_named_value" (Stephen Dolan, review by Xavier Leroy) - #8787, #8788: avoid integer overflow in caml_output_value_to_bytes (Jeremy Yallop, report by Marcello Seri) - #2075, #7729: rename _T macro used to support Unicode in the (Windows) runtime in order to avoid compiler warning (Nicolás Ojeda Bär, review by Gabriel Scherer and David Allsopp) - #2250: Remove extra integer sign-extension in compare functions (Stefan Muenzel, review by Xavier Leroy) - #8607: Remove obsolete macros for pre-2002 MSVC support (Stephen Dolan, review by Nicolás Ojeda Bär and David Allsopp) - #8656: Fix a bug in [caml_modify_generational_global_root] (Jacques-Henri Jourdan, review by Gabriel Scherer) ### Standard library: - #2262: take precision (.<n>) and flags ('+' and ' ') into account in printf %F (Pierre Roux, review by Gabriel Scherer) - #6148, #8596: optimize some buffer operations (Damien Doligez, reports by John Whitington and Alain Frisch, review by Jeremy Yallop and Gabriel Scherer) ### Other libraries: * #2318: Delete the graphics library. This library is now available as a separate "graphics" package in opam. Its new home is: https://github.com/ocaml/graphics (Jérémie Dimino, review by Nicolas Ojeda Bar, Xavier Leroy and Sébastien Hinderer) * #2289: Delete the vmthreads library. This library was deprecated in 4.08.0. (Jérémie Dimino) - #2112: Fix Thread.yield unfairness with busy threads yielding to each other. (Andrew Hunter, review by Jacques-Henri Jourdan, Spiros Eliopoulos, Stephen Weeks, & Mark Shinwell) - #7903, #2306: Make Thread.delay interruptible by signals again (Xavier Leroy, review by Jacques-Henri Jourdan and Edwin Török) - #2248: Unix alloc_sockaddr: Fix read of uninitialized memory for an unbound Unix socket. Add support for receiving abstract (Linux) socket paths. (Tim Cuthbertson, review by Sébastien Hinderer and Jérémie Dimino) ### Compiler user-interface and warnings: * #2276: Remove support for compiler plugins and hooks (also adds [Dynlink.unsafe_get_global_value]) (Mark Shinwell, Xavier Clerc, review by Nicolás Ojeda Bär, Florian Angeletti, David Allsopp and Xavier Leroy) - #2301: Hint on type error on int literal (Jules Aguillon, review by Nicolás Ojeda Bär , Florian Angeletti, Gabriel Scherer and Armaël Guéneau) * #2314: Remove support for gprof profiling. (Mark Shinwell, review by Xavier Clerc and Stephen Dolan) - #2190: fix pretty printing (using Pprintast) of "lazy ..." patterns and "fun (type t) -> ..." expressions. (Nicolás Ojeda Bär, review by Gabriel Scherer) - #2277: Use newtype names as type variable names The inferred type of (fun (type t) (x : t) -> x) is now printed as ('t -> 't) rather than ('a -> 'a). (Matthew Ryan) - #2309: New options -with-runtime and -without-runtime in ocamlopt/ocamlc that control the inclusion of the runtime system in the generated program. (Lucas Pluvinage, review by Daniel Bünzli, Damien Doligez, David Allsopp and Florian Angeletti) - #3819, #8546 more explanations and tests for illegal permutation (Florian Angeletti, review by Gabriel Scherer) - #8537: fix the -runtime-variant option for bytecode (Damien Doligez, review by David Allsopp) - #8541: Correctly print multi-lines locations (Louis Roché, review by Gabriel Scherer) - #8579: Better error message for private constructors of an extensible variant type (Guillaume Bury, review by many fine eyes) ### Code generation and optimizations: - #2278: Remove native code generation support for 32-bit Intel macOS, iOS and other Darwin targets. (Mark Shinwell, review by Nicolas Ojeda Bar and Xavier Leroy) - #8547: Optimize matches that are an affine function of the input. (Stefan Muenzel, review by Alain Frisch, Gabriel Scherer) - #1904, #7931: Add FreeBSD/aarch64 support (Greg V, review by Sébastien Hinderer, Stephen Dolan, Damien Doligez and Xavier Leroy) - #8507: Shorten symbol names of anonymous functions in Flambda mode (the directory portions are now hidden) (Mark Shinwell, review by Nicolás Ojeda Bär) - #8681, #8699, #8712: Fix code generation with nested let rec of functions. (Stephen Dolan, Leo White, Gabriel Scherer and Pierre Chambart, review by Gabriel Scherer, reports by Alexey Solovyev and Jonathan French) ### Manual and documentation: - #7584, #8538: Document .cmt* files in the "overview" of ocaml{c,opt} (Oxana Kostikova, rewiew by Florian Angeletti) - #8757: Rename Pervasives to Stdlib in core library documentation. (Ian Zimmerman, review by David Allsopp) - #8515: manual, precise constraints on reexported types (Florian Angeletti, review by Gabriel Scherer) ### Tools: - #2221: ocamldep will now correctly allow a .ml file in an include directory that appears first in the search order to shadow a .mli appearing in a later include directory. (Nicolás Ojeda Bär, review by Florian Angeletti) ### Internal/compiler-libs changes: - #1579: Add a separate types for clambda primitives (Pierre Chambart, review by Vincent Laviron and Mark Shinwell) - #1965: remove loop constructors in Cmm and Mach (Vincent Laviron) - #1973: fix compilation of catches with multiple handlers (Vincent Laviron) - #2228, #8545: refactoring the handling of .cmi files by moving the logic from Env to a new module Persistent_env (Gabriel Scherer, review by Jérémie Dimino and Thomas Refis) - #2229: Env: remove prefix_idents cache (Thomas Refis, review by Frédéric Bour and Gabriel Scherer) - #2237, #8582: Reorder linearisation of Trywith to avoid a call instruction (Vincent Laviron and Greta Yorsh, additional review by Mark Shinwell; fix in #8582 by Mark Shinwell, Xavier Leroy and Anil Madhavapeddy) - #2265: Add bytecomp/opcodes.mli (Mark Shinwell, review by Nicolas Ojeda Bar) - #2268: Improve packing mechanism used for building compilerlibs modules into the Dynlink libraries (Mark Shinwell, Stephen Dolan, review by David Allsopp) - #2280: Don't make more Clambda constants after starting Cmmgen (Mark Shinwell, review by Vincent Laviron) - #2281: Move some middle-end files around (Mark Shinwell, review by Pierre Chambart and Vincent Laviron) - #2283: Add [is_prefix] and [find_and_chop_longest_common_prefix] to [Misc.Stdlib.List] (Mark Shinwell, review by Alain Frisch and Stephen Dolan) - #2284: Add various utility functions to [Misc] and remove functions from [Misc.Stdlib.Option] that are now in [Stdlib.Option] (Mark Shinwell, review by Thomas Refis) - #2286: Functorise [Consistbl] (Mark Shinwell, review by Gabriel Radanne) - #2291: Add [Compute_ranges] pass (Mark Shinwell, review by Vincent Laviron) - #2292: Add [Proc.frame_required] and [Proc.prologue_required]. Move tail recursion label creation to [Linearize]. Correctly position [Lprologue] relative to [Iname_for_debugger] operations. (Mark Shinwell, review by Vincent Laviron) - #2308: More debugging information on [Cmm] terms (Mark Shinwell, review by Stephen Dolan) - #7878, #8542: Replaced TypedtreeIter with tast_iterator (Isaac "Izzy" Avram, review by Gabriel Scherer and Nicolás Ojeda Bär) - #8598: Replace "not is_nonexpansive" by "maybe_expansive". (Thomas Refis, review by David Allsopp, Florian Angeletti, Gabriel Radanne, Gabriel Scherer and Xavier Leroy) ### Compiler distribution build system: - #2267: merge generation of header programs, also fixing parallel build on Cygwin. (David Allsopp, review by Sébastien Hinderer) - #8514: Use boot/ocamlc.opt for building, if available. (Stephen Dolan, review by Gabriel Scherer) ### Bug fixes: - #8864, #8865: Fix native compilation of left shift by (word_size - 1) (Vincent Laviron, report by Murilo Giacometti Rocha, review by Xavier Leroy) - #2296: Fix parsing of hexadecimal floats with underscores in the exponent. (Hugo Heuzard and Xavier Leroy, review by Gabriel Scherer) - #8800: Fix soundness bug in extension constructor inclusion (Leo White, review by Jacques Garrigue) - #8848: Fix x86 stack probe CFI information in caml_c_call and caml_call_gc (Tom Kelly, review by Xavier Leroy) - #7156, #8594: make top level use custom printers if they are available (Andrew Litteken, report by Martin Jambon, review by Nicolás Ojeda Bär, Thomas Refis, Armaël Guéneau, Gabriel Scherer, David Allsopp) - #3249: ocamlmklib should reject .cmxa files (Xavier Leroy) - #7937, #2287: fix uncaught Unify exception when looking for type declaration (Florian Angeletti, review by Jacques Garrigue) - #8610, #8613: toplevel printing, consistent deduplicated name for types (Florian Angeletti, review by Thomas Refis and Gabriel Scherer, reported by Xavier Clerc) - #8635, #8636: Fix a bad side-effect of the -allow-approx option of ocamldep. It used to turn some errors into successes (Jérémie Dimino) - #8701, #8725: Variance of constrained parameters causes principality issues (Jacques Garrigue, report by Leo White, review by Gabriel Scherer) - #8777(partial): fix position information in some polymorphic variant error messages about missing tags (Florian Angeletti, review by Thomas Refis) - #8779, more cautious variance computation to avoid missing cmis (Florian Angeletti, report by Antonio Nuno Monteiro, review by Leo White) - #8810: Env.lookup_module: don't allow creating loops (Thomas Refis, report by Leo White, review by Jacques Garrigue) - #8862, #8871: subst: preserve scopes (Thomas Refis, report by Leo White, review by Jacques Garrigue) - #8921, #8924: Fix stack overflow with Flambda (Vincent Laviron, review by Pierre Chambart and Leo White, report by Aleksandr Kuzmenko) - #8944: Fix "open struct .. end" on clambda backend (Thomas Refis, review by Leo White, report by Damon Wang and Mark Shinwell)

OCaml submissions are extremely welcome at BOB! BOB Conference 2020 "What happens when we use what's best for a change?" http://bobkonf.de/2020/cfc.html Berlin, February 28 Call for Contributions Deadline: November 8, 2019 You are actively engaged in advanced software engineering methods, implement ambitious architectures and are open to cutting-edge innovation? Attend this conference, meet people that share your goals, and get to know the best software tools and technologies available today. We strive to offer a day full of new experiences and impressions that you can use to immediately improve your daily life as a software developer. If you share our vision and want to contribute, submit a proposal for a talk or tutorial! NOTE: The conference fee will be waived for presenters. Travel expenses will not be covered (for exceptions see "Speaker Grants"). Speaker Grants -------------- BOB has Speaker Grants available to support speakers from groups under-represented in technology. We specifically seek women speakers and speakers who are not be able to attend the conference for financial reasons. Shepherding ----------- The program committee offers shepherding to all speakers. Shepherding provides speakers assistance with preparing their sessions, as well as a review of the talk slides. Topics ------ We are looking for talks about best-of-breed software technology, e.g.: - functional programming - persistent data structures and database - event-based modelling and architectures - types - formal methods for correctness and robustness - abstractions for concurrency and parallelism - metaprogramming - probabilistic programming - math and programming - controlled side effects - beyond REST and SOAP - effective abstractions for data analytics - ... everything really that isn’t mainstream, but you think should be. Presenters should provide the audience with information that is practically useful for software developers. We're especially interested in experience reports. Other topics are also relevant, e.g.: - introductory talks on technical background - overviews of a given field - demos and how-tos Requirements ------------- We accept proposals for presentations of 45 minutes (40 minutes talk + 5 minutes questions), as well as 90 minute tutorials for beginners. The language of presentation should be either English or German. Your proposal should include (in your presentation language of choice): - An abstract of max. 1500 characters. - A short bio/cv - Contact information (including at least email address) - A list of 3-5 concrete ideas of how your work can be applied in a developer's daily life - additional material (websites, blogs, slides, videos of past presentations, …) Submit here: https://bobcfc.active-group.de/en/bob2020/cfp Organisation ------------ - Direct questions to contact at bobkonf dot de - Proposal deadline: November 8, 2019 - Notification: November 22, 2019 - Program: December 6, 2019 Program Committee ----------------- (more information here: https://bobkonf.de/2020/programmkomitee.html) - Matthias Fischmann, Wire - Matthias Neubauer, SICK AG - Nicole Rauch, Softwareentwicklung und Entwicklungscoaching - Michael Sperber, Active Group - Stefan Wehr, factis research Scientific Advisory Board - Annette Bieniusa, TU Kaiserslautern - Torsten Grust, Uni Tübingen - Peter Thiemann, Uni Freiburg

[-- Attachment #1: Type: text/plain, Size: 2868 bytes --] Apologies for cross-posting - Please forward to anybody who might be interested ** PhD Positions in Privacy-Preserving Distributed Artificial Intelligence ** Two funded PhD positions are available in the area of Privacy-preserving Distributed Machine Learning. The PhD candidate will work under the supervision of Prof. Ferdinando Fioretto at the EECS Department, Syracuse University. The position start date is flexible, with a start date as early as January 2020. The PhD candidate is committed to conduct independent and original research, to report on this research in international publications and conference presentations, and to describe the results of the research in a PhD dissertation. ** Topic Description ** The recent surge in optimization and machine learning research, in particular, deep learning, paved the way for a number of applications, many of which use privacy-sensitive user data. The resulting models have been shown to often reveal private user information, which may harm individual users. To contrast these risks, a new line of research aims at developing variants of optimization and ML algorithms that preserve the privacy of the individuals contained in the used datasets. Additionally, there is an increasing interest in leveraging distributed data shared across organizations to augment AI-powered services. Examples include transportation services, sharing location-based data to improve on-demand capabilities, and hospitals, sharing data to prevent epidemic outbreaks. The proliferation of these applications lead to a transition from proprietary data acquisition and processing to data ecosystems where different agents learn and make decisions using data owned by different organizations, boosting the need for privacy-preserving technologies. The project focuses broadly on protecting the privacy of individuals without losing the benefits of large scale data analysis. Topics of interest include: - Privacy-preserving technology, such as Differential Privacy and secure multi-party computation - Distributed Machine Learning - Privacy-preserving Multiagent Systems - Privacy-Preserving Adversarial Deep Learning Models The project will combine fundamental aspects of privacy, optimization and distributed computation to design algorithms that perform (distributed) machine learning and decision making while guaranteeing they do not violate privacy. The ideal candidate will have a strong background and interest in machine learning, privacy-preserving technologies, and/or multi-agent systems. Publications in leading international venues (such as AAAI, IJCAI, AAMAS, ICML, NeurIPS) will be an advantage. ** To Apply ** Applications should be submitted at ffiorett@syr.edu<mailto:ffiorett@syr.edu> and candidates should include their resume and transcript (if available). [-- Attachment #2: Type: text/html, Size: 3988 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3125 bytes --] 22nd International Symposium on Practical Aspects of Declarative Languages (PADL 2020) <https://popl20.sigplan.org/home/PADL-2020#22nd-international-symposium-on-practical-aspects-of-declarative-languages-padl-2020> <https://popl20.sigplan.org/home/PADL-2020#httpspopl20sigplanorghomepadl-2020> https://popl20.sigplan.org/home/PADL-2020,20-21 January 2020, New Orleans, Louisiana, United States <https://popl20.sigplan.org/home/PADL-2020#20-21-january-2020-new-orleans-louisiana-united-states>Co-located with ACM POPL 2020 ( <https://popl20.sigplan.org/home/PADL-2020#co-located-with-acm-popl-2020-httpspopl20sigplanorg> https://popl20.sigplan.org/) ------------------------------ *Declarative languages* is an umbrella term that include functional, logic, and constraint programming languages. These languages have been successfully applied to many different real-world situations, ranging from database management to active networks to software engineering to decision support systems. New developments in theory and implementation have opened up new application areas. At the same time, applications of declarative languages to challenging problems raise intriguing research questions, such as scalable design and implementation, language extensions for application deployment, and programming environments. PADL is a well-established forum for researchers and practitioners to present original work emphasizing novel applications and implementation techniques for all forms of declarative programming, including functional and logic programming, database and constraint programming, and theorem proving. Topics of interest include, but are not limited to: - Innovative applications of declarative languages - Declarative domain-specific languages and applications - Practical applications of theoretical results - New language developments and their impact on applications - Declarative languages for software engineering - Evaluation of implementation techniques on practical applications - Practical experiences and industrial applications - Novel uses of declarative languages in the classroom - Practical languages and extensions such as probabilistic and reactive languages *PADL 2020* especially welcomes new ideas and approaches pertaining to applications, design and implementation of declarative languages going beyond the scope of the past PADL symposia, for example, advanced database languages and contract languages, as well as verification and theorem proving methods that rely on declarative languages. Important Dates and Submission Guidelines: <https://popl20.sigplan.org/home/PADL-2020#important-dates-and-submission-guidelines> - Abstracts due: 11 October 2019 - Papers due: 18 October 2019 - Notification to authors: 18 November 2019 - Camera-ready: 29 November 2020 - Symposium dates: 20 - 21 January 2020 Submission instructions can be found at: https://popl20.sigplan.org/home/PADL-2020#Call-for-Papers Looking forward to receiving your submission, PADL19 PC members: https://popl20.sigplan.org/home/PADL-2020#About [-- Attachment #2: Type: text/html, Size: 8277 bytes --]

```
Quoting Thomas Blanc <thomas.blanc@ocamlpro.com> (snt: 2019-09-17 14:32 +0200 CEST) (rcv: 2019-09-17 14:34 +0200 CEST):
> Dear OCaml users,
>
>
> It is our pleasure to announce the release of our up-to-date cheat-sheets
> for the OCaml language and standard library.
[...]
Thank you!
Oliver
```

Dear OCaml users, It is our pleasure to announce the release of our up-to-date cheat-sheets for the OCaml language and standard library. Our original cheat-sheets were published in 2011, and as you know there has been quite a few changes in the language, library and ecosystem overall. See http://www.ocamlpro.com/2019/09/13/updated-cheat-sheets-ocaml-language-and-ocaml-standard-library/ for details. Links: * OCaml language (pdf, 1 page): http://www.ocamlpro.com/wp-content/uploads/2019/09/ocaml-lang.pdf * OCaml stdlib (pdf, 2 pages): http://www.ocamlpro.com/wp-content/uploads/2019/09/ocaml-stdlib.pdf * Sources: https://github.com/OCamlPro/ocaml-cheat-sheets Comments and contributions on Github are welcome. Special thanks to Hannes Mehnert for his lightning fast bug-reporting and Fourchaux for his keen spelling eye. As you can see, our Github repository contains not-yet-updated cheat-sheets. Stay tuned for coming updates! Obviously, our opam cheat-sheet is already in writing by the greatest opam experts you can find. We also wish to make sheets for Lwt, Core, Dune, ppx - any suggestions are welcome. Happy hacking! -- Thomas Blanc OCamlPRO SAS PS: if you're curious about what we've been doing lately, check out our blogpotst: http://www.ocamlpro.com/2019/08/30/ocamlpros-compiler-team-work-update/ http://www.ocamlpro.com/2019/07/11/opam-2-0-5-release/ http://www.ocamlpro.com/2019/07/09/alt-ergo-participation-to-the-smt-comp-2019/

FIRST Call For Papers FLOPS 2020: 15th International Symposium on Functional and Logic Programming =============================== 23-25 April, 2020, Akita, Japan https://www.ipl.riec.tohoku.ac.jp/FLOPS2020/ Writing down detailed computational steps is not the only way of programming. An alternative, being used increasingly in practice, is to start by writing down the desired properties of the result. The computational steps are then (semi-)automatically derived from these higher-level specifications. Examples of this declarative style of programming include functional and logic programming, program transformation and rewriting, and extracting programs from proofs of their correctness. FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming paradigm, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming. *** Scope *** FLOPS solicits original papers in all areas of the declarative programming: * functional, logic, functional-logic programming, rewriting systems, formal methods and model checking, program transformations and program refinements, developing programs with the help of theorem provers or SAT/SMT solvers, verifying properties of programs using declarative programming techniques; * foundations, language design, implementation issues (compilation techniques, memory management, run-time systems, etc.), applications and case studies. FLOPS promotes ross-fertilization among different styles of declarative programming. Therefore, research papers must be written to be understandable by the wide audience of declarative programmers and researchers. In particular, each submission should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, explaining why it is significant for its area, and comparing it with previous work. Submission of system descriptions and declarative pearls are especially encouraged. *** Submission *** Submissions should fall into one of the following categories: * Regular research papers: they should describe new results and will be judged on originality, correctness, and significance. * System descriptions: they should describe a working system and will be judged on originality, usefulness, and design. * Declarative pearls: new and excellent declarative programs or theories with illustrative applications. System descriptions and declarative pearls must be explicitly marked as such in the title. Submissions must be unpublished and not submitted for publication elsewhere. Work that already appeared in unpublished or informally published workshops proceedings may be submitted. See also ACM SIGPLAN Republication Policy, as explained on the web at http://www.sigplan.org/Resources/Policies/Republication. Submissions must be written in English and can be up to 15 pages excluding references, though system descriptions and pearls are typically shorter. The formatting has to conform to Springer's guidelines. Regular research papers should be supported by proofs and/or experimental results. In case of lack of space, this supporting information should be made accessible otherwise (e.g., a link to an anonymized Web page or an appendix, which does not count towards the page limit). However, it is the responsibility of the authors to guarantee that their paper can be understood and appreciated without referring to this supporting information; reviewers may simply choose not to look at it when writing their review. FLOPS 2020 will employ a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules: 1. author names and institutions must be omitted, and 2. references to authors' own related work should be in the third person (e.g., not "We build on our previous work …" but rather "We build on the work of …"). The purpose of this process is to help the reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult (e.g., important background references should not be omitted or anonymized). In addition, authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas. Papers should be submitted electronically at EasyChair which will be available soon from the Web Site of FLOPS 2020. *** Proceedings *** The proceedings will be published by Springer International Publishing in the Lecture Notes in Computer Science (LNCS) series. *** Important Dates *** 15 November 2019 (AoE): Abstract submission 22 November 2019 (AoE): Submission deadline 24 January 2020: Author notification 16 February 2020: Camera ready due 23-25 April 2020: FLOPS Symposium *** Organizers *** Keisuke Nakano Tohoku University, Japan (PC Co-Chair, General Chair) Kostis Sagonas Uppsala University, Sweden (PC Co-Chair) Kazuyuki Asada Tohoku University, Japan (Local Co-Chair) Ryoma Sin'ya Akita University, Japan (Local Co-Chair) Katsuhiro Ueno Tohoku University, Japan (Local Co-Chair) *** Contact Address *** flops2020 _AT_ easychair.org -------------------------------------------------------------------------------

[Please accept our apologies if you receive multiple copies of this message.] Call for Papers of EPEW 2019 ------------------------------------------------------------------------ The 16th European Performance Engineering Workshop will be held in Milano, Italy, on November 28 - 29, 2019. https://www.epew19.deib.polimi.it/ (Home page) Conference Highlights ------------------------------------------------------------------------ General Chairs - Marco Gribaudo, Politecnico di Milano, Italy - Mauro Iacono, Università degli Studi della Campania "Luigi Vanvitelli", Italy Program Chairs - Rostislav Razumchik, Federal Research Center “Computer Science and Control” of Russian Academy of Sciences, Russia - Tuan Phung-Duc, University of Tsukuba, Japan Keynote Speakers - Prof. Anne Remke, University of Munster, Germany - Prof. emeritus Giuseppe Serazzi, Politecnico di Milano, Italy Scope and Topics ------------------------------------------------------------------------ The European Performance Engineering Workshop is an annual event that aims to gather academic and industrial researchers working on all aspects of performance engineering. We invite original papers related to the following areas: - Theoretical advances in performance modeling and evaluation, e.g.: • Probabilistic, stochastic, or performability models, such as Queueing Networks, Petri Nets, and Process Calculi • Specification of quantitative properties • Analytical and numerical solution techniques and simulation techniques • Quantitative model checking, equivalence checking, and static analysis • Context-aware modelling and analysis techniques - System, software, and network performance engineering, e.g.: • Performance-oriented design, architecture, implementation, deployment, monitoring, and maintenance • Constraint-based and model-driven system design • Performance analysis, simulation, and experimental design • Benchmark design and benchmark-based evaluation and monitoring • Automated interpretation of analysis results • Quality of service, and trade-offs between security, performance, dependability, energy consumption, usability, etc. • Software performance modeling languages, model composition and tool interoperability • 5G and beyond - Case studies, e.g.: • Cloud systems, Hybrid Cloud, and Fog Computing • Internet of Things • Cyber-physical systems • E-health systems • Blockchain and Cryptocurrency applications • Sharing services such as carshare and rideshare Important Dates ------------------------------------------------------------------------ Paper submission: extended to September 23, 2019 (abstract), September 26, 2019 (full paper) Author notification: October 14, 2019 Camera ready: November 4, 2019 Conference: November 27-28, 2019 Submissions ------------------------------------------------------------------------ All accepted papers must be presented at the conference by one of the authors. Submissions must be original and should not have been published previously or be under consideration for publication. All submitted papers will be evaluated by at least three reviewers on the basis of their originality, technical quality, scientific or practical contribution to the state of the art, methodology, clarity, and adequacy of references. Accepted papers will be published in the conference proceedings, in the Lecture Notes in Computer Science series, by Springer-Verlag. Authors will be required to sign a copyright release. Submissions must be prepared in LaTeX, following Springer's LNCS guidelines. Submitted papers must not exceed 15 pages in camera-ready form, including figures and references. Papers should be submitted electronically using the EasyChair online submission system at the following link: https://easychair.org/conferences/?conf=epew2019 Special Issue: ------------------------------------------------------------------------ Best papers will be invited to submit their extended work to the Special Issue “Queue and Stochastic Models for Operations Research” of the Mathematics journal. Contacts: ---------------------------------------------------------------------- Marco Gribaudo: marco[dot]gribaudo[at]polimi[dot]it Mauro Iacono: mauro[dot]iacono[at]unicampania[dot]it Tuan Phung-Duc: tuan[at]sk[dot]tsukuba[dot]ac[dot]jp Rostislav Razumchik: rrazumchik[at]ipiran[dot]ru

** Please accept our apologies for cross-posting ** ** It would be highly appreciated if you could disseminate this CFP among your colleagues ** ---------------------------------------------------------------------------- Some DEADLINES of the 24th European Conference on Artificial Intelligence (ECAI 2020) are APPROACHING. Please find below the overall Call for Papers, but particularly consider these deadlines: + WORKSHOP Proposal submission will close by October 30, 2019 + ECAI2020 Abstract submission will close by November 15, 2019 + PAIS Abstract submission will close by November 21, 2019 ECAI 2020 will take place in Santiago de Compostela from June 8 to 12, 2020. For additional information visit www.ecai2020.eu. CALL FOR PAPERS =============== The biennial European Conference on Artificial Intelligence (ECAI) is Europe's premier venue for presenting scientific results in AI. Under the general theme "Paving the way towards Human-Centric AI", the 24th edition of ECAI will be held in Santiago de Compostela, a UNESCO's World Heritage City which is the destination of unique Routes that cross all Europe since the Middle Ages. The conference dates are 10-12 June 2020, with the workshops taking place on 8-9 June. Save these dates! The Program Committee of the 24th European Conference on Artificial Intelligence (ECAI 2020) invites the submission of papers for the technical programme of the Conference. High-quality original submissions are welcome from research results and applications of all areas of AI. The following list of topics is indicative; other topics are welcome. - Agent-based and Multi-agent Systems (MAS) - Computational Intelligence (CI) - Constraints and Satisfiability (CS) - Games and Virtual Environments (GAME) - Heuristic Search (HEU) - Human Aspects in AI (HAI) - Information Retrieval and Filtering (IRF) - Knowledge Representation and Reasoning (KRR) - Machine Learning (ML) - Multidisciplinary Topics and Applications (MULT) - Natural Language Processing (NLP) - Planning and Scheduling (PLAN) - Robotics (ROB) - Safe, Explainable, and Trustworthy AI (XAI) - Semantic Technologies (SEM) - Uncertainty in AI (UAI) - Vision (VIS) The Call for Papers is available at http://ecai2020.eu/call-for-papers/mainconference/ WORKSHOPS, TUTORIALS AND OTHER EVENTS ------------------------------------- In addition to its full programme of technical papers, ECAI2020 will feature many AI-related events for researchers, students and all attendants who are interested on contemporary AI. Separate calls have been issued for: - Workshop proposals, CFP available at http://ecai2020.eu/call-for-papers/workshops/ - Tutorial proposals, CFP available at http://ecai2020.eu/call-for-papers/tutorials/ - PAIS 2020, the Prestigious Applications of Intelligent Systems conference, CFP available at http://ecai2020.eu/call-for-papers/pais/ - STAIRS 2020, the Starting AI Researcher Symposium, CFP available at http://ecai2020.eu/call-for-papers/stairs/ In addition, other AI-related events will be announced, specially addressing the role of AI in Europe (and vice-versa) with special focus on the Conference general theme. Among these, The Frontiers in AI track sessions, the Lab To Market event, the Women in AI Breakfast and the EU Challenges forum. Futhermore, ECAI2020 will have a special focus on Starting Researchers, who will be able to participate in an specific program including the Doctoral Consortium, the Three Minutes Thesis Competition, the Lunch with an EurAI Fellow and the Job Fair. SOME IMPORTANT DATES -------------------- ECAI2020 Abstract submission: November 15, 2019 ECAI2020 Paper submission: November 19, 2019 ECAI2020 Notification of acceptance/rejection: January 15, 2020 WORKSHOP Proposal submission: October 30, 2019 WORKSHOP Proposal notification: November 28, 2019 TUTORIAL Proposal Submission: February 20, 2020 TUTORIAL Acceptance Notification: March 20, 2020 PAIS Abstract submission: November 21, 2019 PAIS Paper submission: November 26, 2019 PAIS Notification of acceptance/rejection: January 20, 2020 ORGANIZATION ------------ The Conference is hosted by the European Association for Artificial Intelligence (EurAI) and the Spanish AI Society (AEPIA). ECAI 2020 is organized by the Intelligent Systems Group (GSI) and the Research Centre in Intelligent Technologies (CiTIUS), University of Santiago de Compostela. SYNERGIES WITH OTHER CONFERENCES -------------------------------- ECAI 2020 is coordinating with AAMAS 2020 and ICAPS 2020 to exploit synergies. Details will be announced very soon at the Website. CONTACT AND UPDATES ------------------- Updates will be regularly published at the Conference Website: www.ecai2020.eu Follow us in Twitter @ECAI2020 -- Luis Magdalena ECAI2020 Publicity Chair www.ecai2020.eu

Dear OCaml users, The release of OCaml 4.09.0 is approaching. We have created a second beta version to help you adapt your softwares to the new features ahead of the release. This new beta integrates in particular the fixes from 4.08.1 that were not yet part of the first beta due to the overlap between the release of 4.08.1 and the first beta. If you tried to test the first beta, and were stopped by the lack of working dune and ocamlfind, those issues has been fixed. The source code is available at these addresses: https://github.com/ocaml/ocaml/archive/4.09.0+beta2.tar.gz https://caml.inria.fr/pub/distrib/ocaml-4.09/ocaml-4.09.0+beta2.tar.gz The compiler can also be installed as an OPAM switch with one of the following commands. opam switch create ocaml-variants.4.09.0+beta2 --repositories=default,beta=git+https://github.com/ocaml/ocaml-beta-repository.git or opam switch create ocaml-variants.4.09.0+beta2+<VARIANT> --repositories=default,beta=git+https://github.com/ocaml/ocaml-beta-repository.git where you replace <VARIANT> with one of these: afl default-unsafe-string flambda fp fp+flambda We want to know about all bugs. Please report them here: https://github.com/ocaml/ocaml/issues Happy hacking — Florian "octachron" Angeletti, for the OCaml team OCaml 4.09.0 ------------------ (Changes that can break existing programs are marked with a "*") ### Code generation and optimizations: - #2278: Remove native code generation support for 32-bit Intel macOS, iOS and other Darwin targets. (Mark Shinwell, review by Nicolas Ojeda Bar and Xavier Leroy) - #8507: Shorten symbol names of anonymous functions in Flambda mode (the directory portions are now hidden) (Mark Shinwell, review by Nicolás Ojeda Bär) - #7931, #1904: Add FreeBSD/aarch64 support (Greg V, review by Sébastien Hinderer, Stephen Dolan, Damien Doligez and Xavier Leroy) - #8547: Optimize matches that are an affine function of the input. (Stefan Muenzel, review by Alain Frisch, Gabriel Scherer) - #8681, #8699, #8712: Fix code generation with nested let rec of functions. (Stephen Dolan, Leo White, Gabriel Scherer and Pierre Chambart, review by Gabriel Scherer, reports by Alexey Solovyev and Jonathan French) ### Compiler user-interface and warnings: * #2276: Remove support for compiler plugins and hooks (also adds [Dynlink.unsafe_get_global_value]) (Mark Shinwell, Xavier Clerc, review by Nicolás Ojeda Bär, Florian Angeletti, David Allsopp and Xavier Leroy) - #2301: Hint on type error on int literal (Jules Aguillon, review by Nicolás Ojeda Bär , Florian Angeletti, Gabriel Scherer and Armaël Guéneau) - #2309: New options -with-runtime and -without-runtime in ocamlopt/ocamlc that control the inclusion of the runtime system in the generated program. (Lucas Pluvinage, review by Daniel Bünzli, Damien Doligez, David Allsopp and Florian Angeletti) - #2314: Remove support for gprof profiling. (Mark Shinwell, review by Xavier Clerc and Stephen Dolan) - #3819, #8546 more explanations and tests for illegal permutation (Florian Angeletti, review by Gabriel Scherer) - #8537: fix the -runtime-variant option for bytecode (Damien Doligez, review by David Allsopp) - #8541: Correctly print multi-lines locations (Louis Roché, review by Gabriel Scherer) - #8579: Better error message for private constructors of an extensible variant type (Guillaume Bury, review by many fine eyes) ### Compiler distribution build system: - #2267: merge generation of header programs, also fixing parallel build on Cygwin. (David Allsopp, review by Sébastien Hinderer) - #8514: Use boot/ocamlc.opt for building, if available. (Stephen Dolan, review by Gabriel Scherer) ### Internal/compiler-libs changes: - #1579: Add a separate types for clambda primitives (Pierre Chambart, review by Vincent Laviron and Mark Shinwell) - #1965: remove loop constructors in Cmm and Mach (Vincent Laviron) - #1973: fix compilation of catches with multiple handlers (Vincent Laviron) - #2190: fix pretty printing (using Pprintast) of "lazy ..." patterns and "fun (type t) -> ..." expressions. (Nicolás Ojeda Bär, review by Gabriel Scherer) - #2228, #8545: refactoring the handling of .cmi files by moving the logic from Env to a new module Persistent_env (Gabriel Scherer, review by Jérémie Dimino and Thomas Refis) - #2229: Env: remove prefix_idents cache (Thomas Refis, review by Frédéric Bour and Gabriel Scherer) - #2237, #8582: Reorder linearisation of Trywith to avoid a call instruction (Vincent Laviron and Greta Yorsh, additional review by Mark Shinwell; fix in #8582 by Mark Shinwell, Xavier Leroy and Anil Madhavapeddy) - #2265: Add bytecomp/opcodes.mli (Mark Shinwell, review by Nicolas Ojeda Bar) - #2268: Improve packing mechanism used for building compilerlibs modules into the Dynlink libraries (Mark Shinwell, Stephen Dolan, review by David Allsopp) - #2277: Use newtype names as type variable names (Matthew Ryan) - #2280: Don't make more Clambda constants after starting Cmmgen (Mark Shinwell, review by Vincent Laviron) - #2281: Move some middle-end files around (Mark Shinwell) - #2283: Add [is_prefix] and [find_and_chop_longest_common_prefix] to [Misc.Stdlib.List] (Mark Shinwell, review by Alain Frisch and Stephen Dolan) - #2284: Add various utility functions to [Misc] and remove functions from [Misc.Stdlib.Option] that are now in [Stdlib.Option] (Mark Shinwell, review by Thomas Refis) - #2286: Functorise [Consistbl] (Mark Shinwell, review by Gabriel Radanne) - #2291: Add [Compute_ranges] pass (Mark Shinwell, review by Vincent Laviron) - #2292: Add [Proc.frame_required] and [Proc.prologue_required]. Move tail recursion label creation to [Linearize]. Correctly position [Lprologue] relative to [Iname_for_debugger] operations. (Mark Shinwell, review by Vincent Laviron) - #2308: More debugging information on [Cmm] terms (Mark Shinwell, review by Stephen Dolan) - #7878, #8542: Replaced TypedtreeIter with tast_iterator (Isaac "Izzy" Avram, review by Gabriel Scherer and Nicolás Ojeda Bär) - #8598: Replace "not is_nonexpansive" by "maybe_expansive". (Thomas Refis, review by David Allsopp, Florian Angeletti, Gabriel Radanne, Gabriel Scherer and Xavier Leroy) ### Runtime system: - #1725, #2279: Deprecate Obj.set_tag and Obj.truncate (Stephen Dolan, review by Gabriel Scherer, Damien Doligez and Xavier Leroy) - #2075, #7729: rename _T macro used to support Unicode in the (Windows) runtime in order to avoid compiler warning (Nicolás Ojeda Bär, review by Gabriel Scherer and David Allsopp) * #2240: Constify "identifier" in struct custom_operations (Cedric Cellier, review by Xavier Leroy) - #2250: Remove extra integer sign-extension in compare functions (Stefan Muenzel, review by Xavier Leroy) * #2293: Constify "caml_named_value" (Stephen Dolan, review by Xavier Leroy) - #8607: Remove obsolete macros for pre-2002 MSVC support (Stephen Dolan, review by Nicolás Ojeda Bär and David Allsopp) - #8656: Fix a bug in [caml_modify_generational_global_root] (Jacques-Henri Jourdan, review by Gabriel Scherer) - #8787, #8788: avoid integer overflow in caml_output_value_to_bytes (Jeremy Yallop, report by Marcello Seri) ### Standard library: - #2262: take precision (.<n>) and flags ('+' and ' ') into account in printf %F (Pierre Roux, review by Gabriel Scherer) - #6148, #8596: optimize some buffer operations (Damien Doligez, reports by John Whitington and Alain Frisch, review by Jeremy Yallop and Gabriel Scherer) ### Other libraries: - #2112: Fix Thread.yield unfairness with busy threads yielding to each other. (Andrew Hunter, review by Jacques-Henri Jourdan, Spiros Eliopoulos, Stephen Weeks, & Mark Shinwell) - #7903, #2306: Make Thread.delay interruptible by signals again (Xavier Leroy, review by Jacques-Henri Jourdan and Edwin Török) - #2248: Unix alloc_sockaddr: Fix read of uninitialized memory for an unbound Unix socket. Add support for receiving abstract (Linux) socket paths. (Tim Cuthbertson, review by Sébastien Hinderer and Jérémie Dimino) - #2289: Delete the vmthreads library. This library was deprecated in 4.08.0. (Jérémie Dimino) - #2318: Delete the graphics library. This library is now available as a separate "graphics" package in opam. Its new home is: https://github.com/ocaml/graphics (Jérémie Dimino, review by Nicolas Ojeda Bar, Xavier Leroy and Sébastien Hinderer) ### Tools: - #2221: ocamldep will now correctly allow a .ml file in an include directory that appears first in the search order to shadow a .mli appearing in a later include directory. (Nicolás Ojeda Bär, review by Florian Angeletti) ### Manual and documentation: - #8757: Rename Pervasives to Stdlib in core library documentation. (Ian Zimmerman, review by David Allsopp) - #7584, #8538: Document .cmt* files in the "overview" of ocaml{c,opt} (Oxana Kostikova, rewiew by Florian Angeletti) - #8515: manual, precise constraints on reexported types (Florian Angeletti, review by Gabriel Scherer) ### Bug fixes: - #7156, #8594: make top level use custom printers if they are available (Andrew Litteken, report by Martin Jambon, review by Nicolás Ojeda Bär, Thomas Refis, Armaël Guéneau, Gabriel Scherer, David Allsopp) - #3249: ocamlmklib should reject .cmxa files (Xavier Leroy) - #7937, #2287: fix uncaught Unify exception when looking for type declaration (Florian Angeletti, review by Jacques Garrigue) - #2296: Fix parsing of hexadecimal floats with underscores in the exponent. (Hugo Heuzard and Xavier Leroy, review by Gabriel Scherer) - #8610, #8613: toplevel printing, consistent deduplicated name for types (Florian Angeletti, review by Thomas Refis and Gabriel Scherer, reported by Xavier Clerc) - #8635, #8636: Fix a bad side-effect of the -allow-approx option of ocamldep. It used to turn some errors into successes (Jérémie Dimino) - #8701, #8725: Variance of constrained parameters causes principality issues (Jacques Garrigue, report by Leo White, review by Gabriel Scherer) - #8777(partial): fix position information in some polymorphic variant error messages about missing tags (Florian Angeletti, review by Thomas Refis) - #8779, more cautious variance computation to avoid missing cmis (Florian Angeletti, report by Antonio Nuno Monteiro, review by Leo White) - #8800: Fix soundness bug in extension constructor inclusion (Leo White, review by Jacques Garrigue) - #8810: Env.lookup_module: don't allow creating loops (Thomas Refis, report by Leo White, review by Jacques Garrigue) - #8848: Fix x86 stack probe CFI information in caml_c_call and caml_call_gc (Tom Kelly, review by Xavier Leroy) - #8864, #8865: Fix native compilation of left shift by (word_size - 1) (Vincent Laviron, report by Murilo Giacometti Rocha, review by Xavier Leroy) - #8862, #8871: subst: preserve scopes (Thomas Refis, report by Leo White, review by Jacques Garrigue) - #8921, #8924: Fix stack overflow with Flambda (Vincent Laviron, review by Pierre Chambart and Leo White, report by Aleksandr Kuzmenko)

[-- Attachment #1: Type: text/plain, Size: 3799 bytes --] [ This message is intentionally written in French. ] * Merci de faire circuler : premier appel à communications * JFLA'2020 ( http://jfla.inria.fr/jfla2020.html) Journées Francophones des Langages Applicatifs Gruissan - du 29 janvier au 1 février 2020 Dates importantes --------------------- 1 octobre 2019 : soumission des résumés 8 octobre 2019 : soumission des articles 2 novembre 2019 : notification aux auteurs Les trente et unièmes Journées Francophones des Langages Applicatifs (JFLA) se tiendront à Gruissan, et plus précisément à l'hôtel Hôtel Phoebus Garden & spa du mercredi 29 janvier au samedi 1 février 2020. Les JFLA réunissent concepteurs, utilisateurs et théoriciens ; elles ont pour ambition de couvrir les domaines des langages applicatifs, de la preuve formelle, de la vérification de programmes, et des objets mathématiques qui sous-tendent ces outils. Ces domaines doivent être pris au sens large : nous souhaitons promouvoir les ponts entre les différentes thématiques. . Langages fonctionnels et applicatifs : sémantique, compilation, optimisation, typage, mesures, extensions par d'autres paradigmes. . Assistants de preuve : implémentation, nouvelles tactiques, développements présentant un intérêt technique ou méthodologique. . Logique, correspondance de Curry-Howard, réalisabilité, extraction de programmes, modèles. . Spécification, prototypage, développements formels d'algorithmes. . Vérification de programmes ou de modèles, méthode déductive, interprétation abstraite, raffinement. . Utilisation industrielle des langages fonctionnels et applicatifs, ou des méthodes issues des preuves formelles, outils pour le web. Les articles soumis aux JFLA sont relus par au moins deux personnes s'ils sont acceptés, trois personnes s'ils sont rejetés. Les critiques des relecteurs sont toujours bienveillantes et la plupart du temps encourageantes et constructives, même en cas de rejet. Il n'y a donc pas de raison de ne pas soumettre aux JFLA ! Soumissions ----------- Nous acceptons deux types de soumissions : . Article de recherche de seize pages au plus (bibliographie incluse), portant sur des travaux originaux. Nous acceptons des travaux en cours, pour lesquels l'aspect recherche n'est pas entièrement finalisé. . Article court de huit pages au plus (bibliographie incluse), pour décrire un prototype, faire la démonstration d'un outil, rechercher de l'aide pour résoudre un problème particulier, ou reparler d'un papier déjà publié. Dans tous les cas, la forme de l'article devra être soignée. Les articles sélectionnés seront publiés dans les actes de la conférence, et les auteurs seront invités à faire une présentation lors des journées, de vingt-cinq minutes pour les articles longs et de quinze minutes pour les courts. L'article peut être rédigé en anglais, auquel cas la présentation devra être effectuée en français. Néanmoins, dans le cas où il s'agit d'une republication au format court d'un article déjà publié, la publication doit être en français et la publication originale en anglais. Le style LaTeX Easychair doit être respecté : https://easychair.org/publications/for_authors Les soumissions se font sur la page Easychair des JFLA : https://easychair.org/conferences/?conf=jfla20 Notez que toute intention de soumission doit être annoncée au plus tard le 1er octobre 2019 par le dépôt d'un résumé sur Easychair. date limite de soumission des résumés : 1er octobre 2019 date limite de soumission des articles : 8 octobre 2019 [-- Attachment #2: Type: text/html, Size: 4321 bytes --]

[-- Attachment #1: Type: text/plain, Size: 9327 bytes --] On Tue, Sep 10, 2019 at 10:38 AM Oleg <oleg@okmij.org> wrote: > > > https://github.com/BinaryAnalysisPlatform/bap - the BAP project per se. > > ... > That is quite a project! And interesting, too. Thank you for letting > me know. Now I understand what you mean by ``universe of types > actually grew quite large, that large that the linear search in the > registry is not an option for us anymore.'' > > What your message has made it very clear, to me, is that we really > need the standard type representation library -- hopefully being part > of Stdlib and eventually integrated with the compiler. For one, it is > high time we standardized the spelling of the ('a,'b) eq type and its > constructor. Mainly, as your message has well demonstrated, an > efficient trep is actually non-trivial, and takes lots of experience > to design. Incidentally, the situation on Haskell is very similar: > Typeable is now well integrated with the compiler. It is quite a > popular library. > Definitely! So far the closest to what could be called a standard representation is the Base.Type_equal [1] module (and its extensions [2]). But unfortunately, it comes with strings attached and that hampers its adoption in other projects. Basically, we need at least to put the data constructor in a separate library (as it was done for the `result` type previously). Going beyond just defining the data type would require some consensus. A good example would be deciding how to implement the total order relation on type indices. The Base Library is using `Obj.extension_constructor` which has a few problems: 1) It is in the Obj module with all the ramifications 2) The implementation is inefficient and overly cautious (so cautious that it doesn't work with the Ancient module, for example) 3) The corresponding index is too global, not only shared by all extensible variants and exceptions but every new object increments the identifier (i.e., it is the same global counter which is used by `Oo.id`, which is probably an error which should be fixed in the compiler), therefore there is a chance to overflow it. That's why we decided to implement our own indexing, for example. [1]: https://github.com/janestreet/base/blob/master/src/type_equal.mli [2]: https://github.com/janestreet/typerep > > I'd also like to draw attention to truly type-indexed heterogeneous > collections where trep is a part of a key rather than a part of a > value. I like to treat such structures as a reification of OCaml records so that trep is now a first-class field and a record is an n-tuple with named fields. Since the fields are named, the n-tuple can grow and shrink, i.e., the size is not fixed. We can implement the n-tuple using heterogeneous maps, hashtables, or just an assoc list. So far we had a few libraries which provided heterogeneous maps indexed by the type index, the `Univ_map` [3] from Janestreet and Hmap [4] from Daniel Bünzli, to name a few. Both libraries follow the same approach, namely parametrizing the existing non-heterogeneous Map functor with the order function induced by the age of a key, with some minor differences, e.g., Base's version is using the int type as the key (where the key denotes the extension constructor identifier), while Daniel is using the trep itself as the key, and extracting the order from the age of the key. However, though semantically data is indeed indexed by the trpep, syntactically it is represented with an extra layer of indirection, e.g., instead of having a single binding type 'key binding = Binding : 'a trep * 'a -> 'key binding we have a non-heterogeneous binding type ('a,'b) binding = Binding of 'a * 'b which packs a universal something like this as `Binding (trep,Pack (trep,x))`. This creates a lot of overhead memory-wise and (given that OCaml performance is usually conditioned by the allocation rate) performance-wise. OCaml AVL-trees are already having a lot of overhead, about 5 extra words per bindings (Base has a little bit less, but still a lot - about 3 words per binding). Therefore, (after lots of profiling) we actually ended up implementing heterogenous AVL trees, which doesn't suffer from this problem. We ended up with the following representation [5] ``` type record = | T0 | T1 : 'a key * 'a -> record | T2 : 'a key * 'a * 'b key * 'b -> record | T3 : 'a key * 'a * 'b key * 'b * 'c key * 'c -> record | T4 : 'a key * 'a * 'b key * 'b * 'c key * 'c * 'd key * 'd -> record | LL : record * 'a key * 'a * record -> record (* h(x) = h(y) - 1 *) | EQ : record * 'a key * 'a * record -> record (* h(x) = h(y) *) | LR : record * 'a key * 'a * record -> record (* h(x) = h(y) + 1 *) ``` Which stores the key and data directly on the branches of a tree without any unnecessary indirection. And also unfolds n-tuples with n < 5, an implementation detail which is not really important wrt to the current discussion, (but was a dealbreaker for us as it significantly reduced the memory consumption and the total number of rebalances, so that at the end of the day we got a factor of 5 improvements both in time and space). Another interesting feature is that if implemented as a functor, this implementation could be used to derive non-heterogeneous maps (e.g., when `'a key = int`). During the implementation, we had to find solutions to a few very interesting problems, like how to represent an existential folding function (or how to fold over heterogeneous map)[6]. Or more interesting, how to update keys and merge two maps [7] and do this efficiently (hint: you have to use CPS). [3]: https://github.com/janestreet/core_kernel/blob/master/src/univ_map.ml [4]: https://github.com/dbuenzli/hmap/blob/master/src/hmap.ml [5]: https://github.com/BinaryAnalysisPlatform/bap/blob/0352edfe42ba5560b178b6bf990cf15e81d78f57/lib/knowledge/bap_knowledge.ml#L766 [6]: https://github.com/BinaryAnalysisPlatform/bap/blob/0352edfe42ba5560b178b6bf990cf15e81d78f57/lib/knowledge/bap_knowledge.ml#L824 [7]: https://github.com/BinaryAnalysisPlatform/bap/blob/0352edfe42ba5560b178b6bf990cf15e81d78f57/lib/knowledge/bap_knowledge.ml#L1316 Treating heterogenous maps as a generalization of records brings us to another interesting development. We do not want to completely forfeit types of records and treat all records as a member of one universal record type. We would like to be able to define type schemes so that we can distinguish between a `student record` and a `course record` while keeping both universal and extensible. In BAP we implemented this using classes and slots (borrowing those ideas from frame languages of AI, any resemblance to OO is purely coincidental). We turn our untyped `record` into a value parameterized by its class, e.g., ``` type 'a value = { cls : 'a cls; data : record; } ``` The `'a cls` type could be phantom, e.g., `type 'a cls = 'a`, but we can benefit from storing some type information to implement runtime reflection. And an extra layer of indirection on top of treps enables the structural definition of a record type that can span across multiple modules: ``` type ('a,'p) slot = { cls : 'a cls; key : 'p key; } ``` so that now a class is defined by its slots, e.g., ``` val name : (student, string) slot val age : (student, age) slot ... val teacher : (course, teacher) slot ``` and an abstract interface of the Value will prevent us from confusing different fields: ``` module Value : sig type 'a t val get : ('a,'p) slot -> 'a t -> 'p val put : ('a,'p) slot -> 'a t -> p -> 'a t end ``` The real implementation in BAP [8], is a little bit more convoluted since we want to create hierarchies of classes (which we need for type-safe representation of their denotational semantics) and make classes indexable by runtime values. Therefore our class is actually a collection of sorts. And we also have triggers (i.e., computable fields), as well as we use domains (aka Scott-Ershov domains) to represent the properties of classes, which gives us a nice feature - our `Value.get` function is total as for each type of property we have the bottom value as the default. Finally, we can store our values in a database and hide this storage under a monad interface, so that we can implement different access schemes (and put a fixed point computation inside), but this is a completely different story. The takeaway is that OCaml as a language is now fully equipped for implementing efficient heterogeneous data structures and can be used in domains which previously were previously dominated by languages with dynamic typing. Besides, the Knowledge library is totally independent on BAP despite the fact that it is currently distributed from the BAP repository. We've tried not to leak any domain-specific details into the knowledge abstraction albeit keeping it versatile enough to be able to represent the knowledge representation of the program semantics. [8]: https://github.com/BinaryAnalysisPlatform/bap/blob/master/lib/knowledge/bap_knowledge.mli#L153 Cheers, Ivan Gotovchits [-- Attachment #2: Type: text/html, Size: 12168 bytes --]

> https://github.com/BinaryAnalysisPlatform/bap - the BAP project per se. > ... That is quite a project! And interesting, too. Thank you for letting me know. Now I understand what you mean by ``universe of types actually grew quite large, that large that the linear search in the registry is not an option for us anymore.'' What your message has made it very clear, to me, is that we really need the standard type representation library -- hopefully being part of Stdlib and eventually integrated with the compiler. For one, it is high time we standardized the spelling of the ('a,'b) eq type and its constructor. Mainly, as your message has well demonstrated, an efficient trep is actually non-trivial, and takes lots of experience to design. Incidentally, the situation on Haskell is very similar: Typeable is now well integrated with the compiler. It is quite a popular library. I'd also like to draw attention to truly type-indexed heterogeneous collections where trep is a part of a key rather than a part of a value. To explain what I mean, let's recall the state of the art of heterogeneous collections. Let ('key,'v) coll be an ordinary homogeneous collection (a map, a hashtable, or an associative list) with a look-up function lookup : 'key -> ('key,'v) coll -> 'v option We can turn it into a heterogeneous collection that stores data of various types by using dynamics dyn: an existential that contains the data of some type t along with t trep, the representation of the type t. You have showed a very efficient dyn (which I will keep in mind, thank you). The dyn extraction from_dyn_opt : 'a trep -> dyn -> 'a option checks if the trep given as an argument matches trep stored inside dyn, and if so, returns dyn's value, of the requested type. Related from_dyn : 'a trep -> dyn -> 'a throws an exception on mismatch. The heterogeneous collection is then ('key, dyn) coll, with the look-up operation that is a `composition' of lookup and from_dyn let lookup_het : 'key -> 'a trep -> ('key,dyn) coll -> 'a option = fun key trep coll -> match lookup key coll with | None -> None | Some dyn -> Some (from_dyn trep dyn) I grant the elegance of the implementation and the reuse of the existing collections. What bothers me however is that the 'a trep is a part of the element value (part of dyn) rather a part of the key. The real lookup is done solely on the key, and the trep comparison is used as a verification, just to make sure we found the right dyn. If the code is correct, the check does not fail. Somehow I am always bothered by operations whose results isn't actually used but still have to be done. Wouldn't it be nice if all operations advanced us towards the goal, with no need for looking back and double-checking. Heterogeneous collections, at least, could be designed that way. Here is the gist: type 'key binding = B : 'key * 'a trep * 'a -> 'key binding (a more efficient existential could be designed, following the ideas of your message.) The binding is what its name says: an association of the key, the trep, and the value. The simplest heterogeneous collection, the analogue of association lists, is a list of bindings. type 'key halist = 'key binding list let lookup_hetkey : type a key. key -> a trep -> key halist -> a option = fun key trep coll -> let rec loop : key halist -> a option = function | [] -> None | B (key',trep',v) :: t -> match (key=key',teq trep' trep) with | (true,Some Refl) -> Some v | _ -> loop t in loop coll Now both key and trep equally participate in search: the mismatch of trep and trep' is not a failure but an indicator to continue search. The clear drawback is that the shown code uses a linear search -- and we cannot use off-the-shelf Maps or hashtables to speed it up. Still, an adaptation of an extant Hashtable is rather straightforward. In fact, the following file http://okmij.org/ftp/ML/hetcoll.ml shows the implementation of type-indexed heterogeneous hash tables. It is almost the same as Stdlib.Hashtable, but stripped to bare minimum and slightly adjusted. (The biggest adjustment has nothing to do with types; I simply didn't like how resizing was implemented). module type TypedHashedType = sig type t (* key type *) val equal: t -> t -> bool (* key equality *) val hash: t -> 'a trep -> int (* Hash the key and trep *) end module type S = sig type key type t val create: int -> t val clear : t -> unit val add: t -> key -> 'a trep -> 'a -> unit val find_opt: t -> key -> 'a trep -> 'a option val length: t -> int end Although the interface is very minimal, it is enough for registering your types and classes and my canonical functions. Stdlib.Map could likewise be adjusted.

[-- Attachment #1: Type: text/plain, Size: 2010 bytes --] Call for participation: School and Colloquium 16th International Colloquium on Theoretical Aspects of Computing (ICTAC 2019) http://ictac2019.redcad.org Alhambra Hotel, Yassmine Hammamet, Tunisia 31st October - 4th November 2019 The aim of this colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing. ICTAC also aims to promote research cooperation between developing and industrial countries. A school will be held as a pre-program to the ICTAC2019 Colloquium from from 31st October to 1st November 2019. Leaders in the field will give lectures on the practice, research, and state of the art in Theoretical Aspects of Computing. ------- Registration is open as follows: • Early – Before 1 September • Late – Before 1 October • On site – After 31 October Registration is via the ICTAC2019 website: http://www.redcad.org/events/ictac2019/Website/registration.html ------- Programme Information The conference will feature invited speakers and presentations of accepted papers. More details on the programme: http://www.redcad.org/events/ictac2019/Website/program.html ------- Invited Speakers School Speakers Patrick Cousot, New York University, USA Kamel Barkaoui, Conservatoire National des Arts et Métiers, Paris, France Dominique Méry, LORIA, Université de Lorraine, France Akka Zemmari, University of Bordeaux, France Keynote Speakers Patrick Cousot, New York University, USA Thomas A. Henzinger, Institute of Science and Technology, Austria Dominique Méry, LORIA, Université de Lorraine, France ------- Chairs General chairs: Mohamed Jmaiel, University of Sfax, Tunisia Walid Gaaloul, Paris-Saclay University, France Programme chairs: Robert M. Hierons, University of Sheffield, United Kingdom Mohamed Mosbah, LaBRI, Bordeaux INP, France [-- Attachment #2: Type: text/html, Size: 2346 bytes --]

--------------------------------------------------------------------------- CALL FOR PARTICIPATION TAPAS 2019 10th Workshop on Tools for Automatic Program Analysis Part of the 3rd World Congress on Formal Methods Porto, Portugal, October 8, 2019 http://staticanalysis.org/tapas2019 --------------------------------------------------------------------------- ABOUT TAPAS 2019 is a satellite workshop of SAS 2019, the 26th Static Analysis Symposium. It is intended to promote discussions between users of static analysis tools, and specialists in all areas of program analysis design and implementation. REGISTRATION Register via the FM'19 World Congress at http://bit.ly/fm19-register: - Early until Sep 10 (AoE) - Late from Sep 11 until 5 Oct (AoE) - On site from Oct 6 to Oct 11 (AoE) INVITED TALKS - Pascal Lacabanne (Airbus) - Bernard Schmidt (Bosch) PROGRAM The conference program is available at https://easychair.org/smart-program/TAPAS2019/. FM'19 WORLD CONGRESS For additional information about the 3rd World Congress on Formal Methods, visit http://formalmethods2019.inesctec.pt/. Hope to see you in Porto! David Delmas, Program Chair

[-- Attachment #1: Type: text/plain, Size: 12124 bytes --] Very interesting and thought-provoking writeup, thank you! Incidentally, we're investigating the same venues, in our CMU BAP project, as we found out that we need the extensibility in the style of type classes/canonical structures to decouple complex dependencies which arise in the program analysis domain. In fact, we build our new BAP 2.0 framework largely on your [tagless-final][1] style which, let's admit it, works much better with type classes. Therefore we ended up implementing extensible type representations along with registries for our type classes. Unfortunately, the idea of storing rules in the registry didn't visit us, but we're now thinking about how to incorporate it (the classes that we have are very nontrivial, usually having hundreds of methods, so we're currently using functors to manually derive on class from another, and registering the resulting structures - but using your approach we can register functors as well and automate the derivation). We also didn't generalize the type class instantiation, so our solutions do have some boilerplate (but I have to admit, that the total number of type classes that we need is not very big, so it really never bothered us). What could be surprising is that the universe of types actually grew quite large, that large that the linear search in the registry is not an option for us anymore. In fact, we have so many comparisons between treps, that instead of extracting the extension constructor number from an extensible variant we had to rely on our own freshly generated identifier. But I'm running in front of myself, an important lesson that we have learned is that treps should not only be equality comparable but also ordered (and even hashable) so that we can implement our registries as hash tables. It is also better to keep them abstract so that we can later extend them without breaking user code (to implement introspection as well as different resolution schemes). This is basically an elaboration of your approach (which is also could be commonly found in Janestreet's Core (Type_equal.Uid.t) and other implementations of existentials). In our case, we ended up with the following implementation ``` type 'a witness = .. module type Witness = sig type t type _ witness += Id : t witness end type 'a typeid = (module Witness with type t = 'a) type 'a key = { ord : int; key : 'a typeid; name : string; (* for introspection *) show : 'a -> Sexp.t; (* also for introspection *) } ``` Now, we can use the `ord` field to order types, compare them, store in maps, hash tables, and even arrays. E.g., this is how our `teq` function looks like, ``` let same (type a b) x y : (a,b) Type_equal.t = if x.id = y.id then let module X = (val x.key : Witness with type t = a) in let module Y = (val y.key : Witness with type t = b) in match X.Id with | Y.Id -> Type_equal.T | _ -> failwith "broken type equality" else failwith "types are not equal" ``` It is often used in the context where we already know that `x.id = y.id`, e.g., when we already found an entry, so we just need to obtain the equality witness (we use Janestreet's Type_equal.T, which is the same as yours eq type). Concerning the representation of the registry, we also experimented with different approaches (since we have a few ways to make a type existential in OCaml), and found out the following to be the most efficient and easy to work with, ``` type ordered = { order : 'a. 'a key -> 'a -> 'a -> int; } [@@unboxed] ``` Notice, that thanks to `[@@unboxed]` we got a free unpacked existential. We will next store `ordered` in our registry, which is a hash table, ``` let ordered : ordered Hashtbl.M(Int).t = Hashtbl.create (module Int) ``` and register it as simple as, ``` let register: type p. p Key.t -> (p -> p -> int) -> unit = fun key order -> Hashtbl.add_exn vtables ~key:(uid key) ~data:{ order = fun (type a) (k : a key) (x : a) (y : a) -> let T = same k key in (* obtain the witness that we found the right structure *) order x y } ``` Instead of a hashtable, it is also possible to use `ordered array ref` (since our `ord` is just an integer which we increment every time a new class is declared). This will give us even faster lookup. I hope that this was interesting. And if yes, I'm ready to elaborate more on our design decision or to hear suggestions and critics. Here are a few links: - https://github.com/BinaryAnalysisPlatform/bap - the BAP project per se. - https://binaryanalysisplatform.github.io/knowledge-intro-1 - a small introductionary post about BAP 2.0 Knowledge representation - https://github.com/BinaryAnalysisPlatform/bap/blob/master/lib/knowledge/bap_knowledge.ml - the implementation of the knowledge system - https://github.com/BinaryAnalysisPlatform/bap/tree/master/lib/bap_core_theory - The Core Theory, an exemplar type class of the theory that we're developing :) Cheers, Ivan Gotovchits Research Scientist, CMU Cylab [1]: http://okmij.org/ftp/tagless-final/index.html On Wed, Sep 4, 2019 at 11:23 AM Oleg <oleg@okmij.org> wrote: > > This is to announce a simple, plain OCaml library to experiment with > type-class/implicits resolution, which can be thought of as evaluating > a Prolog-like program. One may allow `overlapping instances' -- or > prohibit them, insisting on uniqueness. One may make the search fully > deterministic, fully non-deterministic, or something in-between. > There is an immediate, albeit modest practical benefit: the facility > like "#install_printer", which was restricted to top-level, is now > available for all -- as a small, self-contained, plain OCaml library > with no knowledge or dependencies on the compiler internals. We show > an example at the end of the message. > > This message has been inspired by the remarkable paper > Canonical Structures for the working Coq user > Assia Mahboubi, Enrico Tassi > DOI: 10.1007/978-3-642-39634-2_5 > Its introduction is particularly insightful: the power of > (mathematical) notation is in eliding distracting details. Yet to > formally check a proof, or to run a program, the omitted has to be > found. When pressed to fill in details, people `skillful in the art' > look in the database of the `state of the art', with the context as > the key. Computers can be programmed similarly; types well represent > the needed context to guide the search. > > Mahboubi and Tassi's paper explains very well how this eliding and > filling-in is realized, as a programmable unification, and used in > Coq. Yet their insights go beyond Coq and deserve to be known better. > This message and the accompanying code is to explain them in > plain OCaml and encourage experimentation. It could have been titled > `Canonical Structures for the working OCaml (meta) programmer'. > > The rudiment of canonical structures is already present in OCaml, in > the form of the registry of printers for user-defined types. This > facility is available only at the top-level, however, and deeply > intertwined with it. As a modest practical benefit, this facility is > now available for all programs, as a plain, small, self-contained > library, with no compiler or other magic. The full potential of the > method is realized however in (multi-) staged programming. In fact, I'm > planning to use it in the upcoming version of MetaOCaml to implement > `lifting' from a value to the code that produces it -- letting the > users register lifting functions for their own data types. > > > http://okmij.org/ftp/ML/canonical.ml > The implementation and the examples, some of which are noted below. > http://okmij.org/ftp/ML/trep.ml > A generic library of type representations: something like > Typeable in Haskell. Some day it may be built-in into the compiler > http://okmij.org/ftp/ML/canonical_leadup.ml > A well-commented code that records the progressive development of > canonical.ml. It is not part of the library, but may serve as > its explanation. > > Here are a few examples, starting with the most trivial one > module Show = MakeResolve(struct type 'a dict = 'a -> string end) > let () = Show.register Int string_of_int (* Define `instances' *) > let () = Show.register Bool string_of_bool > Show.find Int 1;; > > However contrived and flawed, it is instructive. Here (Int : int trep) > is the value representing the type int. The type checker can certainly > figure out that 1 is of the type int, and could potentially save us > trouble writing Int explicitly. What the type checker cannot do by > itself is to find out which function to use to convert an int to a > string. After all, there are many of them. Show.register lets us > register the *canonical* int->string function. Show.find is to search > the database of such canonical functions: in effect, finding *the* > evidence that the type int->string is populated. Keeping Curry-Howard > in mind, Show.find does a _proof search_. > > The type of Show.find is 'a trep -> ('a -> string). Compare with > Haskell's show : Show a => a -> String (or, desuraging => and Show) > show : ('a -> string) -> ('a -> string). Haskell's show indeed does > not actually do anything: it is the identity function. All the hard > work -- finding out the right dictionary (the string producing > function) -- is done by the compiler. If one does not like the way the > compiler goes about it -- tough luck. There is little one may do save > complaining on reddit. In contrast, the first argument of Show.find is > trivial: it is a mere reflection of the type int, with no further > information. Hence Show.find has to do a non-trivial work. In the > case of int, this work is the straightforward database search -- > or, if you prefer, running the query ?- dict(int,R) against a logic > program > dict(int,string_of_int). > dict(bool,string_of_bool). > The program becomes more interesting when it comes to pairs: > dict(T,R) :- T = pair(X,Y), !, > dict(X,DX), dict(Y,DY), R=make_pair_dict(DX,DY). > Here is how it is expressed in OCaml: > let () = > let open Show in > let pat : type b. b trep -> b rule_body option = function > | Pair (x,y) -> > Some (Arg (x, fun dx -> Arg (y, fun dy -> > Fact (fun (x,y) -> "(" ^ dx x ^ "," ^ dy y ^ ")")))) > | _ -> None > in register_rule {pat} > > let () = Show.register (Pair(Bool,Bool)) > (fun (x,y) -> string_of_bool x ^ string_of_bool y) > > Our library permits `overlapping instances'. We hence registered the > printer for generic pairs, and a particular printer just for pairs of > booleans. > > The library is extensible with user-defined data types, for example: > type my_fancy_datatype = Fancy of int * string * (int -> string) > > After registering the type with trep library, and the printer > type _ trep += MyFancy : my_fancy_datatype trep > let () = Show.register MyFancy (function Fancy(x,y,_) -> > string_of_int x ^ "/" ^ y ^ "/" ^ "<fun>") > > one can print rather complex data with fancy, with no further ado: > Show.find (List(List(Pair(MyFancy,Int)))) [[(Fancy ...,5)];[]] > > As Mahboubi and Tassi would say, proof synthesis at work! > > We should stress that what we have described is not a type-class > facility for OCaml. It is *meta* type-class facility. Show.find has > many drawbacks: we have to explicitly pass the trep argument like > Int. The resolution happens at run time, and hence the failure of the > resolution is a run-time exception. But the canonical instance > resolution was intended to be a part of a type checker. There, the > resolution failure is a type checking error. The trep argument, > representing the type in the object program, is also at > hand. Likewise, the drawbacks of Show.find disappear when we use the > library in a meta-program (code generator). The library then becomes a > type-class/implicits facility, for the generated code -- the facility, > we can easily (re)program. > [-- Attachment #2: Type: text/html, Size: 14810 bytes --]

This is to announce a simple, plain OCaml library to experiment with type-class/implicits resolution, which can be thought of as evaluating a Prolog-like program. One may allow `overlapping instances' -- or prohibit them, insisting on uniqueness. One may make the search fully deterministic, fully non-deterministic, or something in-between. There is an immediate, albeit modest practical benefit: the facility like "#install_printer", which was restricted to top-level, is now available for all -- as a small, self-contained, plain OCaml library with no knowledge or dependencies on the compiler internals. We show an example at the end of the message. This message has been inspired by the remarkable paper Canonical Structures for the working Coq user Assia Mahboubi, Enrico Tassi DOI: 10.1007/978-3-642-39634-2_5 Its introduction is particularly insightful: the power of (mathematical) notation is in eliding distracting details. Yet to formally check a proof, or to run a program, the omitted has to be found. When pressed to fill in details, people `skillful in the art' look in the database of the `state of the art', with the context as the key. Computers can be programmed similarly; types well represent the needed context to guide the search. Mahboubi and Tassi's paper explains very well how this eliding and filling-in is realized, as a programmable unification, and used in Coq. Yet their insights go beyond Coq and deserve to be known better. This message and the accompanying code is to explain them in plain OCaml and encourage experimentation. It could have been titled `Canonical Structures for the working OCaml (meta) programmer'. The rudiment of canonical structures is already present in OCaml, in the form of the registry of printers for user-defined types. This facility is available only at the top-level, however, and deeply intertwined with it. As a modest practical benefit, this facility is now available for all programs, as a plain, small, self-contained library, with no compiler or other magic. The full potential of the method is realized however in (multi-) staged programming. In fact, I'm planning to use it in the upcoming version of MetaOCaml to implement `lifting' from a value to the code that produces it -- letting the users register lifting functions for their own data types. http://okmij.org/ftp/ML/canonical.ml The implementation and the examples, some of which are noted below. http://okmij.org/ftp/ML/trep.ml A generic library of type representations: something like Typeable in Haskell. Some day it may be built-in into the compiler http://okmij.org/ftp/ML/canonical_leadup.ml A well-commented code that records the progressive development of canonical.ml. It is not part of the library, but may serve as its explanation. Here are a few examples, starting with the most trivial one module Show = MakeResolve(struct type 'a dict = 'a -> string end) let () = Show.register Int string_of_int (* Define `instances' *) let () = Show.register Bool string_of_bool Show.find Int 1;; However contrived and flawed, it is instructive. Here (Int : int trep) is the value representing the type int. The type checker can certainly figure out that 1 is of the type int, and could potentially save us trouble writing Int explicitly. What the type checker cannot do by itself is to find out which function to use to convert an int to a string. After all, there are many of them. Show.register lets us register the *canonical* int->string function. Show.find is to search the database of such canonical functions: in effect, finding *the* evidence that the type int->string is populated. Keeping Curry-Howard in mind, Show.find does a _proof search_. The type of Show.find is 'a trep -> ('a -> string). Compare with Haskell's show : Show a => a -> String (or, desuraging => and Show) show : ('a -> string) -> ('a -> string). Haskell's show indeed does not actually do anything: it is the identity function. All the hard work -- finding out the right dictionary (the string producing function) -- is done by the compiler. If one does not like the way the compiler goes about it -- tough luck. There is little one may do save complaining on reddit. In contrast, the first argument of Show.find is trivial: it is a mere reflection of the type int, with no further information. Hence Show.find has to do a non-trivial work. In the case of int, this work is the straightforward database search -- or, if you prefer, running the query ?- dict(int,R) against a logic program dict(int,string_of_int). dict(bool,string_of_bool). The program becomes more interesting when it comes to pairs: dict(T,R) :- T = pair(X,Y), !, dict(X,DX), dict(Y,DY), R=make_pair_dict(DX,DY). Here is how it is expressed in OCaml: let () = let open Show in let pat : type b. b trep -> b rule_body option = function | Pair (x,y) -> Some (Arg (x, fun dx -> Arg (y, fun dy -> Fact (fun (x,y) -> "(" ^ dx x ^ "," ^ dy y ^ ")")))) | _ -> None in register_rule {pat} let () = Show.register (Pair(Bool,Bool)) (fun (x,y) -> string_of_bool x ^ string_of_bool y) Our library permits `overlapping instances'. We hence registered the printer for generic pairs, and a particular printer just for pairs of booleans. The library is extensible with user-defined data types, for example: type my_fancy_datatype = Fancy of int * string * (int -> string) After registering the type with trep library, and the printer type _ trep += MyFancy : my_fancy_datatype trep let () = Show.register MyFancy (function Fancy(x,y,_) -> string_of_int x ^ "/" ^ y ^ "/" ^ "<fun>") one can print rather complex data with fancy, with no further ado: Show.find (List(List(Pair(MyFancy,Int)))) [[(Fancy ...,5)];[]] As Mahboubi and Tassi would say, proof synthesis at work! We should stress that what we have described is not a type-class facility for OCaml. It is *meta* type-class facility. Show.find has many drawbacks: we have to explicitly pass the trep argument like Int. The resolution happens at run time, and hence the failure of the resolution is a run-time exception. But the canonical instance resolution was intended to be a part of a type checker. There, the resolution failure is a type checking error. The trep argument, representing the type in the object program, is also at hand. Likewise, the drawbacks of Show.find disappear when we use the library in a meta-program (code generator). The library then becomes a type-class/implicits facility, for the generated code -- the facility, we can easily (re)program.

ACM Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH'19) Athens, Greece Sun 20 - Fri 25 October 2019 2019.splashcon.org twitter.com/splashcon www.facebook.com/SPLASHCon Sponsored by ACM SIGPLAN SPLASH is the ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity. SPLASH embraces all aspects of software construction and delivery, to make it the premier conference on the applications of programming languages--at the intersection of programming languages and software engineering. SPLASH 2019 will take place in Athens from Sunday 20th to Friday 25th of October 2019. SPLASH includes the following co-located conferences: OOPSLA, Onward!, GPCE, SLE, DLS (note changed date), and MPLR; as well as a large array of workshops and events. The Rebase track (formerly “SPLASH-I”) aims to deliver presentations of interest to software practitioners and researchers alike. Rebase will feature perspectives from industry giants, to rocketship startups, to academic research, and solutions from algorithms to physical computing, to quantum computing. Registration ------------ ** Friday, 20th September 2019 (Early Deadline) ** <-- very soon! * Contact: info at splashcon.org * Register: https://2019.splashcon.org/attending/Registration * Venue: https://2019.splashcon.org/venue/splash-2019-venue Conference ---------- OOPSLA 2019 https://2019.splashcon.org/track/splash-2019-oopsla Onward! Papers https://2019.splashcon.org/track/splash-2019-Onward-papers Onward! Essays https://2019.splashcon.org/track/splash-2019-Onward-essays Rebase https://2019.splashcon.org/track/splash-2019-rebase Dynamic Languages Symposium (DLS) *Note*: DLS’19 will be on Sunday instead of its usual slot https://conf.researchr.org/home/dls-2019 Generative Programming: Concepts & Experiences (GPCE) https://conf.researchr.org/home/gpce-2019 Software Language Engineering (SLE) https://conf.researchr.org/home/sle-2019 Managed Programming Languages and Runtimes (MPLR) https://conf.researchr.org/home/mplr-2019 SPLASH-E https://2019.splashcon.org/track/splash-2019-SPLASH-E Doctoral Symposium http://2019.splashcon.org/track/splash-2019-Doctoral-Symposium Student Research Competition https://2019.splashcon.org/track/splash-2019-SRC Workshops --------- AGERE (Actors, Agents, and Decentralized Control) https://2019.splashcon.org/home/agere-2019 AI-SEPS (AI-Inspired and Empirical Methods for SE on Parallel Computing Systems) https://2019.splashcon.org/home/seps-2019 DSM (Domain-Specific Modeling) https://2019.splashcon.org/home/dsm-2019 IC (Incremental Computing) https://2019.splashcon.org/home/ic-2019 LIVE (Live Programming) https://2019.splashcon.org/home/live-2019 META (Metaprogramming) https://2019.splashcon.org/home/meta-2019 NJR (Normalized Java Resource) https://2019.splashcon.org/home/njr-2019 REBLS (Reactive and Event-based Languages and Systems) https://2019.splashcon.org/home/rebls-2019 STOKED (Spatio-Temporal platforms for Observations and Knowledge of Earth Data) https://2019.splashcon.org/home/stoked-2019 VMIL (Virtual Machines and Intermediate Languages) https://2019.splashcon.org/home/vmil-2019 Looking forward to seeing you in Athens!