Non generalizable type of constants?

Non generalizable type of constants?

[Thorsten Ohl]

OK, maybe I'm really too dumb to use O'Caml, but can some kind soul
explain why in

    module type Ring = sig type t val unit : t end
    
    module Group (R : Ring) =
      struct
	type 'a t = Unit | Prod of (R.t * 'a)
	let unit = Unit
	let atom a = Prod (R.unit, a)
      end
    
    module FreeRing (R : Ring) =
      struct
	module M = Group(R)
	module A = Group(R)
	type 'a t = 'a M.t A.t
	let unit_good = A.Prod (R.unit, M.unit)
	let unit_bad = A.atom (M.unit)
      end

O'Caml infers the types

      val unit_good : 'a M.t A.t
      val unit_bad : '_a M.t A.t

respectively?  As one might guess, I want to make [['a Group.t]]
abstract (because I want to hide a more complicated structure), in
which case the definition of [[unit_good]] will not work any more.  At
the same time, I need [[unit]] to have type [['a FreeRing.t]] and not
[['_a FreeRing.t]].

The usual tricks for functions with non generalizable argument types
don't work.  What can one do for constants?  Or am I overlooking
something obvious?

Merci,
-Thorsten
-- 
Thorsten Ohl, Physics Department, TU Darmstadt -- ohl@hep.tu-darmstadt.de
http://heplix.ikp.physik.tu-darmstadt.de/~ohl/ [<=== PGP public key here]

Re: Non generalizable type of constants?

[Pierre Weis]

> OK, maybe I'm really too dumb to use O'Caml, but can some kind soul
> explain why in
> 
>     module type Ring = sig type t val unit : t end
>     
>     module Group (R : Ring) =
>       struct
> 	type 'a t = Unit | Prod of (R.t * 'a)
> 	let unit = Unit
> 	let atom a = Prod (R.unit, a)
>       end
>     
>     module FreeRing (R : Ring) =
>       struct
> 	module M = Group(R)
> 	module A = Group(R)
> 	type 'a t = 'a M.t A.t
> 	let unit_good = A.Prod (R.unit, M.unit)
> 	let unit_bad = A.atom (M.unit)
>       end
> 
> O'Caml infers the types
> 
>       val unit_good : 'a M.t A.t
>       val unit_bad : '_a M.t A.t

Because unit_bad is a function application (that cannot be
generalized, due to value restriction polymorphism), while unit_good is a
constructor application and hence is a generalizable value.

> respectively?  As one might guess, I want to make [['a Group.t]]
> abstract (because I want to hide a more complicated structure), in
> which case the definition of [[unit_good]] will not work any more.  At
> the same time, I need [[unit]] to have type [['a FreeRing.t]] and not
> [['_a FreeRing.t]].
> 
> The usual tricks for functions with non generalizable argument types
> don't work.  What can one do for constants?  Or am I overlooking
> something obvious?

If you insist at abstracting the type Groupe.t, I'm not aware of any
solution to your problem, except turning your unit_bad identifier into
a function let unit_bad () = A.atom (M.unit). More generally, what you
call constants are computed values, even if the computation is simple
in your case, hence we have the general problem of references.

> Merci,
> -Thorsten
> -- 
> Thorsten Ohl, Physics Department, TU Darmstadt -- ohl@hep.tu-darmstadt.de
> http://heplix.ikp.physik.tu-darmstadt.de/~ohl/ [<=== PGP public key here]
> 

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

Re: Non generalizable type of constants?

[Thorsten Ohl]

Pierre Weis <Pierre.Weis@inria.fr> writes:

> If you insist at abstracting the type Groupe.t,

I do, because this way I can hide details of different groups from
free constructions over them ...

> I'm not aware of any solution to your problem, except turning your
> unit_bad identifier into a function let unit_bad () = A.atom (M.unit).

Syntactically, It's not pretty, but I can live with it.  I shied away
from this because I was not sure about the result of

  module F = FreeRing ( some ring ...)
  compare (F.unit_bad ()) (F.unit_bad ())

in this case.  Does O'Caml guarantee that the expression will always
evaluate to 0?  [ Currently it appears to, but can I depend on it? ]

> More generally, what you call constants are computed values, even if
> the computation is simple in your case, hence we have the general
> problem of references.

I had this confused, thanks for pointing it out!
-Thorsten
-- 
Thorsten Ohl, Physics Department, TU Darmstadt -- ohl@hep.tu-darmstadt.de
http://heplix.ikp.physik.tu-darmstadt.de/~ohl/ [<=== PGP public key here]

Re: Non generalizable type of constants?

[Pierre Weis]

> > I'm not aware of any solution to your problem, except turning your
> > unit_bad identifier into a function let unit_bad () = A.atom (M.unit).
> 
> Syntactically, It's not pretty, but I can live with it.  I shied away
> from this because I was not sure about the result of
> 
>   module F = FreeRing ( some ring ...)
>   compare (F.unit_bad ()) (F.unit_bad ())
> 
> in this case.  Does O'Caml guarantee that the expression will always
> evaluate to 0?  [ Currently it appears to, but can I depend on it? ]

Yes, since constant constructors are uniquely represented.

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/