# Re: Non generalizable type of constants?

From: Pierre Weis (Pierre.Weis@inria.fr)
Date: Mon Feb 15 1999 - 18:45:30 MET

From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <199902151745.SAA19162@pauillac.inria.fr>
Subject: Re: Non generalizable type of constants?
Date: Mon, 15 Feb 1999 18:45:30 +0100 (MET)

> 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
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
> --