Exposing equalities in variants

[Drup]

I attempted to use the variant feature in tyre. The goal was the following:

1. Functorize a common version that works on both re and Javascript
2. Have an extended version which uses re's specific features

The first step worked well (and the resulting organization is very pleasant compared to full functorization, I must say). I used a virtual module Regex and implemented various versions of it: everythings went well.

However, I couldn't complete the second step: I discovered that, unlike functors, I can't instructs variants to expose the additional type equalities that I need. In particular, in the variant implementation that uses re, I can't expose that Regex.t = Re.t.

@rgrinberg proposed to circumvent the abstraction by exposing another module that would have the type equalities. I'm not actually sure how that's possible (the OCaml type system doesn't really allow that), but I only got #2092 out of it.

For anyone wanting to experiment, here is the (failling) branch: https://github.com/Drup/tyre/tree/variant

[ghost]

I don't believe it is possible to expose such a type equality in only one implementation with variants. One thing you could do though is expose conversion functions between Regex.t and Re.t. The conversion functions would fail in the javascript implementation and they would be the identity in the re one.

However, that does mean that the main tyre library would always depend on re.

[Drup]

I don't want to expose "only one variant". I want the same behavior as functors: If I apply a functor of type (Regex : Regex) -> S to a module R, I know that the instances of Regex.type in S are really R.type.

That's not the case with variants.

However, that does mean that the main tyre library would always depend on re.

Well, that's on purpose. tyre is the normal API that most people would use. People who explicitly want to write cross-plateform code would use another package, with a subset of the API.

[ghost]

I don't think it's possible to get the same behaviour as functors with variants though. The underlying idea of variants is to have one identical shared interface on top of different implementations. If you expose a type equality in the shared interface, it has to hold in all the implementations.

I suppose you could have the re implementation expose a type equality witness though. For instance:

type 'a is_re = T : Re.t is_re
val is_re : Regex.t is_re

Would that work for your use case?

[Drup]

Functors also have "one identical shared interface". The type equalities only get introduced when you apply the functor, which in term of variant is when you link both a virtual library and its implementation.

I suppose you could have the re implementation expose a type equality witness though. For instance:

type 'a is_re = T : Re.t is_re
val is_re : Regex.t is_re

Doesn't that imply making the virtual library depend on re ?

[ghost]

Yh, I hear you but I have no idea how variants could support that :/

Doesn't that imply making the virtual library depend on re ?

It does. However, we could imagine allowing such a pattern. For instance, if the virtual library made no other references to re, then it could be only a compile time dependency of the virtual library. A bit like Unix used to be a compile time dependency of Bigarray.

I'm not too sure how we could expose such a feature to users in a nice and safe way though.

[Drup]

I'm not sure I like the idea of the compile-time only dependency. It seems ever more magical from the user's perspective.

Would it help you if OCaml had transparent ascriptions (aka (M :> S) which works like a module constraints, except all the types are exposed) ?

Alternatively we could consider allowing concrete libraries to expose their own module signature which is used when both variant and concrete libraries are linked. We just have to check for inclusion between the concrete and the virtual signatures. Unfortunately, that kind of feature would probably not work outside of dune.

[ghost]

I don't think any of this would help. Let's consider an environment in which the user can see that Regex.t = Re.t. Let's consider the set of transitive interface imports of Regex. i.e. you run ocamlobjinfo regex.cmi, recurse through the list of imports and consider the set of all seen imports. Is it possible that Re is not part of this set of transitive interface imports?

If the answer is no, then I don't believe it is possible to expose the type equality between Regex.t and Re.t without re being at least a compile time dependency of the virtual library.

[Drup]

My proposition was precisely to allow the concrete library to overwrite the virtual cmi with its own (again, at the condition that the inclusion works, which would be checked when defining the concrete library).

[ghost]

Oh, I see. But how could that work? I mean, you wouldn't be able to link together a user of the virtual library and a user of the concrete library given that they make different assumption about the interface of this module.

[Drup]

Ah, indeed, the CRCs are going to get in the way. And hacking around that, while feasible, is certainly not a good idea. We would need a more structural notion of CRCs ....

[ghost]

I suppose we could allow interfaces to expose a set of CRCs instead of just one. When compiling the cmi of the concrete implem, we would ask the compiler to check that it is an instance of the virtual one. Then the compiler would put the two CRCs in the cmi file. When something would be compiled against an interface with several CRCs, it would record the set of CRCs in its list of imports.

When two set of CRCs don't match, we would take the bigger one if one of them is included in the other, and fail otherwise. This way you could link a user of the general API and of the concrete API simultaneously, but you wouldn't be able to link two users of two different concrete APIs.

[Drup]

That's an interesting idea, although a bit hackish.

If we start modifying the compiler, I feel like there are higher level solutions that we could aim for, but I don't have concrete feasible ideas so far.

[rgrinberg]

I apologize for seeding this confusion. I believe that solutions to this problem are currently outside what is feasible in dune.