a module with multiple signatures

a module with multiple signatures

[Keiko Nakata]

Hello, 

I tried to give a module different signatures through an use of functors.
Then I faced a situation for which I do not understand the reason.

This is the simplified version of my situation.

module M = struct type s = S type t = T1 | T2 of s end

module F1 = functor (X : sig type t end) -> struct type t = X.t end

module F2 = functor (X : sig type s type t end) -> 
                 struct type s = X.s type t = X.t  end

module M1 = F1(M)

module M2 = F2(M)

let f x = match x with  M1.T1 -> 1 | M1.T2 x -> 2;;
(* This is not type checked *)
(* I got the error "Unbound constructor M1.T1" *)

(* This is type checked *)
let g (x : M1.t) = match x with  M.T1 -> 1 | M.T2 x -> 2;;

Why M1.T1 should not be bound?

Anyway,
there may be a nicer way to give a module multiple signatures
while avoiding duplicate type declarations as possible?
(In the above setting, I want to make the type s in M abstract in some 
context, but transparent in another context.)

Regards,
NAKATA Keiko

Re: [Caml-list] a module with multiple signatures

[Julien Signoles]

> module M = struct type s = S type t = T1 | T2 of s end
>
> module F1 = functor (X : sig type t end) -> struct type t = X.t end
>
> module F2 = functor (X : sig type s type t end) ->
>                  struct type s = X.s type t = X.t  end
>
> module M1 = F1(M)
>
> module M2 = F2(M)
>
> let f x = match x with  M1.T1 -> 1 | M1.T2 x -> 2;;
> (* This is not type checked *)
> (* I got the error "Unbound constructor M1.T1" *)
>
> (* This is type checked *)
> let g (x : M1.t) = match x with  M.T1 -> 1 | M.T2 x -> 2;;
>
> Why M1.T1 should not be bound?

Because only M.T1 exists, not M1.T1. You can see this on a simpler
example:

module X = struct type t = T end
module Y = struct type t = X.t end
let f x = match x with Y.T -> ()
(* type error : "Unbound constructor Y.T" *)
let f (x:Y.t) = match x with X.t -> ()
(* val f : Y.t -> unit *)

But, in ocaml, it possible to export the constructor T in Y by using the
following syntax:

module X = struct type t = T end
module Y = struct type t = X.t = T (* T is egal to X.t *) end
let f x = match x with Y.T -> ()
(* val f : Y.t -> unit *)

> Anyway,
> there may be a nicer way to give a module multiple signatures
> while avoiding duplicate type declarations as possible?

You can use signature constraints:

module M = struct type s = S type t = T1 | T2 end
module M1 : sig type t = M.t end = M
module M2 : sig type s = M.s type t = M.t end = M

Hope this helps,
Julien
-- 
mailto:Julien.Signoles@lri.fr ; http://www.lri.fr/~signoles
"In theory, practice and theory are the same,
but in practice they are different" (Larry McVoy)

Re: [Caml-list] a module with multiple signatures

[Keiko Nakata]

> Because only M.T1 exists, not M1.T1. You can see this on a simpler
> example:
> 
> module X = struct type t = T end
> module Y = struct type t = X.t end
> let f x = match x with Y.T -> ()
> (* type error : "Unbound constructor Y.T" *)
> let f (x:Y.t) = match x with X.t -> ()
> (* val f : Y.t -> unit *)
Hmmm, I see ...

> But, in ocaml, it possible to export the constructor T in Y by using the
> following syntax:
> 
> module X = struct type t = T end
> module Y = struct type t = X.t = T (* T is egal to X.t *) end
> let f x = match x with Y.T -> ()
> (* val f : Y.t -> unit *)
> You can use signature constraints:
> 
> module M = struct type s = S type t = T1 | T2 end
> module M1 : sig type t = M.t end = M
> module M2 : sig type s = M.s type t = M.t end = M

This means that if I want to export T1 and T2 then I have to write as
 module M1 : sig type t = M.t = T1 | T2 end = M
Is it correct?

In my situation, M defines many types and many type constructors,
and I want to give M different signatures, each of which will export
different sets of type constructors.
Then, it seems that I have to write the same type constructor declarations
a number of times....
Isn't it avoidable?

Best regards,
NAKATA keiko.

Re: [Caml-list] a module with multiple signatures

[Julien Signoles]

> This means that if I want to export T1 and T2 then I have to write as
>  module M1 : sig type t = M.t = T1 | T2 end = M
> Is it correct?

Yes it is. It is exactly what J.C. Filliâtre propose.

> In my situation, M defines many types and many type constructors,
> and I want to give M different signatures, each of which will export
> different sets of type constructors.
> Then, it seems that I have to write the same type constructor declarations
> a number of times....
> Isn't it avoidable?

You can use the "include" statement:

module M = struct type s = S type t = T1 | T2 end
module type S = sig type s = M.s = S end
module type T = sig type t = M.t = T1 | T2 end
module type ST = sig include S include T end
module MS : S = M
module MT : T = M
module MST : ST = M

Julien
-- 
mailto:Julien.Signoles@lri.fr ; http://www.lri.fr/~signoles
"In theory, practice and theory are the same,
but in practice they are different" (Larry McVoy)

Re: [Caml-list] a module with multiple signatures

[Jean-Christophe Filliatre]

Keiko Nakata writes:
 > 
 > I tried to give a module different signatures through an use of functors.
 > Then I faced a situation for which I do not understand the reason.
 > 
 > This is the simplified version of my situation.
 > [...]
 > Anyway,
 > there may be a nicer way to give a module multiple signatures
 > while avoiding duplicate type declarations as possible?
 > (In the above setting, I want to make the type s in M abstract in some 
 > context, but transparent in another context.)

I think you can proceed as follows:

  module M = struct type s type t = A | B end
  module M1 : sig type t = M.t = A | B end = M
  module M2 : ... = M

i.e. you cannot put only "t = M.t" in the signature of M1, you need to
add "=  A|B". This is called  a "re-exported variant  type" in Ocaml's
manual (see http://caml.inria.fr/pub/docs/manual-ocaml/manual018.html)

-- 
Jean-Christophe