[Caml-list] type proofs

[Caml-list] type proofs

[Charles Martin]

I have the usual kind of type error:

Values do not match:
  val send : ('a, int, 'b) t -> 'a -> int
is not included in
  val send : ('a, 'b, 'c) t -> 'a -> int

Now, this is just the tip of an iceberg that goes very deep.  Does anyone have
a tool somewhere that will print out a more complete type proof?  I could check
such a proof over to find the true mistake.

Failing such a tool, can anyone suggest some power techniques that will speed
up my type debugging?

Thanks!

__________________________________________________
Do You Yahoo!?
Send your FREE holiday greetings online!
http://greetings.yahoo.com
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] type proofs

[Markus Mottl]

On Fri, 07 Dec 2001, Charles Martin wrote:
> Failing such a tool, can anyone suggest some power techniques that will speed
> up my type debugging?

Two standard techniques:

  * Make types in the code more general by introducing type holes
    (e.g. by replacing some suspicious expression with "assert false").
    If things suddenly compile, you know where the evil type originates
    from.

  * Add explicit type annotations to suspicious expressions to let
    type errors appear earlier, i.e. more closely to the source of
    the problem.

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] type proofs

[Jacques Garrigue]

From: Charles Martin <joelisp@yahoo.com>

> I have the usual kind of type error:
> 
> Values do not match:
>   val send : ('a, int, 'b) t -> 'a -> int
> is not included in
>   val send : ('a, 'b, 'c) t -> 'a -> int
> 
> Now, this is just the tip of an iceberg that goes very deep.  Does
> anyone have a tool somewhere that will print out a more complete
> type proof?  I could check such a proof over to find the true
> mistake.

You can read your source code in the ocamlbrowser editor, and
typecheck it (compiler menu). Then you will be able to check the type
of any subexpression, which is equivalent to having a proof of the
typing.

Not that this works particularly well in your case, since the type error
above is at the module level, and your implementation has been checked
succesfully. I know of no tool to build a partial proof, which would
be needed when type checking is not succesful.

Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] type proofs

[Francois Pottier]

On Fri, Dec 07, 2001 at 01:28:18PM -0800, Charles Martin wrote:
> I have the usual kind of type error:
> 
> Values do not match:
>   val send : ('a, int, 'b) t -> 'a -> int
> is not included in
>   val send : ('a, 'b, 'c) t -> 'a -> int

Your implementation is well-typed, but less general than what's
declared in your interface. The right thing to do is to add type
annotations to your code to help pinpoint the error location.
One would like to write:

  let send (x : ('a, 'b, 'c) t) (y : 'a) = ...

Unfortunately, this will not help, because O'Caml interprets these
type variables as existentially bound, i.e. it thinks it is OK to
instantiate 'b with int. There is no way, as far as I know, to require
them to be intepreted as universally bound. One work-around here is
to write:

  let send (x : ('a, bool, 'c) t) (y : 'a) = ...

Here, if your code were general enough, your implementation would still
typecheck. However, because the inferred type mentions int and you have
required bool, a type error will arise somewhere, and that should help
you locate the error. (Here, I have used bool, but any concrete or
abstract type other than int would do.) Of course, you'll need to remove
the annotation when done.

I hope this helps,

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr