Caml implementation of the relaxed value restriction

Caml implementation of the relaxed value restriction

[Julien SIGNOLES]

Hello,

In the article "Many Holes in Hindley-Milner" [1], Sam Lindley claims
that the type of x is ('a * 'a s, int) NList.t in the following ocaml
program because of Garrigue's relaxed value restriction [2].
==========
type 'a s

module NList : sig
  type (+'length, +'elem_type) t
  val nil : ('m*'m, 'a) t
  val cons: 'a * ('m*'n, 'a) t -> ('m*'n s,'a) t
end = struct
  type ('i,'a) t = 'a list
  let nil = []
  let cons (x, l) = x :: l
end

let x = NList.cons (1, NList.nil)
==========

But, both with ocaml v3.10.2 and ocaml v3.12.0+dev1 (2008-12-03) (that
is the current cvs version), the infered type of [x] only contains a
weak type variable: ('_a * '_a s, int) NList.t.

I quickly look at the typing rules introduced by Jacques Garrigue in [2]
and it seems to me that Sam Lindley is right: [x] is generalisable in
the above program.

So, what's wrong here?

[1] Many Holes in Hindley-Milner.
    Sam Lindley. In ACM Sigplan Workshop of ML 2008, Victoria, British
    Columbia, Canada, September 2008.
[2] Relaxing the value restriction.
        Jacques Garrigue. In International Symposium on Functional and
        Logic Programming, Nara, April 2004. Springer-Verlag LNCS 2998.

Best regards,
Julien Signoles
-- 
Researcher-engineer
CEA LIST, Software Reliability Lab
91191 Gif-Sur-Yvette Cedex
tel:(+33)1.69.08.71.83  fax:(+33)1.69.08.83.95  Julien.Signoles@cea.fr

Re: [Caml-list] Caml implementation of the relaxed value restriction

[Mark Shinwell]

On Wed, Jan 14, 2009 at 04:31:24PM +0100, Julien SIGNOLES wrote:
> In the article "Many Holes in Hindley-Milner" [1], Sam Lindley claims
> that the type of x is ('a * 'a s, int) NList.t in the following ocaml
> program because of Garrigue's relaxed value restriction [2].
> ==========
> type 'a s
> 
> module NList : sig
>   type (+'length, +'elem_type) t
>   val nil : ('m*'m, 'a) t
>   val cons: 'a * ('m*'n, 'a) t -> ('m*'n s,'a) t
> end = struct
>   type ('i,'a) t = 'a list
>   let nil = []
>   let cons (x, l) = x :: l
> end
> 
> let x = NList.cons (1, NList.nil)
> ==========
> 
> But, both with ocaml v3.10.2 and ocaml v3.12.0+dev1 (2008-12-03) (that
> is the current cvs version), the infered type of [x] only contains a
> weak type variable: ('_a * '_a s, int) NList.t.
> 
> I quickly look at the typing rules introduced by Jacques Garrigue in [2]
> and it seems to me that Sam Lindley is right: [x] is generalisable in
> the above program.
> 
> So, what's wrong here?

You need to say "type +'a s", otherwise the compiler (since "s" is an
abstract type) cannot know the variance of that type parameter inside a
value of type 'a s.  That information is needed to determine how to
generalize the type of x.

Mark