Re: Type constraint to explain that a polymorphic variants is included into another

[Sylvain Le Gall <sylvain@le-gall.net>]

Hello,

On 08-10-2010, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
> On 2010/10/09, at 2:13, Sylvain Le Gall wrote:
>
>> Hello all,
>> 
>> I would like to build an interface for plugins that allow to extract at the
>> same time a very specific data for a plugin family and to extract
>> general help for plugins.
>> 
>> Here is an example:
>
> [...]
>
>> This code doesn't compile because I see no way to explain that F.kind is
>> included into plugin_kind. 
>
> I'm not sure of what you are trying to do, but private rows where introduced
> with this goal in mind.
>
> The idea is to change the abstract definition of kind in PLUGIN_FAMILY to
>
>   type kind = private [< plugin_kind]
>
> meaning that kind can be instantiated to any subset of plugin_kind.
> You can then use subtyping to convert from kind to plugin_kind.
>

Very nice OCaml extension. It indeed solves my problem. I was aware of private
type, but don't yet know how to use it.

> Here is a typable version of your code.
>
> let run pkg = 
>  prerr_endline (help (pkg.plugin_build :> MapPlugin.key));
>  prerr_endline (help (pkg.plugin_install :> MapPlugin.key));
>  (Build.act pkg.plugin_build) ();
>  Install.act pkg.plugin_install []
>

That is perfect. If I add the following call, with your solution:

 (Install.act pkg.plugin_build) []

I get this error:

ocamlc -o test test.ml
File "test.ml", line 84, characters 14-30:
Error: This expression has type [ `Build ] plugin = [ `Build ] * string
       but an expression was expected of type
         [ `Install ] plugin = [ `Install ] * string
       These two variant types have no intersection
make: *** [all] Erreur 2

This is exactly what I want.

Thanks,
Sylvain Le Gall