Implicitely abstracted type

Implicitely abstracted type

[Louis Gesbert]

Yesterday I encountered an ocaml error that, if I can now make some 
sense out of it -- it's not properly speaking a bug -- was quite 
confusing at first and took me  some time to figure out.

What happens is that a sum-type defined in a module can implicitely be 
turned into abstract because of its inner contents.

Here is a small example:
------
module F (A : sig type a end) = struct
  type a = A.a
  type t = X of A.a
end

(* if A.a is abstract, the type F.t is made abstract *)
module A = F (struct type a end)
(*
  The inferred interface is:
  module A : sig type a type t end

  I figure ocaml can't guess what to put in the interface for the 
definition of t,
  but maybe an error would be better than silently turning it into 
abstract ?
*)

(* it gets confusing in the following use case (and of course if type t
   has many cases and you just added an abstract type somewhere deep) *)
let _ = A.X (assert false)
  (* the constructor A.X is not found *)

(* if t is defined as "X of a" instead of "X of A.a", no problem arises *)
------

I don't know exactly what to do with it, but maybe it should be made an 
error ? (types escaping their scope usually are)

Louis

-- 
Louis Gesbert
R & D @ MLstate
15, rue Berlier
75013 Paris

Re: [Caml-list] Implicitely abstracted type

[rossberg]

> Yesterday I encountered an ocaml error that, if I can now make some
> sense out of it -- it's not properly speaking a bug -- was quite
> confusing at first and took me  some time to figure out.
>
> What happens is that a sum-type defined in a module can implicitely be
> turned into abstract because of its inner contents.
>
> Here is a small example:
> ------
> module F (A : sig type a end) = struct
>   type a = A.a
>   type t = X of A.a
> end
>
> (* if A.a is abstract, the type F.t is made abstract *)
> module A = F (struct type a end)
> (*
>   The inferred interface is:
>   module A : sig type a type t end

That is a well-known limitation. The fix is to name the argument module:

  module TA = struct type a end
  module A = F (TA)

/Andreas

Re: [Caml-list] Implicitely abstracted type

[Alain Frisch]

On 12/16/2010 02:31 PM, Louis Gesbert wrote:
> What happens is that a sum-type defined in a module can implicitely be
> turned into abstract because of its inner contents.

Here is an explanation of this behavior. When applying a functor of type 
functor(X:S1) -> S2 to a module of type T, the module type for the 
result can be obtained in two different ways:

(1) T is a path: the module type is obtained by substituting X with T in S2.

(2) T is not a path: the module type is obtained by computing the 
smallest supertype of S2 that doesn't contain X anymore (under the extra 
assumption that X has type T).


In your example, you are in case (2), and the only way (of which the 
compiler is aware) to get rid of the dependency on the functor's formal 
argument is to turn a concrete type declaration into an abstract one. If 
you are interested in the implementation, this happens in the function 
Ctype.nondep_type_decl (where a Not_found exception raised by 
nondep_type_rec is turned into a Type_abstract).

Admittedly, this fallback behavior of turning automatically a concrete 
type declaration into an abstract one is not completely natural. As far 
as I can tell, it would be straightforward to add a warning in this 
situation.  Do you want to fill a feature request?


Alain

Re: [Caml-list] Implicitely abstracted type

[rossberg]

Alain Frisch wrote:
>
> When applying a functor of type
> functor(X:S1) -> S2 to a module of type T, the module type for the
> result can be obtained in two different ways:
>
> (1) T is a path: the module type is obtained by substituting X with T in S2.
>
> (2) T is not a path: the module type is obtained by computing the
> smallest supertype of S2 that doesn't contain X anymore (under the extra
> assumption that X has type T).

I believe this doesn't type-check. :) You probably meant to say:

"When applying a functor of type
functor(X:S1) -> S2 to a module M of type T, the module type for the
result can be obtained in two different ways:

(1) M is a path: the module type is obtained by substituting X with M in S2.

(2) M is not a path: the module type is obtained by computing the
smallest supertype of S2 that doesn't contain X anymore (under the extra
assumption that X has type T)."

/Andreas