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

Variance problem in higher-order Functors?

[oleg]

Jacques Carette posed the problem: given

> 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

how to write a functor of the type
> module type Trans = functor(U:UPDATE) ->  functor(D:DOMAIN) -> sig
> ... end

so that we can instantiate it with DivisionUpdate and Rational,
GeneralUpdate and Rational, GeneralUpdate and Integer but not
DivisionUpdate and Integer.

The second argument of the functor has the signature DOMAIN -- as it
should so we can accept both Rational and Integer as
structures. However, that means that the formal parameter D has type
that abstracts over `domain_is_field' and `domain_is_ring' -- thus
removing the very distinction we need to typecheck the application of
UPDATE.

There seem to be three solutions, the last of which precisely
implements the signature of Trans. 

The first solution avoids higher-order functors altogether. That is,
rather than instantiating Trans with an UPDATE structure and then with
a DOMAIN structure, we instantiate it with a DUPDATE structure (which
has a DOMAIN structure as one of the components). The end result is
essentially the same. That DUPDATE structure can only be produced in
certain ways (e.g., by DivisionUpdate functor), which will make sure
that the concrete domain is indeed a field. So, we emulate `dependent
typing' by restricting the production of the values of desired types.


(* A bit of infrastructure *)
module type KIND  = sig type kind end
type domain_is_field
type domain_is_ring
module KindF      = struct type kind = domain_is_field end
module KindR      = struct type kind = domain_is_ring  end
module type DOMAIN = sig include KIND type v val zero : v end
module type DOMAINR = DOMAIN with type kind = domain_is_ring
module type DOMAINF = DOMAIN with type kind = domain_is_field

module Float : DOMAINF = struct
  include KindF
  type v = float
  let zero = 0.0
end;;
module Integer  : DOMAINR = struct 
  include KindR
  type v = int
  let zero = 0
end;;


(* The field D has a general DOMAIN type, abstracted over `kind' *)
module type DUPDATE = sig module D: DOMAIN val update : unit -> unit end;;

(* But the structures of the type DUPDATE can only produced by the
   following two functors. And DivisionUpdate will require the
   _specific_ field DOMAINF rather than general domain.
*)
module DivisionUpdate(D: DOMAINF) : DUPDATE = struct
  module D = D
  let update () = print_endline "division update"
end;;

module GeneralUpdate(D: DOMAIN) : DUPDATE = struct
  module D = D
  let update () = print_endline "general update"
end;;

module Trans (U:DUPDATE) : sig
  val zero : U.D.v
  val update : unit -> unit
end = struct
  let zero = U.D.zero
  let update = U.update
end;;

(* the following three work *)
module A = Trans(DivisionUpdate(Float));;
module B = Trans(GeneralUpdate(Float));;
module C = Trans(GeneralUpdate(Integer));;

(* But this gives an error -- a field is not a ring. Just as we wanted. *)
module D = Trans(DivisionUpdate(Integer));;


The second solution is based in re-writing the type

> module type Trans = functor(U:UPDATE) ->  functor(D:DOMAIN) -> sig ... end

into something more refined:

> module type Trans = functor(K:KIND) -> functor(U:UPDATE with type
> kind ...) ->  functor(D:DOMAIN with type kind ...) -> sig ... end

so now we can explicitly deal with the distinction between different
kinds. Basically, we lifted the parameterization over kind. More
concretely, given the above KIND infrastructure, we continue.

module type UPDATE2 = sig
  type kind
  module F : functor (D: DOMAIN with type kind = kind) ->
              sig val update : unit -> unit end
end;;

(* This module has a specific Kind: a field *)
module DivisionUpdate2  = struct
 include KindF
 module F(D: DOMAINF) =
   struct
     let update () = print_endline "division update"
   end
end;;

(* This module is essentially universally quantified over KIND. It
   accepts any KIND *)
module GeneralUpdate2(K:KIND) = struct
 type kind = K.kind
 module F(D: DOMAIN with type kind = kind) =
   struct
     let update () = print_endline "general update"
   end
end;;

module Trans2 (K:KIND)(U:UPDATE2 with type kind = K.kind)
    (D:DOMAIN with type kind = K.kind) : sig
  val zero : D.v
  val update : unit -> unit
end = struct
  module U = U.F(D)
  let zero = D.zero
  let update = U.update
end;;

(* the following three work: *)

module A = Trans2(KindF)(DivisionUpdate2)(Float);;

(* We have to specifically instantiate a universally quantified
   structure GeneralUpdate2 *)
module B = Trans2(KindF)(GeneralUpdate2(KindF))(Float);;

module C = Trans2(KindR)(GeneralUpdate2(KindR))(Integer);;

(* But the following two don't work -- just as we wanted them not to.
   The last line shows that we can't lie about the kind of Integer *)
module D = Trans2(KindR)(DivisionUpdate2)(Integer);;
module D' = Trans2(KindF)(DivisionUpdate2)(Integer);;


The third solution seems closer to the desired one, although it has a
drawback in being simplified. We need a bounded quantification
over module types rather than just quantification. We start with a new
infrastructure, which should make the lattice of module types and
structures apparent. It would be great if we did not have to repeat
the same thing at the type and module levels.

module type KIND  = sig end
module type KINDR = sig include KIND type domain_is_ring end
module type KINDF = sig include KINDR type domain_is_field end

module KindR = struct type domain_is_ring end
module KindF = struct include KindR type domain_is_field end

module type DOMAIN = sig type v val zero : v end
module type DOMAINR = sig include DOMAIN include KINDR end
module type DOMAINF = sig include DOMAIN include KINDF end

(* define two domains as before *)
module Float : DOMAINF = struct
  include KindF
  type v = float
  let zero = 0.0
end;;
module Integer  : DOMAINR = struct 
  include KindR
  type v = int
  let zero = 0
end;;

(* Here's the main part. Alas, it should actually say that ReqDomain
  is a subtype of a DOMAIN... We need to fiddle with `include' to
  factor out the main DOMAIN part and thus to achieve the bounded
  quantification. But it is too late for today, and it works for
  a simple example. *)

module type UPDATE2 = sig
  module type ReqDomain
  module F : functor (D: ReqDomain) ->
              sig val update : unit -> unit end
end;;

(* Two sample update modules *)

module DivisionUpdate2  = struct
 module type ReqDomain = DOMAINF
 module F(D: DOMAINF) =
   struct
     let update () = print_endline "division update"
   end
end;;

module GeneralUpdate2 = struct
 module type ReqDomain = DOMAIN
 module F(D: DOMAIN) =
   struct
     let update () = print_endline "general update"
   end
end;;

(* And finally, our functor *)

module Trans2 (U:UPDATE2) (D:U.ReqDomain) : sig
  val update : unit -> unit
end = struct
  module U = U.F(D)
  let update = U.update
end;;


(* These three tests typecheck *)
module A = Trans2(DivisionUpdate2)(Float);;
module B = Trans2(GeneralUpdate2)(Float);;
module C = Trans2(GeneralUpdate2)(Integer);;

(* This reports the error that DivisionUpdate2.ReqDomain
   requires the field `domain_is_field' but Integer fails to provide it.
   This is the clearest error message *)
module D = Trans2(DivisionUpdate2)(Integer);;