Version française
Home     About     Download     Resources     Contact us    
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: -- (:)
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