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

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

[Sylvain Le Gall]

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:

(** All the plugins I want to manage *)
type plugin_kind = [`Build | `Install]

(** Generic plugin *)
type 'a plugin = 'a * string

(** Help data for all plugin *)
module MapPlugin = 
  Map.Make
    (struct
       type t = plugin_kind plugin
       let compare = compare
     end)

let all_help: string MapPlugin.t ref = 
  ref MapPlugin.empty

let help plg = 
  MapPlugin.find plg !all_help

(** Functor to build function related to one type of plugin *)
module type PLUGIN_FAMILY = 
sig
  type act
  type kind
  val kind_default: kind
end


module Make (F: PLUGIN_FAMILY) = 
struct

  module MapPluginSelf = 
    Map.Make
      (struct 
         type t = F.kind plugin
         let compare = compare
       end)

  let all_act: F.act MapPluginSelf.t ref = 
    ref MapPluginSelf.empty

  let act (plg : F.kind plugin) =
    MapPluginSelf.find plg !all_act

  let create name help act = 
    let id = 
      F.kind_default, name
    in
      all_help := MapPlugin.add id help !all_help;
      all_act  := MapPlugin.add id act !all_act;
      id
end

(** Functions for build plugins *)
module Build =
  Make
    (struct 
       type act = unit -> unit 
       type kind = [`Build]
       let default = `Build
     end)

(** Functions for install plugins *)
module Install = 
  Make
    (struct 
       type act = string list -> unit
       type kind = [`Install]
       let default = `Install
     end)

type package = 
    {
      name: string;
      plugin_build: [`Build] plugin;
      plugin_install: [`Install] plugin;
    }

let run pkg = 
  prerr_endline (help pkg.plugin_build);
  prerr_endline (help pkg.plugin_install);
  (Build.act pkg.plugin_build) ();
  (Install.act pkg.plugin_install) ()


This code doesn't compile because I see no way to explain that F.kind is
included into plugin_kind. 

Here is the precise error:
camlc -o test test.ml
File "test.ml", line 51, characters 32-34:
Error: This expression has type F.kind * 'a
       but an expression was expected of type
         MapPlugin.key = plugin_kind * string
       Type F.kind is not compatible with type
         plugin_kind = [ `Build | `Install ] 
make: *** [all] Erreur 2

Does anyone know a good solution to this problem? Does anyone have a
better solution to this problem? (different design?)

Thank you for your answers,
Sylvain Le Gall

Re: [Caml-list] Type constraint to explain that a polymorphic variants is included into another

[Jake Donham]

On Fri, Oct 8, 2010 at 10:13 AM, Sylvain Le Gall <sylvain@le-gall.net> wrote:
> This code doesn't compile because I see no way to explain that F.kind is
> included into plugin_kind.

As you have written it, F.kind is of course completely abstract. I am
not sure where you need F.kind to be a strict subtype of plugin_kind,
but you could say type kind = plugin_kind (this seems a bit useless
however).

I don't think there is a way to use subtyping implicitly when applying
a functor, but you can always do it explicitly by interposing a module
of signature PLUGIN_FAMILY which embeds the specific kind in
plugin_kind and passes the other components through.

You could also have a general and a specific type in the plugin
signature, and use the general one for general operations (e.g. help)
but the specific one wherever that is needed. I am not sure I
understand what you're trying to achieve however.

Jake

Re: [Caml-list] Type constraint to explain that a polymorphic variants is included into another

[Jacques Garrigue]

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.

Here is a typable version of your code.
Note that I had to do a few other changes to make the types match.

Jacques

(** All the plugins I want to manage *)
type plugin_kind = [`Build | `Install]

(** Generic plugin *)
type 'a plugin = 'a * string

(** Help data for all plugin *)
module MapPlugin = 
 Map.Make
   (struct
      type t = plugin_kind plugin
      let compare = compare
    end)

let all_help: string MapPlugin.t ref = 
 ref MapPlugin.empty

let help plg = 
 MapPlugin.find plg !all_help

(** Functor to build function related to one type of plugin *)
module type PLUGIN_FAMILY = 
sig
 type act
 type kind = private [< plugin_kind]
 val kind_default: kind
end


module Make (F: PLUGIN_FAMILY) = 
struct

 module MapPluginSelf = 
   Map.Make
     (struct 
        type t = F.kind plugin
        let compare = compare
      end)

 let all_act: F.act MapPluginSelf.t ref = 
   ref MapPluginSelf.empty

 let act (plg : F.kind plugin) =
   MapPluginSelf.find plg !all_act

 let create name help act = 
   let id = 
     F.kind_default, name
   in
     all_help := MapPlugin.add (id :> plugin_kind * _) help !all_help;
     all_act  := MapPluginSelf.add id act !all_act;
     id
end

(** Functions for build plugins *)
module Build =
 Make
   (struct 
      type act = unit -> unit 
      type kind = [`Build]
      let kind_default = `Build
    end)

(** Functions for install plugins *)
module Install = 
 Make
   (struct 
      type act = string list -> unit
      type kind = [`Install]
      let kind_default = `Install
    end)

type package = 
   {
     name: string;
     plugin_build: [`Build] plugin;
     plugin_install: [`Install] plugin;
   }

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 []

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

[Sylvain Le Gall]

On 08-10-2010, Jake Donham <jake@donham.org> wrote:
> On Fri, Oct 8, 2010 at 10:13 AM, Sylvain Le Gall <sylvain@le-gall.net> wrote:
>> This code doesn't compile because I see no way to explain that F.kind is
>> included into plugin_kind.
>
> As you have written it, F.kind is of course completely abstract. I am
> not sure where you need F.kind to be a strict subtype of plugin_kind,
> but you could say type kind = plugin_kind (this seems a bit useless
> however).
>
> I don't think there is a way to use subtyping implicitly when applying
> a functor, but you can always do it explicitly by interposing a module
> of signature PLUGIN_FAMILY which embeds the specific kind in
> plugin_kind and passes the other components through.
>
> You could also have a general and a specific type in the plugin
> signature, and use the general one for general operations (e.g. help)
> but the specific one wherever that is needed. I am not sure I
> understand what you're trying to achieve however.
>

My goal is that the compiler prevents me to do 
Build.act pkg.plugin_install 
-> because plugin_install is of type [`Install] plugin and Build.act
   needs [`Build] plugin

but allow me to do 

help pkg.plugin_install 
-> because help needs [`Build | `Install] plugin.

But maybe I am missing something here and try to overengineer something
simple.

Regards,
Sylvain Le Gall

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

[Sylvain Le Gall]

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