[Caml-list] weak type variables in module type declarations

[Caml-list] weak type variables in module type declarations

[Tyng-Ruey Chuang]

Dear all,

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"). See
http://www.ocaml.org/bin/caml-bugs/not%20a%20bug?expression=weak;user=guest

What do you do to get around this? In my case, the week type variables
are indeed useful, and I want to keep them. But since I have no way
in putting weak type variables in module type declarations, I am prevented
to program in a modular way. Consider the following code segment:


	let ($) f g x = f (g x)   (* functional composition *)
	let id x = x              (* the identity function  *)

	module 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

	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


The compiler report module type SUM as

	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

which is different from my specification. Therefore, I cannot write
code like

	module Empty = functor (S: SUM) -> struct  end
	module E = Empty(Sum)

because the last line produces a "signature dismatch" error from
the compiler.

Of course, the dismatch goes away if the code for module Sum is changed to

        module Sum =
        struct
          type ('a, 'b) t = Pink of 'a | Blue of 'b
          let pair = ((fun a -> Pink a), (fun b -> Pink b))
        end                                                                    

because the week type variables now disappear. However, this is not what
I want. I program mostly in equational style. The function "id"
in the original definition of module Sum in fact is a complex function
that better to be left alone. I also need the two occurrences 
of the weak type variable '_a to resolve to the same type.

The usual Obj.magic trick to coerce the compiler to accept unsafe
value definition does not work either, as it cannot eliminate 
weak types.

I will appreciate any thought on how to deal with this situation.

Last, but not least, many thanks to the Caml team for
the fine language and compiler.

Tyng-Ruey Chuang
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

Re: [Caml-list] weak type variables in module type declarations

[Remi VANICAT]

Tyng-Ruey Chuang <trc@iis.sinica.edu.tw> writes:

> Dear all,
> 
> 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"). See
> http://www.ocaml.org/bin/caml-bugs/not%20a%20bug?expression=weak;user=guest
> 
> What do you do to get around this? In my case, the week type variables
> are indeed useful, and I want to keep them. But since I have no way
> in putting weak type variables in module type declarations, I am prevented
> to program in a modular way. Consider the following code segment:
> 
> 
> 	let ($) f g x = f (g x)   (* functional composition *)
> 	let id x = x              (* the identity function  *)
> 
> 	module 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

i really don't believe you want weak type here : weak type are that
will be determine latter :
if you make a 
Sum.pair 1 2
then after this, Sum.pair will have the mostly monomorphic type 
    val pair : (int -> (int, '_b) t) * (int -> (int, '_d) t)

you may have something very similar, but without weaktype, thanks to
an eta-transformation :

module Sum =
struct 
  type ('a, 'b) t = Pink of 'a | Blue of 'b
  let pair = ((fun x -> (id $ (fun a -> Pink a)) x),(fun x -> (id $ (fun b -> Pink b)) x));;
end

which have as type:

module Sum :
  sig
    type ('a, 'b) t = Pink of 'a | Blue of 'b
    val pair : ('a -> ('a, 'b) t) * ('c -> ('c, 'd) t)
  end

Which is probably what you want.

The problem with weak type is mostly a FAQ, you should read the FAQ
at this subject
-- 
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

Re: [Caml-list] weak type variables in module type declarations

[Francois Pottier]

Dear Tyng-Ruey,

Weak type variables are not allowed to appear in declared signatures,
because there would be no good way of defining their meaning.

Instead of

> 	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

how about trying

  module type SUM =
  sig
    type a
    type b
    type t = Pink of a | Blue of b

    val pair: (a -> t) * (a -> t)
  end

Then, you can use, say,

  SUM with type a = int
       and type b = bool

in a context where you know that a and b should be instantiated to
int and bool, respectively.

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

Re: [Caml-list] weak type variables in module type declarations

[Xavier Leroy]

> 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