question on type checking

question on type checking

[Stephen Weeks]

Why does one of the programs below fail to type check while the other two minor
variants succeed?  I would expect all three to succeed.

----------------------------------------------------------------------
(* FAILS *)
module F (Z : sig end) = struct
  type t = A
end

module S = struct
  module Z = struct end
  module M = F (Z)
  include M
end

let f x =
  let module S = S in
  match x with
  | S.A -> ()
----------------------------------------------------------------------
(* WORKS *)
module F (Z : sig end) = struct
  type t = A
end

module S = struct
  module M = F (struct end)
  include M
end

let f x =
  let module S = S in
  match x with
  | S.A -> ()
----------------------------------------------------------------------
(* WORKS *)
module F (Z : sig end) = struct
  type t = A
end

module S = struct
  module Z = struct end
  module M = F (Z)
  include M
end

let f x =
  match x with
  | S.A -> ()
----------------------------------------------------------------------

Re: [Caml-list] question on type checking

[Derek Dreyer]

This appears to be a bug in the typechecker.  Perhaps a more obvious
instance of the problem is if, after the (top-level) definition of S
in your first example you write:

module T = S
let x = if true then T.A else S.A

This clearly should typecheck, but instead you get the error message:

> This expression has type S.t = F(S.Z).t but is here used with type
>   T.t = F(T.Z).t

Huh?  You mean S.t does not equal T.t when I just defined T = S?

The problem is precisely that the typechecker is not properly
selfifying (strengthening) the signature of S in processing "module T
= S".  When properly selfified, the signature of S (and thus also T)
should be

sig
  module Z : sig end
  module M : sig type t = F(S.Z) = A end
  type t = F(S.Z) = A end
end

but instead of F(S.Z), it's just doing F(Z).  This wouldn't be an
issue if the language tracked structure identities across renamings
(since S.Z and T.Z are clearly the same structure), but it doesn't.

In your second example, this bug didn't pop up because Z was not
named, so M.t could not be characterized precisely through an
applicative functor type of the form F(<something>).t.

In your third example, this bug didn't pop up because you didn't
rename the structure S (and hence tickle the signature strengthening
bug).

I'm guessing this bug should be easy to fix.

Derek

On 3/20/07, Stephen Weeks <sweeks@sweeks.com> wrote:
> Why does one of the programs below fail to type check while the other two minor
> variants succeed?  I would expect all three to succeed.
>
> ----------------------------------------------------------------------
> (* FAILS *)
> module F (Z : sig end) = struct
>  type t = A
> end
>
> module S = struct
>  module Z = struct end
>  module M = F (Z)
>  include M
> end
>
> let f x =
>  let module S = S in
>  match x with
>  | S.A -> ()
> ----------------------------------------------------------------------
> (* WORKS *)
> module F (Z : sig end) = struct
>  type t = A
> end
>
> module S = struct
>  module M = F (struct end)
>  include M
> end
>
> let f x =
>  let module S = S in
>  match x with
>  | S.A -> ()
> ----------------------------------------------------------------------
> (* WORKS *)
> module F (Z : sig end) = struct
>  type t = A
> end
>
> module S = struct
>  module Z = struct end
>  module M = F (Z)
>  include M
> end
>
> let f x =
>  match x with
>  | S.A -> ()
> ----------------------------------------------------------------------
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] question on type checking

[Stephen Weeks]

Thanks for the reply Derek.  I also thought it looked like a bug, and
your explanation makes sense.  However, Markus Mottl pointed me to the
following  issue in the bug tracker

  http://caml.inria.fr/mantis/view.php?id=3476

The problem there looks very similar, and would seem to indicate that
the situation is not viewed as a bug (in the sense that it won't be
fixed).

Re: [Caml-list] question on type checking

[Derek Dreyer]

Very interesting.  So now, looking back at Xavier's POPL'95 paper on
applicative functors, I see what he means by saying it's a fundamental
problem with how applicative functors work in OCaml.  I.e. it's not
just a bug in the typechecker, but in the type system in the original
paper.  In particular, the definition of signature strengthening on
page 7 of that paper includes the following case:

(module x_i : M; S)/p =
    module x_i : (M/p.x); S/p

But I believe this is a mistake, and instead of S/p it should be
  (S{x_i <- p.x})/p

In other words, first replace references to x_i (esp. in functor
applications in types) inside S with references to p.x, and then
proceed with selfification as usual.  Is there some reason this would
not work or would be difficult to implement?

I believe this would eliminate the bugs we're looking at here.  And
I'm sort of surprised that this would be hard to do, but I'm not
familiar with the implementation.

Derek

On 3/21/07, Stephen Weeks <sweeks@sweeks.com> wrote:
> Thanks for the reply Derek.  I also thought it looked like a bug, and
> your explanation makes sense.  However, Markus Mottl pointed me to the
> following  issue in the bug tracker
>
>  http://caml.inria.fr/mantis/view.php?id=3476
>
> The problem there looks very similar, and would seem to indicate that
> the situation is not viewed as a bug (in the sense that it won't be
> fixed).
>

Re: [Caml-list] question on type checking

[Xavier Leroy]

> Very interesting.  So now, looking back at Xavier's POPL'95 paper on
> applicative functors, I see what he means by saying it's a fundamental
> problem with how applicative functors work in OCaml.  I.e. it's not
> just a bug in the typechecker, but in the type system in the original
> paper.  In particular, the definition of signature strengthening on
> page 7 of that paper includes the following case:
>
> (module x_i : M; S)/p =
>    module x_i : (M/p.x); S/p
>
> But I believe this is a mistake, and instead of S/p it should be
>  (S{x_i <- p.x})/p

Thanks for this very interesting suggestion.

As Derek knows, there are two deep limitations in the syntactic
type system for modules used in OCaml, namely

1) at most one type equality can be recorded per type declaration, and
2) structure equality is not tracked, therefore the types F(M).t and F(N).t
   (assuming t is abstract in F's result signature) are distinct even if
   N is an alias for M.

I managed to convince myself that the problems with applicative functors
discussed e.g. in PR#3476 cannot be solved without lifting one of
these limitations, which is something I don't know how to do (neither
theoretically nor implementation-wise).

Derek's suggestion seems to prove me wrong.  The two definitions of
signature strengthening (the one in my papers, used in OCaml, and
Derek's proposal) appear to have the same expressive power in a system
with generative functors, but Derek's definition is definitely
stronger in conjunction with applicative functors.

> In other words, first replace references to x_i (esp. in functor
> applications in types) inside S with references to p.x, and then
> proceed with selfification as usual.  Is there some reason this would
> not work or would be difficult to implement?

Difficult to implement: I don't think so.  Would not work: some formal
soundness argument would be nice of course :-), but there is a
strong intuition that at the point of the ";" in the equation above,
the two paths "x_i" and "p.x" carry the same amount of typing information,
so replacing the latter by the former appears sound.

Best wishes,

- Xavier