Variance problem in higher-order Functors?

Variance problem in higher-order Functors?

[Jacques Carette]

I seem to have encountered a problem in type-checking of higher-order 
functors with type constraints -- it seems to me that the containment 
check is backwards.  Below I include complete code (between ======= 
makers).  This was tried in ocaml 3.09.01

Basically, I use singleton types to encode presence/absence of a 
semantic property.  I use type constraints to ensure that the functor 
cannot be applied if the constraint is not satisfied.  If I write 
everything "simply", it all works.  If I go higher-order, it fails.  
Below is what I can distill from a much much larger program and still 
show the issue.
=============
(* this works *)
module type DOMAIN = sig
    type kind
    type foo
    val  upd : foo -> foo
end

type domain_is_field

module Rational = struct
    type kind = domain_is_field
    type foo  = int * int
    let  upd (x,y) = (x-1, y+1)
end

module Integer = struct
    type kind
    type foo  = int
    let  upd x = x-1
end

module type UPDATE = sig
    type obj
    val update : obj -> obj
end

module DivisionUpdate(D:DOMAIN with type kind = domain_is_field) = struct
    type obj = D.foo
    let update a = D.upd a
end

(* this one is semantically incorrect! *)
module BadUpdate(D:DOMAIN) = struct
    type obj = D.foo
    let update a = D.upd a
end

(* works, as expected *)
module A = DivisionUpdate(Rational)
(* _correctly_ generates an error
module A = DivisionUpdate(Integer)
*)

(* However, if we go higher order: *)
module type UPDATE2 =
    functor(D:DOMAIN) -> sig
    type obj = D.foo
    val update : obj -> obj
end

(* this is the same as the "updates" above, just wrapped in a module *)
module Bar(D:DOMAIN)(U:UPDATE2) = struct
    module U = U(D)
    let update x = U.update x
end

(* works as there are no restrictions *)
module T3 = Bar(Integer)(BadUpdate) ;;

(* and now this does not work?!?! even though it should!*)
module T2 = Bar(Rational)(DivisionUpdate) ;;

============
The error I get on this very last line is
Signature mismatch:
Modules do not match:
  functor
    (D : sig type kind = domain_is_field type foo val upd : foo -> foo 
end) ->
    sig type obj = D.foo val update : D.foo -> D.foo end
is not included in
  UPDATE2
Modules do not match:
  DOMAIN
is not included in
  sig type kind = domain_is_field type foo val upd : foo -> foo end
Type declarations do not match:
  type kind
is not included in
  type kind = domain_is_field

and this last check seems to be looking at signature inclusion 
*backwards*, especially since it works if you do the same at the 'top 
level' instead of passing things in through a functor.

Or I am making a mistake somewhere above?

Jacques

Re: [Caml-list] Variance problem in higher-order Functors?

[Andreas Rossberg]

"Jacques Carette" <carette@mcmaster.ca> wrote:
> I seem to have encountered a problem in type-checking of higher-order
> functors with type constraints -- it seems to me that the containment
> check is backwards.

Well, yes. That's contravariance.

> (* this works *)
> module type DOMAIN = sig
>     type kind
>     type foo
>     val  upd : foo -> foo
> end
>
> type domain_is_field
>
> module Rational = struct
>     type kind = domain_is_field
>     type foo  = int * int
>     let  upd (x,y) = (x-1, y+1)
> end
>
> module Integer = struct
>     type kind
>     type foo  = int
>     let  upd x = x-1
> end
>
> module type UPDATE = sig
>     type obj
>     val update : obj -> obj
> end
>
> module DivisionUpdate(D:DOMAIN with type kind = domain_is_field) = struct
>     type obj = D.foo
>     let update a = D.upd a
> end
>
> (* this one is semantically incorrect! *)
> module BadUpdate(D:DOMAIN) = struct
>     type obj = D.foo
>     let update a = D.upd a
> end
>
> (* works, as expected *)
> module A = DivisionUpdate(Rational)
> (* _correctly_ generates an error
> module A = DivisionUpdate(Integer)
> *)
>
> (* However, if we go higher order: *)
> module type UPDATE2 =
>     functor(D:DOMAIN) -> sig
>     type obj = D.foo
>     val update : obj -> obj
> end
>
> (* this is the same as the "updates" above, just wrapped in a module *)
> module Bar(D:DOMAIN)(U:UPDATE2) = struct
>     module U = U(D)
>     let update x = U.update x
> end
>
> (* works as there are no restrictions *)
> module T3 = Bar(Integer)(BadUpdate) ;;
>
> (* and now this does not work?!?! even though it should!*)
> module T2 = Bar(Rational)(DivisionUpdate) ;;

No, it should not work. Bar(Rational) has the signature

  functor(U: functor(D:DOMAIN)->S1) -> S2

i.e. argument signature

  functor(D:DOMAIN)->S1

but you are trying to apply it to module DivisionUpdate, which has signature

  functor(D:DOMAIN')->S1

where DOMAIN'=(DOMAIN with type kind = domain_is_field). This is a
*sub*signature of DOMAIN! Since functors are necessarily contravariant in
their argument, however, it had to be a *super*signature of DOMAIN instead
to allow passing the functor to Bar.

That is, the problem with your example boils down to this:

  module type DOMAIN = sig type kind end
  module type DOMAIN' = sig type kind = unit end

  module Bar (U : functor(D : DOMAIN) -> sig end) = struct end
  module Up (D : DOMAIN') = struct end

  module T = Bar(Up)

-->

  Signature mismatch:
  Modules do not match:
    functor (D : DOMAIN') -> sig  end
  is not included in
    functor (D : DOMAIN) -> sig  end
  Modules do not match: DOMAIN is not included in DOMAIN'
  Type declarations do not match: type t is not included in type kind = unit

- Andreas

How do I achiece this, was Re: [Caml-list] Variance problem in higher-order Functors?

[Jacques Carette]

My real question is (and should have been), how do I translate

module type DOMAIN = sig type kind end
type domain_is_field
type domain_is_ring
module Rational = struct type kind = domain_is_field end
module Integer = struct type kind = domain_is_ring end

module DivisionUpdate(D:DOMAIN with type kind = domain_is_field) = struct
  (* something only valid with D a field*)
end

module GeneralUpdate(D:DOMAIN) = struct
   (* something that always works, for rings and fields *)
end

The behaviour I want should be the same as the first-order applications
module A = DivisionUpdate(Rational)  (* OK *)
module B = GeneralUpdate(Rational)  (* OK *)
module C = DivisionUpdate(Integer)  (* ERROR *)
module D = GeneralUpdate(Integer)  (* OK *)
BUT I want to pass all these modules as parameters to a functor.  I 
don't see how to build the proper type that will work!
[I have read the manuals in depth, Googled around the caml.inria.fr web 
site, played around with the implementation, etc to no avail]

In other words, I want to be able to define
module type Trans = functor(U:UPDATE) ->  functor(D:DOMAIN) -> sig ... end
but none of my attempts have worked, even though the first-order code 
works fine.

I would be happy with a solution that uses polymorphic variants, or 
objects, or whatever work.  The only thing I can't do is "run-time" 
tests, as I have a dozen domains, with more functors and more 
constraints floating around, so I really want this to be a type-level 
solution.  If OCaml had conditional module application, I could use 
that, but "expanding" my definitions is not realistic.

Jacques

Re: How do I achiece this, was Re: [Caml-list] Variance problem in higher-order Functors?

[Jacques Garrigue]

From: Jacques Carette <carette@mcmaster.ca>

> In other words, I want to be able to define
> module type Trans = functor(U:UPDATE) ->  functor(D:DOMAIN) -> sig ... end
> but none of my attempts have worked, even though the first-order code 

I think I have a solution, at least to your first post.
If I am right, what you need is to express that Bar's 2nd parameter
is a functor with input of type "DOMAIN with type kind = D.kind".
But you cannot use "with", because the functor type is defined as an
abrreviation. The trick is to wrap the module type definition in a
functor, and to use applicative types.

(* If we go higher order: *)
module UPDATE2(D0:DOMAIN) = struct
  module type S =
    functor(D:DOMAIN with type kind = D0.kind) -> sig
      type obj = D.foo
      val update : obj -> obj
    end
end

(* this is the same as the "updates" above, just wrapped in a module *)
module Bar(D:DOMAIN)(U:UPDATE2(D).S) = struct
    module U = U(D)
    let update x = U.update x
end

(* works as there are no restrictions *)
module T3 = Bar(Integer)(BadUpdate) ;;

(* and now this works! *)
module T2 = Bar(Rational)(DivisionUpdate) ;;

This trick of wrapping module types inside functors proves useful in
many situations, when you want to express sharing that cannot be
expressed by with alone.

Jacques Garrigue