Abstract away Sig_item_map module

[azzsal]

This should eventually resolve #96. I have implemented the empty value and the add function. The tests are failing since the diff function is yet to be implemented. @panglesd @NathanReb Please check if I am on the right track.

[azzsal]

@NathanReb Thank for the suggestions. I have taken them into account. I have added an initial implementation of the diff function, but the there is an error I couldn't solve. The first error suggests that a type_item is a concrete type, not an abstract type, the outer type a seems to be unrecognized as an abstract type in the diff_item function type. Please point me to resources about the issue.

[panglesd]

First, here is small list of resources on GADTs, which I'm sure you have already read.

• The language manual : https://ocaml.org/manual/5.2/gadts-tutorial.html
• The real world of ocaml chapter on GADTs : https://dev.realworldocaml.org/gadts.html
• Another tutorial on GADTs : https://discuss.ocaml.org/t/tutorial-on-gadts/14040

Now, here are some resources specific to your problem:

• https://ocaml.org/manual/5.2/polymorphism.html#s%3Ahigher-rank-poly
• https://discuss.ocaml.org/t/type-of-explicitly-polymorphic-function/11604/3

GADTs are notoriously hard! And those resources on your specific problem are a bit hidden when you don't know exactly what to search. Let me know if you have further problem! (Your current implementation is already very good and I appreciate that you asked for resources instead of a solution!)

[NathanReb]

The section you'll be interested in is this one: https://ocaml.org/manual/5.2/gadts-tutorial.html#s:gadts-recfun

The . in the type annotation is important as that's the part that means "For all types a". This can be a bit confusing.

[NathanReb]

Ok, my suggestion is a bit misleading. To better understand the situation here I suggest you read the manual chapter on polymoprhism: https://ocaml.org/manual/5.2/polymorphism.html and in particular this section: https://ocaml.org/manual/5.2/polymorphism.html#s:higher-rank-poly.

[panglesd]

Let me just emphasize that your problem actually has nothing to do with GADTs (although, this problem comes often in the case of a GADT.

When typing a structure item, OCaml introduces type variables. For instance, given:

let apply_and_add f x y = f x + f y

the typer starts by introducing type variables for f, x, y, for instance 'a, 'b and 'c. Then, it "infer" constraints on the types by reasoning on the expression. For instance, the fact that f is applied with x says that actually, 'a must be of the form 'b -> 'd. Similarly, 'a must be of the form 'c -> 'e. Therefore, 'b = 'c and 'd = 'e. The + says that 'd = int.

In the end, the type for apply_and_add is ('a -> int) -> 'a -> 'a -> int. There is an unbound variable here: 'a. The typer "quantify" it by interpreting the type as "For every type 'a, apply_and_add has the type ('a -> int) -> 'a -> 'a -> int". This quantification is written with a . in OCaml: in our example, 'a . ('a -> int) -> 'a -> 'a -> int This allows you to apply it in various context:

let square x = x * x
let _ = apply_and_add square 3 4
(* Works, because the quantified ['a] can be instanciated with type [int].
   Result is is 25 *)
let _ = apply_and_add List.length [1;2;3] [1;2]
(* Similar. Result is 5 *)
let _ = apply_and_add List.length [1;2;3] ["1";"2"]
(* Does not work: ['a] cannot be instanciated to any type that would make that work. *)

However, this quantification happens at the end of the typing of a structure item. In particular, the typer will nevel come up by itself with a quantification in the middle of a type, such as: ('x. 'x -> int) -> 'a -> 'b -> int. Having this would have made the previous example work...

In your case, you are applying diff_item once with Value (which has some type) and once with Module (which has a different type), so the typer fails to type the expression (since the typer cannot introduce a "forall" in the type of diff_item).

More information on the resources I linked!

[panglesd]

The section you'll be interested in is this one: https://ocaml.org/manual/5.2/gadts-tutorial.html#s:gadts-recfun

(To read only if you are confused with the syntax used in the link above! You do not need to know this to fix your error.)

One last precision on syntax, since it can be confusing.

You already know the locally abstract type syntax: (type a). I just introduced you the "forall" syntax (for instance 'a . 'a -> 'a). In the context of recursive function working with GADTs (not your case), there is a third syntax, which is actually just a combination of the two syntax you know: the type a . ... syntax.

Quoting this post:

let rec eval: type t. t term -> t = function

is actually a shorthand for the exactly equivalent:

let rec eval: 't. 't term -> 't = 
fun (type t) (x: t term): t ->

(But again, you don't need that!)

[azzsal]

@panglesd @NathanReb Thank you so much for the detailed explanations, they clarified a lot of things for me. I'll take the time to go through the linked resources to better understand parametric polymorphism in OCaml. I hope as I am working on the project to get a deeper understanding of type checking and type inference. I think I have found a solution to my problem by quickly reading Higher-rank polymorphic funcitons. I'll update the code to reflect that. Thanks again!

[NathanReb]

Well done!