When looking at inferred types in the presence of modules and
combinations of abstract and concrete types, the results are often quite
puzzling. For small pieces of code, it is not a big issue. When one is
using 4th-order functors (!), with a mixture of abstract and concrete
types, a fair amount of type synonyms, error message become extremely
difficult to interpret!
Below is some (largish for an email) code that demonstrates this. It
seems difficult to show how puzzling this gets with much smaller code,
although one can indeed reproduce the behaviour with smaller code.
Consider first
module Sig = struct
type domain_is_field
type domain_is_ring
module type DOMAIN = sig
type kind
type v
val z : v
end
module type COLL = sig
module Dom : DOMAIN
type coll
end
end
module Doms = struct
open Sig
module FDomain = struct
type kind = domain_is_field
type v = float
let z = 0.0
end
module IDomain = struct
type kind = domain_is_ring
type v = int
let z = 0
end
module GColl(Dom:DOMAIN) =
struct
module Dom = Dom
type coll = Dom.v list
end
end ;;
In the above, the printed types all seem quite reasonable.
Now we start with some more complex stuff:
module GEF = struct
open Sig
module DivisionUpdate
(C:COLL with type Dom.kind = domain_is_field) = struct
let update x = x
end
module Gen(C: COLL)
(Update: functor(C:COLL with type Dom.kind = C.Dom.kind)
-> sig val update : C.Dom.v -> C.Dom.v end) =
struct
module U = Update(C)
let foo = U.update(C.Dom.z)
end
end;;
where the printed type is
# module GEF :
sig
module DivisionUpdate :
functor
(C : sig
module Dom :
sig type kind = Sig.domain_is_field type v val z : v end
type coll
end) ->
sig val update : 'a -> 'a end
module Gen :
functor (C : Sig.COLL) ->
functor
(Update : functor
(C : sig
module Dom :
sig
type kind = C.Dom.kind
type v
val z : v
end
type coll
end) ->
sig val update : C.Dom.v -> C.Dom.v end) ->
sig
module U : sig val update : C.Dom.v -> C.Dom.v end
val foo : C.Dom.v
end
end
which seems fair enough. When we start to "test" this, we get:
module Test = GEF.Gen(Doms.GColl(Doms.FDomain))(GEF.DivisionUpdate);;
let test = Test.foo;;
# module Test :
sig
module U :
sig
val update :
Doms.GColl(Doms.FDomain).Dom.v -> Doms.GColl(Doms.FDomain).Dom.v
end
val foo : Doms.GColl(Doms.FDomain).Dom.v
end
# val test : Doms.GColl(Doms.FDomain).Dom.v = 0.
Note how the type of update and foo look very "complex", even though the
typechecker seems to know quite well that 'test' is actually of type
float. How is one supposed to know that the typechecker knows this and
that ...Dom.v is not abstract?
If we continue in that vein, contrast the following:
module C_F = Doms.GColl(Doms.FDomain);;
module Test1 = GEF.Gen(C_F)(GEF.DivisionUpdate);; (* works *)
module C_I = Doms.GColl(Doms.IDomain);;
module Test2 = GEF.Gen(C_I)(GEF.DivisionUpdate);; (* throws an error, as
expected *)
The biggest difference is that FDomain has kind = domain_is_field while
IDomain has kind = domain_is_ring.
Let's look at the printed type of C_F and Test1:
# module C_F :
sig
module Dom :
sig type kind = Doms.FDomain.kind type v = Doms.FDomain.v val z :
v end
type coll = Dom.v list
end
# module Test1 :
sig
module U : sig val update : C_F.Dom.v -> C_F.Dom.v end
val foo : C_F.Dom.v
end
Why Doms.FDomain.kind instead of Sigs.domain_is_field for the kind?
Since test1 *works*, clearly these are known to be the same.
Also, not how foo has type C_F.Dom.v -- which one has to chase to Dom.v,
to Doms.FDomain.v, and finally to float. When this occurs in an error
message, having to do 4 (or more) levels of type-expansions can be quite
difficult. (And misleading too, but that is a different issue).
Now let's look at what we get for the rest:
# module C_I :
sig
module Dom :
sig type kind = Doms.IDomain.kind type v = Doms.IDomain.v val z :
v end
type coll = Dom.v list
end
and then a long error message for Test2, which ends with
Modules do not match:
sig type kind = C_I.Dom.kind type v = Dom.v val z : v end
is not included in
sig type kind = Sig.domain_is_field type v val z : v end
Type declarations do not match:
type kind = C_I.Dom.kind
is not included in
type kind = Sig.domain_is_field
Now, C_I.Dom.kind is actually Sig.domain_is_ring -- why wasn't that
printed? That would have been SO much more informative! In similar
situations, one can take a long time chasing down why it seems that
C_I.Dom.kind was somehow abstract when it should have been concrete, and
so on.
Would it be possible to get some switches to optionally ask for all
types to be fully expanded? Also, it would be nice to be able to
visually distinguish between an abstract type and a concrete but elided
type even when not asking for types to be expanded.
Note that in other situations (the code is even larger), one can get a
strange mixture of non-expanded, partially-expanded and fully-expanded
types all for essentially the same situation, although it seems that
this latter part may be due to MetaOCaml rather than OCaml. But it is
rather difficult to be certain...
Jacques
PS: the work that led up to this email is joint work with Oleg Kiselyov.
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
|
