Re: [Caml-list] Signature substitution and type parameters

["Raphaël Proust" <raphlalou@gmail.com>]

Unsuccessful attempts with functors and type constraints:

# module Monomorphise (P: Poly) (T: sig type t end) = struct
  type 'a t = T.t constraint 'a = int
  Interrupted.
# module Monomorphise (P: Poly) (T: sig type t end) = struct
  type 'a t constraint 'a = T.t
  include (P : Poly with type 'a t := 'a t constraint 'a = T.t)
  end ;;
Syntax error: ')' expected, the highlighted '(' might be unmatched
# module Monomorphise (P: Poly) (T: sig type t end) = struct
  type 'a t constraint 'a = T.t
  include (P : Poly with type 'a t := 'a t)
  end ;;
Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match:
         type 'a t = 'a t constraint 'a = T.t
       is not included in
         type 'a t
       Their constraints differ.




On Mon, Aug 12, 2013 at 8:45 AM, Gabriel Kerneis <gabriel@kerneis.info> wrote:
> Dear all,
>
> Is there a concise way to instanciate a module containing a parametric
> type for a particular value of this type parameter?
>
>   module type Poly = sig type 'a t val f : 'a t -> 'a t end ;;
>   module type Mono = sig type t val f : t -> t end ;;
>
>   module PolyM : Poly = struct type 'a t let f x = x end ;;
>
> The following works but is tedious when Poly contains many functions
> instead of only one:
>
>   module MonoM : Mono = struct
>     open PolyM
>     type t = int PolyM.t
>     let f = PolyM.f
>   end ;;
>
> My other attempts so far:
>
>   # module MonoM : (Mono with type t := int PolyM.t) = PolyM ;;
>   Error: Only type constructors with identical parameters can be
>   substituted.
>
>   # module MonoM : (Mono with type t = int PolyM.t) = PolyM ;;
>   Error: Signature mismatch:
>     Modules do not match:
>       sig type 'a t = 'a PolyM.t val f : 'a t -> 'a t end
>     is not included in
>       sig type t = int PolyM.t val f : t -> t end
>     Type declarations do not match:
>       type 'a t = 'a PolyM.t
>     is not included in
>       type t = int PolyM.t
>     They have different arities.
>
> Is this a fundamental limitation of the typechecker, which would
> otherwise lead to unsafe behaviour?
>
>   Note: The initial motivation for doing this was to use Jean-Christophe
>   Filliātre's Hset as a drop-in replacement for OCaml's Set in one of my
>   programs, without having to add type parameters all over the place.
>   https://www.lri.fr/~filliatr/ftp/ocaml/ds/hset.mli.html
>
> Kind regards,
> --
> Gabriel
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs



-- 
______________
Raphaël Proust