[
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: | 2006-07-23 (21:12) |
From: | Andreas Rossberg <AndreasRossberg@w...> |
Subject: | Re: [Caml-list] Variance problem in higher-order Functors? |
"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