[Caml-list] Strange behavior from type inference after functor application

[Caml-list] Strange behavior from type inference after functor application

[rixed]

Given these definitions:

-- v1 --

module type TYPE = sig type t end

module Combi (S1 : TYPE) (S2 : TYPE) :
    TYPE with type t = S1.t * S2.t =
struct
    type t = S1.t * S2.t
end

module TypeWithConf (Conf : sig val v : int end) :
	TYPE =
struct
    type t = unit
end

module S = struct type t = unit end

module C = Combi (S) (TypeWithConf (struct let v = 1 end))

let f (x : C.t) = fst x

-----

Here, the compiler fails to infer that C.t is indeed the product of two types
(as stated in the Combi signature), and complains that:

Error: This expression has type C.t but an expression was expected of type 'a * 'b
(pointing at the argument of fst)

There is two ways to satisfies it:

- either, state that the type of TypeWithConf is 'TYPE with type t = unit'
  instead of merely 'TYPE'

- or, more surprisingly, to define the Conf structure as in:

-- v2 --
(* ... *)

module Conf = struct let v = 1 end
module C = Combi (S) (TypeWithConf (Conf))

(* ... *)
-----

Can someone help me find an explanation to this behavior?

Re: [Caml-list] Strange behavior from type inference after functor application

[Gabriel Scherer]

The problem with
  module C = Combi (S) (TypeWithConf (struct let v = 1 end))
is that the resulting type has no "name": (struct let v = 1 end) can
not be part of a type path.

On the contrary, TypeWithConf(Conf) has a type t with name
TypeWithConf(Conf).t, so C.t can be equal to S.t *
TypeWithConf(Conf).t. There would be no such type as S.t *
TypeWIthConf(struct let v = 1 end).t.

The other fix, forcing TypeWithConf to return a signature with (t =
unit), makes the "naming problem" go away: whatever functor you pass
as a parameter (either a path such as "Conf" or a struct exrpession),
the resulting type is equal to "unit", you don't have to try to name
it from the way it was constructed.

On Thu, May 31, 2012 at 10:05 PM,  <rixed@happyleptic.org> wrote:
> Given these definitions:
>
> -- v1 --
>
> module type TYPE = sig type t end
>
> module Combi (S1 : TYPE) (S2 : TYPE) :
>    TYPE with type t = S1.t * S2.t =
> struct
>    type t = S1.t * S2.t
> end
>
> module TypeWithConf (Conf : sig val v : int end) :
>        TYPE =
> struct
>    type t = unit
> end
>
> module S = struct type t = unit end
>
> module C = Combi (S) (TypeWithConf (struct let v = 1 end))
>
> let f (x : C.t) = fst x
>
> -----
>
> Here, the compiler fails to infer that C.t is indeed the product of two types
> (as stated in the Combi signature), and complains that:
>
> Error: This expression has type C.t but an expression was expected of type 'a * 'b
> (pointing at the argument of fst)
>
> There is two ways to satisfies it:
>
> - either, state that the type of TypeWithConf is 'TYPE with type t = unit'
>  instead of merely 'TYPE'
>
> - or, more surprisingly, to define the Conf structure as in:
>
> -- v2 --
> (* ... *)
>
> module Conf = struct let v = 1 end
> module C = Combi (S) (TypeWithConf (Conf))
>
> (* ... *)
> -----
>
> Can someone help me find an explanation to this behavior?
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Strange behavior from type inference after functor application

[rixed]

-[ Thu, May 31, 2012 at 10:23:13PM +0200, Gabriel Scherer ]----
> The problem with
>   module C = Combi (S) (TypeWithConf (struct let v = 1 end))
> is that the resulting type has no "name": (struct let v = 1 end) can
> not be part of a type path.

So in order for the compiler to infer a type the type must have a 'name'?
That's funny because this 'name' is not used anywhere. Couldn't just
such anonymous modules be given random names so that everything works as
long as these names are unused? I mean, in the given example no type of
this Conf module was required to infer that C.t is a product type (which
was everything needed since f was returning the first value).

Or would it be just too obscure and not useful enough?

Anyway, thank you for the explanation. Hopefully I will remember it for
the next encounter.

Re: [Caml-list] Strange behavior from type inference after functor application

[Andreas Rossberg]

On May 31, 2012, at 23.22 h, rixed@happyleptic.org wrote:
> -[ Thu, May 31, 2012 at 10:23:13PM +0200, Gabriel Scherer ]----
>> The problem with
>>  module C = Combi (S) (TypeWithConf (struct let v = 1 end))
>> is that the resulting type has no "name": (struct let v = 1 end) can
>> not be part of a type path.
>
> So in order for the compiler to infer a type the type must have a  
> 'name'?
> That's funny because this 'name' is not used anywhere. Couldn't just
> such anonymous modules be given random names so that everything  
> works as
> long as these names are unused? I mean, in the given example no type  
> of
> this Conf module was required to infer that C.t is a product type  
> (which
> was everything needed since f was returning the first value).
>
> Or would it be just too obscure and not useful enough?

The compiler has to give a module type to the module C, and the OCaml  
type system insists that any module type it computes is expressible by  
a syntactically valid signature. So it has to find one that avoids  
mentioning S2.t. The only way to do so in a syntactically valid manner  
is to make t abstract altogether in the resulting signature.

This is known as the "avoidance problem" in literature on ML modules.  
The only solution to avoid the avoidance problem is to not insist on  
syntactic signatures during type checking, which is essentially what  
you suggest (although it's a bit more complicated in general). Other  
dialects of ML modules indeed work like that, but it would be quite a  
fundamental change to the way module type checking is done in OCaml.

/Andreas