Confusion about types

Context: I’m working through bonsai/02-dynamism.md at master · janestreet/bonsai · GitHub . In particular, the following example:

  1. The code compiles fine.
  2. The additional type annotations are added by me, but otherwise the code is unchanged.
  3. My question is: the type annotations make no sense to me.
let juxtapose_digits ~(delimiter : string) (a : int Value.t) (b : int Value.t) : string Computation.t =
  let%arr (a : int) = a and (b : int) = b in
  (Int.to_string a ^ delimiter ^ Int.to_string b : string)

let _juxtapose_and_sum (a : int Value.t) (b : int Value.t) : string Computation.t =
  let%sub (juxtaposed : string) = juxtapose_digits ~delimiter:" + " a b in
  let%sub (sum : string) =
    let%arr (a : int) = a and (b : int) = b in
    Int.to_string (a + b)
  in
  let%arr (juxtaposed : string) = (juxtaposed : string Value.t) and (sum : string) = (sum : string Value.t) in
  juxtaposed ^ " = " ^ sum

The above code compiles fine. That is not my question.

I’m now going to annotate 3 lines:

Line 1 ###  let%sub (juxtaposed : string) = juxtapose_digits ~delimiter:" + " a b in
Line 2 ###  let%sub (sum : string) =
...
Line 3 ### let%arr (juxtaposed : string) = (juxtaposed : string Value.t) and (sum : string) = (sum : string Value.t) in

Here comes the WTF part.

In line 1 & 2, we defined juxtaposed / sum to have type `string.

In line 3, the magically become string Value.t

How does this happen ?

1 Like

Hmm, yeah this is weird.

tl;dr: It’s because of the generated ppx code that the type of juxtaposed seems to magically change underneath you.


(This is a bit rambling, but it will get there eventually…)

Check it out, the type signature for Let_syntax.sub says this:

val sub : 
  ?here:Core.Source_code_position.t ->
  'a Computation.t ->
  f:('a Value.t -> 'b Computation.t) ->
  'b Computation.t

which means I would expect to treat juxtaposed as a string Value.t in this line:

  let%sub (juxtaposed : string Value.t) = juxtapose_digits ~delimiter:" + " a b in

but as I’m sure you noticed, if you put that type in there, you get a compile error something like this:

This pattern matches values of type string Value.t
but a pattern was expected which matches values of type string

Huh? Check these two things out right here:

let _juxtapose_and_sum (a : int Value.t) (b : int Value.t) :
    string Computation.t =
  let%sub (juxtaposed : string) = juxtapose_digits ~delimiter:" + " a b in
  (* This line gives an error... 
     This expression (juxtaposed) has type string Value.t 
     but an expression was expected of type string *)
  let _s = juxtaposed ^ " yoooo!" in
  failwith "..."

That’s weird, because earlier, when we try to annotate juxtaposed as a string Value.t it doesn’t compile saying that pattern matches a string, now in the next line, when we try to use juxtaposed as a string, compiler is saying that juxtaposed is in fact NOT a string at all, rather a string Value.t.

Okay, something clearly weird here. Just a sanity check, use the sub function directly and see it works as we expect.

let _juxtapose_and_sum' (a : int Value.t) (b : int Value.t) :
    string Computation.t =
  Let_syntax.sub (juxtapose_digits ~delimiter:" + " a b)
    ~f:(fun (juxtaposed : string Value.t) ->
      let (y : string Value.t) = (juxtaposed : string Value.t) in
      return y )

Yeah compiles fine and all the types look like they should. Okay so what is going on with this weirdness?

First of all, let’s simply the function in question to this:

let foo (a : int Value.t) (b : int Value.t) : string Computation.t =
  let%sub (juxtaposed : string) = juxtapose_digits ~delimiter:" + " a b in
  return (juxtaposed : string Value.t)

It has the values annotated so you can see them. Even though the compiler says this is correct, as you can see it doesn’t make any sense with what we know about sub. So let’s check the generated ppx code and see what’s going on. (Assume i have this in a file called yo.ml.)

$ ocamlc -stop-after parsing -dsource _build/default/yo.pp.ml 2> yo_gen.ml

And you’ll get a function that looks something like this:

let foo (a : int Value.t) (b : int Value.t) : string Computation.t =
  Let_syntax.sub
    ~here:
      { Ppx_here_lib.pos_fname= "yo.ml"
      ; pos_lnum= 24
      ; pos_cnum= 660
      ; pos_bol= 658 } (juxtapose_digits ~delimiter:" + " a b)
    ~f:(fun __pattern_syntax__008_ ->
      Let_syntax.sub
        ~here:
          { Ppx_here_lib.pos_fname= "yo.ml"
          ; pos_lnum= 24
          ; pos_cnum= 660
          ; pos_bol= 658 }
        (Let_syntax.return
           (Let_syntax.map __pattern_syntax__008_ ~f:(function
                | (__pattern_syntax__009_ : string) -> __pattern_syntax__009_ )
             [@merlin.hide] ) )
        ~f:(fun juxtaposed -> return (juxtaposed : string Value.t)) )

The odd thing there is how it’s doing the rewriting… see at the bottom where it is doing this:

(Let_syntax.return
           (Let_syntax.map __pattern_syntax__008_ ~f:(function
                | (__pattern_syntax__009_ : string) -> __pattern_syntax__009_ )
             [@merlin.hide] ) )

Here are the signatures of map and return in the Let_syntax module for reference:

val map : 'a Value.t -> f:('a -> 'b) -> 'b Value.t
val return : 'a Value.t -> 'a Computation.t

Let’s unpack it. __pattern_syntax__008_ is bound to the result of (juxtapose_digits ~delimiter:" + " a b) by the sub function in ~f. It’s a string Value.t because that’s what juxtapose_digits returns.

Now __pattern_syntax__008_ is passed to map:

           (Let_syntax.map __pattern_syntax__008_ ~f:(function
                | (__pattern_syntax__009_ : string) -> __pattern_syntax__009_ )
             [@merlin.hide] )

That f is basically an identity function, and the return value of the expr as a whole is also string Value.t (because that’s what map does). BUT check out that (__pattern_syntax__009_ : string) thing. Well that corresponds to our thing here (because that’s how the let syntax is working)

let%sub (juxtaposed : string) =
        ^^^^^^^^^^^^^^^^^^^^^

And yeah, in that context, __pattern_syntax__009_ (aka juxtaposed) is a string there in that pattern, because it is in the map function and that is what it expects to be there. (which is why you had to annotate is as a string…thats what it is there).

Okay, so that map expression will give you a string Value.t, and that is then passed to return which takes it and returns a string Computation.t. That computation is finally used as an argument to sub, and in THAT call’s function, juxtaposed is a string Value.t, which that is what return returns, and what sub expects. So here, juxtaposed is a string Value.t:

~f:(fun juxtaposed -> return (juxtaposed : string Value.t))

So yeah to answer your question…the type annotations make no sense unless you are looking at the ppx generated code. Now as to why the ppx generates code that happens to have those confusing (seemingly magically changing) types…I don’t have an an answer to that.

2 Likes

According to bonsai/bonsai.mli at master · janestreet/bonsai · GitHub, let%sub takes a 'a Computation.t and gives a 'a Value.t, not bare a 'a (as you’ve annotated). Something screwy happens that lets it slip past despite the incorrect annotations I guess, but it shouldn’t actually be 'a there.

  1. Thank you for the detailed response.

  2. Having written Lisp/Rust macros before, I think I get the gist of it, which condenses to: it’s just the way the macro expands. Possibly buggy, but the way it currently expands.

  3. I guess it’s also time I add

to my toolbox.

1 Like