Lin_api.int_bound polymorphism

[jmid]

There's an issue with the current definition of Lin_api.int_bound, resulting in a confusing error message.

Consider changing a test to use it, e.g., src/hashtbl/lin_tests_dsl.ml:

--- a/src/hashtbl/lin_tests_dsl.ml
+++ b/src/hashtbl/lin_tests_dsl.ml
@@ -9,7 +9,7 @@ struct
   let cleanup _ = ()

   open Lin_api
-  let int,char = nat_small,char_printable
+  let int,char = int_bound 10,char_printable
   let api =
     [ val_ "Hashtbl.clear"    Hashtbl.clear    (t @-> returning unit);
       val_ "Hashtbl.add"      Hashtbl.add      (t @-> char @-> int @-> returning unit);

This change yields a confusing type error in the use of the int variable:

File "src/hashtbl/lin_tests_dsl.ml", line 17, characters 80-83:
17 |       val_ "Hashtbl.find"     Hashtbl.find     (t @-> char @-> returning_or_exc int);
                                                                                     ^^^
Error: This expression has type
         (int, constructible, (char, int) Hashtbl.t, combinable) ty
       but an expression was expected of type
         (int, deconstructible, 'a, combinable) ty
       Type constructible is not compatible with type deconstructible 

I believe this may be caused by value restriction not permitting a computation int_bound 10 to have polymorphic type, and hence forcing the ghost type parameter to constructible. Whether this is correctly understood and if so, how to fix it is a bit up in the air...

[n-osborne]

I'm no expert with GADT, but I think it makes sense that the computation int_bound 10 fixes the type parameter:

• if the api list does not contains any int, then int has type (int, '_weak**, '_weak**, combinable) ty
• if we change the order in the api list so that the type checker encounter its first int in an argument position, the error message is the other way around:

  open Lin_api
  let int,char = int_bound 10 ,char_printable
  let api =
    [ val_ "Hashtbl.clear"    Hashtbl.clear    (t @-> returning unit);
      val_ "Hashtbl.find"     Hashtbl.find     (t @-> char @-> returning_or_exc int);
      val_ "Hashtbl.add"      Hashtbl.add      (t @-> char @-> int @-> returning unit);

gives:

$ dune build
File "src/hashtbl/lin_tests_dsl.ml", line 16, characters 63-66:
16 |       val_ "Hashtbl.add"      Hashtbl.add      (t @-> char @-> int @-> returning unit);
                                                                    ^^^
Error: This expression has type
         (int, deconstructible, (char, int) Hashtbl.t, combinable) ty
       but an expression was expected of type (int, constructible, 'a, 'b) ty
       Type deconstructible is not compatible with type constructible

The easy way would be to warn the user to use int_bound directly in the declaration (in the api list) and not define an alias.

[n-osborne]

I've taken a look at how Monolith deal with this problem.

The way it is design, there is a type ('a, 'b) Spec that can be either constructible or deconstructible. Then, this type has also a SpecIfPol constructor that takes both a constructible and a deconstructible Spec, the right one being picked up at a normalization step depending on the polarity (situation in the type of the function IIUC).

Here, the constructor GenDeconstr has all the information to construct and deconstruct the value, but the type system has to make a choice when int_bound n is evaluated the first time.

I think we could benefit from taking this idea from Monolith.

[jmid]

This limitation has now been documented in #245. The trick is to use the result of Lin.int_bound to describe arguments and use a plain Lin.int for results.