Variance problem in higherorder Functors?
 oleg@p...
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060726 (06:48) 
From:  oleg@p... 
Subject:  Variance problem in higherorder Functors? 
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 higherorder 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 rewriting 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);;