caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: Tyng-Ruey Chuang <trc@iis.sinica.edu.tw>
Cc: caml-list@inria.fr, trc@iiserv.iis.sinica.edu.tw
Subject: Re: [Caml-list] weak type variables in module type declarations
Date: Mon, 28 May 2001 14:50:50 +0200	[thread overview]
Message-ID: <20010528145050.E19801@pauillac.inria.fr> (raw)
In-Reply-To: <200105231324.f4NDOgc28482@mail.iis.sinica.edu.tw>; from trc@iis.sinica.edu.tw on Wed, May 23, 2001 at 09:24:42PM +0800

> O'caml compiler does not seem to recognize user-specified 
> weak type variables. The compiler, however, will automatically
> produce weak type variables when they are needed.
> This behavior has been observed and reported as "Id 246"
> in the "Known bugs" list (and classified as "not a bug").

There is a small bug, which is that weak type variables as printed by
the compiler should not be parse-able as regular type variables.  They
should be unparseable (e.g. '?a instead of '_a), or at the very least,
the compiler should emit a warning when encountering a type variable
starting with an _.

That there is no syntax for weak variables is a conscious decision,
not a bug.  "Weak" (non-generalized) variables represent
under-constrained types that the type inference algorithm failed to
determine, but cannot generalize either.  When users put types in
module signatures or type constraints, they are expected to put
actual, fully-determined types; just leaving "holes" in these types
make little sense to me.  In particular:

> 	module type SUM =
> 	sig
> 	  type ('a, 'b) t = Pink of 'a | Blue of 'b
> 
> 	  val pair : ('_a -> ('_a, '_b) t) * ('_a -> ('_a, '_b) t)
> 	end
> 	module Sum : SUM =
> 	struct
> 	  type ('a, 'b) t = Pink of 'a | Blue of 'b
> 	  let pair = (id $ (fun a -> Pink a), id $ (fun b -> Pink b))
> 	end

Assuming the _a in SUM are mapped to non-generalized variables, these
will be instantiated to actual types ta, tb at the first use of Sum;
so why not defining SUM as

> 	module type SUM =
> 	sig
> 	  type ('a, 'b) t = Pink of 'a | Blue of 'b
> 	  val pair : (ta -> (ta, tb) t) * (ta -> (ta, tb) t)
> 	end

Either you need "pair" to be polymorphic, in which case its definition
should be eta-expanded, or a monomorphic "pair" is OK, in which case
you should give its true type in the signature, as above.  I fail to
see what good it would make to have '_a variables in the SUM signature.

- Xavier Leroy
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr


      parent reply	other threads:[~2001-05-28 12:51 UTC|newest]

Thread overview: 4+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2001-05-23 13:24 Tyng-Ruey Chuang
2001-05-23 13:57 ` Remi VANICAT
2001-05-28  8:03 ` Francois Pottier
2001-05-28 12:50 ` Xavier Leroy [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=20010528145050.E19801@pauillac.inria.fr \
    --to=xavier.leroy@inria.fr \
    --cc=caml-list@inria.fr \
    --cc=trc@iis.sinica.edu.tw \
    --cc=trc@iiserv.iis.sinica.edu.tw \
    /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).