English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
[Caml-list] weak type variables in module type declarations
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2001-05-28 (12:51)
From: Xavier Leroy <Xavier.Leroy@i...>
Subject: Re: [Caml-list] weak type variables in module type declarations
> 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