This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Variance problem in higher-order Functors?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2006-07-23 (19:58) From: Jacques Carette Subject: Variance problem in higher-order Functors?
```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! *)
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 *)

(* 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

```