Variance problem in higher-order Functors?

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);;

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