[Caml-list] Signature substitution and type parameters

[Caml-list] Signature substitution and type parameters

[Gabriel Kerneis]

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

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

[Raphaël Proust]

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

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

[Jeremy Yallop]

On 12 August 2013 08:45, Gabriel Kerneis <gabriel@kerneis.info> wrote:
> 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 ;;

If you use 'include' instead of 'let' it generalizes nicely to the
many-function case:

  module MonoM : Mono = struct
    type t = int PolyM.t
    include (PolyM : Mono with type t := t)
  end

A slight variation makes it possible to achieve a similar effect
without using the Mono signature:

  type _ s = int PolyM.t
  module MonoM = struct
    type t = unit s
    include (PolyM : Poly with type 'a t := 'a s)
  end

Your other approach can be made to work, too.  The key is to define a
type alias with no parameters (type t = int PolyM.t), then use
destructive substitution (:=).

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

[Gabriel Kerneis]

On Mon, Aug 12, 2013 at 11:20:17AM +0100, Jeremy Yallop wrote:
> If you use 'include' instead of 'let' it generalizes nicely to the
> many-function case:
> 
>   module MonoM : Mono = struct
>     type t = int PolyM.t
>     include (PolyM : Mono with type t := t)
>   end

Ha! I tried it written as "include PolyM with ...", which is
invalid syntax, and didn't get any further. Thanks Jeremy. 

> Your other approach can be made to work, too.  The key is to define a
> type alias with no parameters (type t = int PolyM.t), then use
> destructive substitution (:=).

By the way, there is an unanswered question from June by Markus Mottl
about the root causes of this limitation:

  https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00147.html

Maybe you can shed some light on it?

Best regards,
-- 
Gabriel