From: Francois Pottier <francois.pottier@inria.fr>
To: Charles Martin <joelisp@yahoo.com>
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] type proofs
Date: Mon, 10 Dec 2001 09:06:12 +0100 [thread overview]
Message-ID: <20011210090612.A2025@pauillac.inria.fr> (raw)
In-Reply-To: <20011207212818.27730.qmail@web9207.mail.yahoo.com>; from joelisp@yahoo.com on Fri, Dec 07, 2001 at 01:28:18PM -0800
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
prev parent reply other threads:[~2001-12-10 8:06 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2001-12-07 21:28 Charles Martin
2001-12-07 22:14 ` Markus Mottl
2001-12-08 2:20 ` Jacques Garrigue
2001-12-10 8:06 ` Francois Pottier [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20011210090612.A2025@pauillac.inria.fr \
--to=francois.pottier@inria.fr \
--cc=caml-list@inria.fr \
--cc=joelisp@yahoo.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).