Polymorphic recursion

Polymorphic recursion

[Loup Vaillant]

I was reading Okasaki's book, "Purely functionnal data structures",
and discovered that ML (and Ocaml) doesn't support non uniforms
function definitions.

So, even if:

(**)
type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);;
(**)

is correct,

(**)
let rec size = fun
   | Unit -> 0
   | Seq(_, b) -> 1 + 2 * size b;;
(**)

is not. Here is the error:
#
| Seq(_, b) -> 1 + 2 * size b;;
This expression (the last 'b') has type seq ('a * 'a) but is here used
with type seq 'a
#

Why?
Can't we design a type system which allow this "size" function?
Can't we implement non uniform recursive function (efficiently, or at all)?.

I suppose the problem is somewhat difficult, but I can't see where.

Regards,
Loup Vaillant

Re: [Caml-list] Polymorphic recursion

[Jeremy Yallop]

Loup Vaillant wrote:
> I was reading Okasaki's book, "Purely functionnal data structures",
> and discovered that ML (and Ocaml) doesn't support non uniforms
> function definitions.
> 
> So, even if:
> 
> (**)
> type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);;
> (**)
> 
> is correct,
> 
> (**)
> let rec size = fun
>   | Unit -> 0
>   | Seq(_, b) -> 1 + 2 * size b;;
> (**)
> 
> is not.

Right.  You can write polymorphic-recursive functions if you wrap them 
in recursive modules, though:

   module rec Size : sig val size : 'a seq -> int end = struct
     let rec size = function
       | Unit -> 0
       | Seq (_, b) -> 1 + 2 * Size.size b
   end

Hope this helps,

Jeremy.

Re: [Caml-list] Polymorphic recursion

[Till Varoquaux]

There is indeed an issue with polymorphic recursion. It has been shown
that allowing polymorphic recursion in an ML like language would make
the type inference undecidable. One workaround would be for the
typechecker to use type annotations in some given cases. This is
however not the case in Ocaml: type information are either required or
only useful to debug/document some code/"restrict" the type of a given
variable.

Therefor, if you wish to use polymorphic recursion (yep you can) you
might want to use something where you have to specify the type; this
includes records, objects and recursive modules. So this

type 'a seq = Unit | Seq of ('a * ('a * 'a)seq)

type szRec={f:'a.'a seq -> int};;

let size=
 let rec s =
  {f=function
    | Unit -> 0
    | Seq(_, b) -> 1 + 2 * s.f b}
 in
 s.f

might be what you where yearning for.

Cheers,
Till

On 4/3/07, Loup Vaillant <loup.vaillant@gmail.com> wrote:
> I was reading Okasaki's book, "Purely functionnal data structures",
> and discovered that ML (and Ocaml) doesn't support non uniforms
> function definitions.
>
> So, even if:
>
> (**)
> type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);;
> (**)
>
> is correct,
>
> (**)
> let rec size = fun
>    | Unit -> 0
>    | Seq(_, b) -> 1 + 2 * size b;;
> (**)
>
> is not. Here is the error:
> #
> | Seq(_, b) -> 1 + 2 * size b;;
> This expression (the last 'b') has type seq ('a * 'a) but is here used
> with type seq 'a
> #
>
> Why?
> Can't we design a type system which allow this "size" function?
> Can't we implement non uniform recursive function (efficiently, or at all)?.
>
> I suppose the problem is somewhat difficult, but I can't see where.
>
> Regards,
> Loup Vaillant
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Polymorphic recursion

[brogoff]

On Tue, 3 Apr 2007, Till Varoquaux wrote:
> Therefor, if you wish to use polymorphic recursion (yep you can) you
> might want to use something where you have to specify the type; this
> includes records, objects and recursive modules. So this
>
> type 'a seq = Unit | Seq of ('a * ('a * 'a)seq)
>
> type szRec={f:'a.'a seq -> int};;
>
> let size=
>  let rec s =
>   {f=function
>     | Unit -> 0
>     | Seq(_, b) -> 1 + 2 * s.f b}
>  in
>  s.f
>
> might be what you where yearning for.

What I'd be yearning for would be more like

let rec size : 'a . 'a seq -> int =
  fun s ->
    match s with Unit -> 0 | Seq(_,b) -> 1 + 2 * (size b)

rather than having to use recursive modules or higher rank polymorphism
of record fields/polymorphic methods.

-- Brian

Re: [Caml-list] Polymorphic recursion

[skaller]

On Tue, 2007-04-03 at 13:00 -0700, brogoff wrote:
> On Tue, 3 Apr 2007, Till Varoquaux wrote:
> > Therefor, if you wish to use polymorphic recursion (yep you can) you
> > might want to use something where you have to specify the type; this
> > includes records, objects and recursive modules. So this
> >
> > type 'a seq = Unit | Seq of ('a * ('a * 'a)seq)
> >
> > type szRec={f:'a.'a seq -> int};;
> >
> > let size=
> >  let rec s =
> >   {f=function
> >     | Unit -> 0
> >     | Seq(_, b) -> 1 + 2 * s.f b}
> >  in
> >  s.f
> >
> > might be what you where yearning for.
> 
> What I'd be yearning for would be more like
> 
> let rec size : 'a . 'a seq -> int =
>   fun s ->
>     match s with Unit -> 0 | Seq(_,b) -> 1 + 2 * (size b)
> 
> rather than having to use recursive modules or higher rank polymorphism
> of record fields/polymorphic methods.

Why not:

let fun rec size : 'a . 'a seq -> int =
  | Unit -> 0 
  | Seq(_,b) -> 1 + 2 * (size b)

with a nice camlp4 example for people by nicolas.pouillard@gmail.com ? 


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Polymorphic recursion

[skaller]

On Wed, 2007-04-04 at 11:27 +1000, skaller wrote:

> Why not:
> 
> let fun rec size : 'a . 'a seq -> int =
>   | Unit -> 0 
>   | Seq(_,b) -> 1 + 2 * (size b)
> 
> with a nice camlp4 example for people by nicolas.pouillard@gmail.com ? 

Opps .. should be

	let rec fun .. 
	and fun ..
	and ..
	in
	let fun ..
	and ..

that is, the 'fun' should come after the 'rec' keyword if present.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Polymorphic recursion

[Alain Frisch]

Jeremy Yallop wrote:
> Right.  You can write polymorphic-recursive functions if you wrap them
> in recursive modules, though:
> 
>   module rec Size : sig val size : 'a seq -> int end = struct
>     let rec size = function
>       | Unit -> 0
>       | Seq (_, b) -> 1 + 2 * Size.size b
>   end

Note that you don't even need the "rec" in this example, and that the
same idiom would support mutually recursive functions. To make an
automatic translation simpler, you can simply "open Size" at the
beginning of the structure to avoid rewriting self-references in the
function's body. To support local definitions, you can of course rely on
local modules:

let rec f : 'a 'b. t = E1 in E2

becomes:

let module X = struct
  module rec Y : sig val f : t end = struct
    open Y
    let f = E1
  end
  open Y
  let v = E2
end in
X.v

However, this encoding has an important drawback: you cannot use type
variables currently in scope in t, E1, E2 (as a consequence, we don't
need to explicitly quantify over variables in the function prototype,
the encoding forces all the variables in the function's type to be
universally quantified). By changing the encoding, you can allow
references to those type variables in E2:

let f =
 let module X = struct
   module rec Y : sig val f : t end = struct
     open Y
     let f = E1
   end
 end in
 X.Y.f
in
E2


-- Alain

Re: [Caml-list] Polymorphic recursion

[Loup Vaillant]

Thanks, everybody.
Now, does anyone have an idea of the overheads? I can build syntactic
sugar for all three case (using my "not yet build" Lisp syntax), so
which is more efficient?

Classes?
Recursive modules?
Records?

Thanks,
Loup

2007/4/4, Alain Frisch <Alain.Frisch@inria.fr>:
> Jeremy Yallop wrote:
> > Right.  You can write polymorphic-recursive functions if you wrap them
> > in recursive modules, though:
> >
> >   module rec Size : sig val size : 'a seq -> int end = struct
> >     let rec size = function
> >       | Unit -> 0
> >       | Seq (_, b) -> 1 + 2 * Size.size b
> >   end
>
> Note that you don't even need the "rec" in this example, and that the
> same idiom would support mutually recursive functions. To make an
> automatic translation simpler, you can simply "open Size" at the
> beginning of the structure to avoid rewriting self-references in the
> function's body. To support local definitions, you can of course rely on
> local modules:
>
> let rec f : 'a 'b. t = E1 in E2
>
> becomes:
>
> let module X = struct
>   module rec Y : sig val f : t end = struct
>     open Y
>     let f = E1
>   end
>   open Y
>   let v = E2
> end in
> X.v
>
> However, this encoding has an important drawback: you cannot use type
> variables currently in scope in t, E1, E2 (as a consequence, we don't
> need to explicitly quantify over variables in the function prototype,
> the encoding forces all the variables in the function's type to be
> universally quantified). By changing the encoding, you can allow
> references to those type variables in E2:
>
> let f =
>  let module X = struct
>    module rec Y : sig val f : t end = struct
>      open Y
>      let f = E1
>    end
>  end in
>  X.Y.f
> in
> E2
>
>
> -- Alain
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Polymorphic recursion

[Roland Zumkeller]

On 03/04/07, Loup Vaillant <loup.vaillant@gmail.com> wrote:
> Can't we implement non uniform recursive function (efficiently, or at all)?.

It has actually been done: call ocaml with the option "-rectypes" and
your example will work as is.

Best,

Roland

-- 
http://www.lix.polytechnique.fr/~zumkeller/

Re: [Caml-list] Polymorphic recursion

[Alain Frisch]

Roland Zumkeller wrote:
> On 03/04/07, Loup Vaillant <loup.vaillant@gmail.com> wrote:
>> Can't we implement non uniform recursive function (efficiently, or at
>> all)?.
> 
> It has actually been done: call ocaml with the option "-rectypes" and
> your example will work as is.

No. The example would typecheck and the following type will be inferred:

  val size : ('a * 'a as 'a) seq -> int = <fun>

but since there is no value of type ('a * 'a as 'a) (for some 'a), you
will be able to apply the function only to the value Unit:

# size Unit;;
- : int = 0
# size (Seq (1, Unit));;
This expression has type int * 'a seq but is here used with type
  ('b * 'b as 'b) * ('b * 'b) seq


This is a good illustration of why -rectypes is not enabled by default.


-- Alain

Re: [Caml-list] Polymorphic recursion

[Alain Frisch]

Alain Frisch wrote:
> but since there is no value of type ('a * 'a as 'a)

Sorry, there are actually values in this type, but they are all
structurally equal to the result of "let rec x = (x,x) in x".

-- Alain

Re: Polymorphic recursion

[Stefan Monnier]

> This is a good illustration of why -rectypes is not enabled by default.

In my experience, polymorphic recursion is almost always linked to
datatypes whose recursion is itself polymorphic.  As is the case in
Loup's example.

Has there been work in trying to leverage this connection, so that
polymorphic recursion can be automatically inferred by taking advantage of
the implicit type hint provided by the datatype definition?


        Stefan

Re: [Caml-list] Polymorphic recursion

[Roland Zumkeller]

On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote:
> Alain Frisch wrote:
> > but since there is no value of type ('a * 'a as 'a)
>
> Sorry, there are actually values in this type, but they are all
> structurally equal to the result of "let rec x = (x,x) in x".

Yes, but "('a * 'a as 'a) seq" has more than one value (modulo
structural equality), so it works to *some* extent:

# let rec x = (x,x);;
val x : 'a * 'a as 'a =
# size (Seq (x,Unit));;
- : int = 1
# size (Seq (x, Seq (x,Unit)));;
- : int = 3

However, you are right in pointing out that this limited use won't be
helpful for most applications, so I'd suggest:

# let rec size = function
| Unit -> 0
| Seq (_, b) -> 1 + 2 * size (Obj.magic b);;
    val size : 'a seq -> int = <fun>

The function can be checked in richer type systems with annotations
(e.g. Coq's), so we know that Obj.magic is not dangerous here.

Roland

-- 
http://www.lix.polytechnique.fr/~zumkeller/

Re: [Caml-list] Polymorphic recursion

[Alain Frisch]

Roland Zumkeller wrote:
> The function can be checked in richer type systems with annotations
> (e.g. Coq's), so we know that Obj.magic is not dangerous here.

The fact that something is well-typed in Coq does not mean that you can
just translate it to OCaml by adding a few Obj.magic to make the
type-checker happy. OCaml programmers tend to have a rough mental
picture of what the semantic of the Obj module is and what are the
important properties of the runtime representation of values, but they
often only see part of the picture. Do you know what the following piece
of code does?

let () =
  let x = if ("a" = "b") then Obj.magic 0 else String.copy "abc" in
  for i = 0 to 100000 do ignore (ref [1]) done;
  Gc.major ();
  print_endline x

Well, if I knew Coq, I could prove that "a" is not equal to "b" and thus
that x is always bound to a valid string. So the Caml code should print
"abc". Right?

No. This code compiled with ocamlopt produces a segfault on my machine.
I remember spending hours (and wasting my boss' precious time) on a bug
I introduced in some code because I thought that Obj.magic 0 and
Obj.magic () are equivalent. The code above show that this is not the
case (if you replace 0 with (), it works fine).

If you don't understand what's going on, you'd better not use the Obj
module. If you know why, there is probably some other dark corner which
you don't understand and that will bite you some day.


In the present case, we have good solutions that don't require Obj.
Unless a strong case is made that performance is not adequate, there is
really no reason to use Obj.

-- Alain

Re: [Caml-list] Polymorphic recursion

[brogoff]

On Wed, 4 Apr 2007, Alain Frisch wrote:
> In the present case, we have good solutions that don't require Obj.
> Unless a strong case is made that performance is not adequate, there is
> really no reason to use Obj.

I agree with the "don't use Obj" part, but I think the current solutions
are not that good. Encoding with records or objects is unclear, and
while I find the encoding with recursive modules much clearer, that's
still listed as an experimental feature. It also seems a bit heavy,
using a recursive module just to get polymorphic recursion. Providing a
type for the function and having the compiler use it is the right
solution, IMO. It's not as much performance (though that is important!)
as clarity, admittedly subjective, that I am judging the solutions by.

-- Brian

Re: [Caml-list] Polymorphic recursion

[Brian Hurt]

On Tue, 3 Apr 2007, Loup Vaillant wrote:

> I was reading Okasaki's book, "Purely functionnal data structures",
> and discovered that ML (and Ocaml) doesn't support non uniforms
> function definitions.
>
> So, even if:
>
> (**)
> type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);;
> (**)

This way lies GADTs, which are a really neat idea, but even the 
Haskeller's aren't 100% sure how to implement correctly yet.

In any case, there's a fairly simple work around which does work in the 
current type system, which Okasaki describes IIRC.  Basically, you just 
do:

type 'a tuple = Tuple of 'a tuple * 'a tuple | Leaf of 'a;;

type 'a seq = Unit | Set of 'a tuple * 'a seq;;

which is a bit of a pain, but works.

Brian

Re: [Caml-list] Polymorphic recursion

[Loup Vaillant]

2007/4/5, Brian Hurt <bhurt@spnz.org>:
>
>
> On Tue, 3 Apr 2007, Loup Vaillant wrote:
>
> > I was reading Okasaki's book, "Purely functionnal data structures",
> > and discovered that ML (and Ocaml) doesn't support non uniforms
> > function definitions.
> >
> > So, even if:
> >
> > (**)
> > type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);;
> > (**)
>
> This way lies GADTs, which are a really neat idea, but even the
> Haskeller's aren't 100% sure how to implement correctly yet.
>
> In any case, there's a fairly simple work around which does work in the
> current type system, which Okasaki describes IIRC.  Basically, you just
> do:
>
> type 'a tuple = Tuple of 'a tuple * 'a tuple | Leaf of 'a;;
>
> type 'a mono_seq = Unit | Set of 'a tuple * 'a seq;;
>
> which is a bit of a pain, but works.

(note: I have renamed "mono_seq" for disambiguation)

This workaround doesn't work exactly as intended: as Okasaki pointed
at, the binary tree "tuple" is not guaranteed to be balanced.

Therefore, even if we can build a trivial injection of type
(* seq -> mono_seq *), it will not be a surjection as well.

We have lost an invariant, and are forced to maintain it
programmatically. This kind of workaround is well known: we call it
abstract type. What I find cool with polymorphic types is that more
invariants can be checked directly by the type system.
It has two advantages:
-> It is less error prone when writing the module attached to the type.
-> Sometimes, a programmer outside the module can even do pattern
matching on this type and still be guaranteed she will not produce a
single wrong value.

For these reasons,I wanted a way to exploit polymorphic type. You all
provided three. I don't mind the syntactic burden, provided someone
come up a syntactic shortcut.

Loup

Re: [Caml-list] Polymorphic recursion

[Roland Zumkeller]

On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote:
> The fact that something is well-typed in Coq does not mean that you can
> just translate it to OCaml by adding a few Obj.magic to make the
> type-checker happy.

As I understand Pierre Letouzey's PhD thesis explains how this can be
done. Your example couldn't result from translating a Coq term, since
"String.copy", "ref", and "Gc.major" are not part of its formalism (a
flavour of lambda calculus with inductive types).

> let () =
>   let x = if ("a" = "b") then Obj.magic 0 else String.copy "abc" in
>   for i = 0 to 100000 do ignore (ref [1]) done;
>   Gc.major ();
>   print_endline x

> This code compiled with ocamlopt produces a segfault on my machine.

On my machine it prints "$d$d$d$d$d$d$d$d$d$d$d$d$d$d$d" and when
compiled with ocamlc "abc". Is this a bug?

Roland

-- 
http://www.lix.polytechnique.fr/~zumkeller/

Re: [Caml-list] Polymorphic recursion

[Francois Maurel]

About unintuitive - and, of course, strongly implementation dependent
- Obj.magic stuff, one can also patch your example into:

===
let magic x =
  let y =
    Obj.magic x
  in
  y

let () =
  let x = if ("a" = "b") then magic 0 else String.copy "abc" in
 for i = 0 to 100000 do ignore (ref [1]) done;
  Gc.major ();
 print_endline x
===

which is somehow "correct".

The version
===
let magic x =
  Obj.magic x

 ...
===
is not.

François

On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote:
> Roland Zumkeller wrote:
> > The function can be checked in richer type systems with annotations
> > (e.g. Coq's), so we know that Obj.magic is not dangerous here.
>
> The fact that something is well-typed in Coq does not mean that you can
> just translate it to OCaml by adding a few Obj.magic to make the
> type-checker happy. OCaml programmers tend to have a rough mental
> picture of what the semantic of the Obj module is and what are the
> important properties of the runtime representation of values, but they
> often only see part of the picture. Do you know what the following piece
> of code does?
>
> let () =
>   let x = if ("a" = "b") then Obj.magic 0 else String.copy "abc" in
>   for i = 0 to 100000 do ignore (ref [1]) done;
>   Gc.major ();
>   print_endline x
>
> Well, if I knew Coq, I could prove that "a" is not equal to "b" and thus
> that x is always bound to a valid string. So the Caml code should print
> "abc". Right?
>
> No. This code compiled with ocamlopt produces a segfault on my machine.
> I remember spending hours (and wasting my boss' precious time) on a bug
> I introduced in some code because I thought that Obj.magic 0 and
> Obj.magic () are equivalent. The code above show that this is not the
> case (if you replace 0 with (), it works fine).
>
> If you don't understand what's going on, you'd better not use the Obj
> module. If you know why, there is probably some other dark corner which
> you don't understand and that will bite you some day.
>
>
> In the present case, we have good solutions that don't require Obj.
> Unless a strong case is made that performance is not adequate, there is
> really no reason to use Obj.
>
> -- Alain
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] Polymorphic recursion

[Alain Frisch]

Roland Zumkeller wrote:
> On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote:
>> The fact that something is well-typed in Coq does not mean that you can
>> just translate it to OCaml by adding a few Obj.magic to make the
>> type-checker happy.
> 
> As I understand Pierre Letouzey's PhD thesis explains how this can be
> done. Your example couldn't result from translating a Coq term, since
> "String.copy", "ref", and "Gc.major" are not part of its formalism (a
> flavour of lambda calculus with inductive types).

Here is an example which might fall into this class:

let f n =
  let x = if ("a" = "b") then Obj.magic 0 else (Some n) in
  for i = 0 to 100000 do ignore (Some i) done;
  (match x with Some n -> print_int n | None -> ());
in
f 10

It prints 512 on my machine (when compiled with ocamlopt).

> On my machine it prints "$d$d$d$d$d$d$d$d$d$d$d$d$d$d$d" and when
> compiled with ocamlc "abc". Is this a bug?

No, undefined behaviors are not specified.

-- Alain

Re: [Caml-list] Polymorphic recursion

[Daniel de Rauglaudre]

This simpler example segmentation faults on my machine :

let () =
  let x = if "a" = "b" then Obj.magic 0 else String.copy "abc" in
  for i = 0 to 100000 do ignore (ref [1]) done;
  print_endline x

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

polymorphic recursion

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 142 bytes --]

Hello list,
I'm having trouble finding information on this; does ocaml support
polymorphic recursion and, if so, what's the syntax?
--Jacques

[-- Attachment #2: Type: text/html, Size: 160 bytes --]

Re: Polymorphic recursion

[Pierre Weis]

> Could anyone tell me whether the feature of polymorphic
> recursion is available in Caml-light or OCaml? If so,

Basically, the answer is no for the Caml-light or O'Caml
systems. Plans to add some form of polymorphic recursion is on the way.

For more details, have a look in the archive of this mailing list:

http://pauillac.inria.fr/caml/caml-list/subject.html

Subject: polymorphic recursion

Best regards,

Pierre Weis

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

Polymorphic recursion

[Hongwei Xi]

Hi,

Could anyone tell me whether the feature of polymorphic
recursion is available in Caml-light or OCaml? If so,
how to use it (a simply example would suffice)?

Thanks,

--Hongwei

\~~~~/ \\   //  \\    //    @       Mail: hongwei@cse.ogi.edu
C-o^o,  ))__||   \\__//_  // \\     Url: http://www.cse.ogi.edu/~hongwei
(  ^ )  ))__||    \--/-\\     \\    Tel: +1 503 748 1584 (office)
/ \V\   ))  ||     //   \\     \\   Fax: +1 503 748 1553 (department)
------ //   || o  //     \\     \\// 
Department of Computer Science and Engineering
Oregon Graduate Institute of Science and Technology
P. O. Box 91000, Portland, OR 97291-1000, USA

Re: polymorphic recursion

[Pierre Weis]

> This suggestion is quite close to what Haskell imposes
[...]

> Furthermore, the inferred type scheme for the body of f must be more
> general than its type signature prescribes.

Yes, this is implicit in the rule I proposed.

[...]

> Here is a drawback of your proposal that the Haskell folks are
> currently addressing in a revision of the standard:
> you cannot always write a type signature for a nested function.

That's why I considered extending type constraints to not quantified
type variables.

[...]

> In this case, g really has *type* unit -> 'b without 'b being
> all-quantified. Of course, you could write something like:
> 
> let (f : 'a * 'b -> 'b) =
>   fun (x, (y : '_b)) ->
>     let (g : unit -> '_b) =
>       fun () -> y
>     in g ()
> 
> but that would not be nice.
> If I recall correctly, the current Haskell proposal says that
> variables in the outermost type signature are bound in the body of the 
> corresponding definition.
> That's not nice, either.

I agree with you that this is not that nice, although perfectly
unambiguous. On the other hand, the Haskell proposal does not solve
the fundamental problem: type constraints are still puzzling, since
the confusing between quantified type variables and not quantified
type variables still remains.

This confusion is avoided if we extend type constraints to '_ type
variables.  Note also that the sharing type constraint you pointed out
is complex and hardly ever necessary in practice. (Anyway you
perfectly succeeded in expressing it in the framework of my proposal.)

> An alternative that I could imagine is to include explicit binders for 
> the type variables, i.e., big Lambdas, to indicate their scope
> precisely in the rare cases where it is necessary. It could be
> regarded an error to mix explicitly bound and implicitly bound type
> variables, as this might give rise to misunderstandings.

In my mind, explicit binders for type variables would be a major
change in the language, and may not be worth the
modification. Remember that we mainly want to get rid of meaningless
(or puzzling) type annotations and get an easy way to typecheck
polymorphic recursive functions.

Pierre Weis

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

Re: polymorphic recursion

[Peter Thiemann]

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

    Pierre> I suggest the following simple rules:

    Pierre> (1) type expressions appearing in type constraints are supposed to be
    Pierre> type schemes, implicitely quantified as usual. Scope of type variables
    Pierre> is simply delimited by the parens surrounding the type constraint.

    Pierre> (2) a type constraint (e : sigma) is mandatory. It means that sigma IS
    Pierre> a valid type scheme for e, and indeed sigma is the type scheme
    Pierre> associated to e by the compiler. (This implies that sigma is an
    Pierre> instance of the most general type scheme of e.)

This suggestion is quite close to what Haskell imposes, as far as I
know: if there is a top-level type signature for an identifier f, then
it is taken as a type scheme (implicitly all-quantifying all type
variables) and *all* occurrence of f (including recursive ones) are
type-checked using this signature as assumption.
Furthermore, the inferred type scheme for the body of f must be more
general than its type signature prescribes.

This corresponds to the typing rule

A, f:sigma |- e : sigma'
--------------------------- sigma is a generic instance of sigma'
A |- fix f:sigma. e : sigma

Here is a drawback of your proposal that the Haskell folks are
currently addressing in a revision of the standard:
you cannot always write a type signature for a nested function.
Suppose

let (f : 'a * 'b -> 'b) =
  fun (x, y) ->
    let (g : unit -> 'b) =
      fun () -> y
    in g ()

[this would not type check]
In this case, g really has *type* unit -> 'b without 'b being
all-quantified. Of course, you could write something like:

let (f : 'a * 'b -> 'b) =
  fun (x, (y : '_b)) ->
    let (g : unit -> '_b) =
      fun () -> y
    in g ()

but that would not be nice.
If I recall correctly, the current Haskell proposal says that
variables in the outermost type signature are bound in the body of the 
corresponding definition.
That's not nice, either.

An alternative that I could imagine is to include explicit binders for 
the type variables, i.e., big Lambdas, to indicate their scope
precisely in the rare cases where it is necessary. It could be
regarded an error to mix explicitly bound and implicitly bound type
variables, as this might give rise to misunderstandings.

Having a unified treatment for these things would really make life
easier.

-Peter

Re: polymorphic recursion

[Pierre Weis]

> This is one of those little dark spots in ML-style languages that I
> hope will be cleaned some day by drastic simplifications (as the
> problem with polymorphic refs was drastically simplified by the value
> restriction).  (Argumented) suggestions are welcome.

In my mind the dark spot comes from the confusion between types and
type schemes due to the implicit quantification of type
variables. Writing ML programs, we need type schemes and not
types. Usual semantics for type annotations is ambiguous, since it
rely on strange rules to get rid of the absence of explicit
quantifiers in ML type schemes. Hence the strange semantics of
original ML (and CAML) type annotations: useless to the compiler and
useless to the reader of the program.

I suggest the following simple rules:

(1) type expressions appearing in type constraints are supposed to be
type schemes, implicitely quantified as usual. Scope of type variables
is simply delimited by the parens surrounding the type constraint.

(2) a type constraint (e : sigma) is mandatory. It means that sigma IS
a valid type scheme for e, and indeed sigma is the type scheme
associated to e by the compiler. (This implies that sigma is an
instance of the most general type scheme of e.)

This is fairly conservative and easy to implement. For those
interested in details, I elaborate below on the consequences of this
two rules.


(I) What we gain:
=================

-- type constraints have a reliable meaning as type annotations in
programs,
-- polymorphic recursive definitions are easy to type check, if type
(scheme) annotated.

Examples:

let (f : int -> int) = function x -> x;;
Accepted:
--------
 int -> int is a valid type scheme for f (although not the most general one).
 f gets type (scheme) int -> int.

let (f : 'a -> 'b) = function x -> raise Not_found;;
Accepted:
---------
 'a -> 'b is a valid type scheme for f (the most general one).
 f gets type scheme Forall 'a 'b. 'a -> 'b

let (f : 'a -> 'a) = function x -> raise Not_found;;
Accepted:
---------
 'a -> 'a is a valid type scheme for f.
 f gets type scheme Forall 'a. 'a -> 'a

let (f : int -> int) = function x -> raise Not_found;;
Accepted:
---------
 int -> int is a valid type scheme for f.
 f gets type (scheme) int -> int.

let (f : 'a -> 'b) = function x -> x + 1;;
Rejected: 'a -> 'b is not a valid type scheme for f.
---------

let (f : 'a -> 'a) = function x -> x + 1;;
Rejected: 'a -> 'a is not a valid type scheme for f.
---------

The difference between this treatment and the actual semantics of type
annotations in Caml is fairly conservative: all the ``Accepted''
examples are already legal O'Caml programs and type assignments are
exactly the same. On the other hand, the strange ``Rejected''
annotations, that indeed use types that are more general than the
principal type scheme of the program, are now rejected.

(II) What we loose:
===================

As you may have noticed this new semantics precludes the sharing of
type variables between distinct type annotations. It is not clear to
me that this sharing is needed or really useful or desirable. Anyway,
this sharing is now impossible due to the new scope rule of type
variables, and to the type scheme interpretation of type annotations.
For instance, if we write:

let f (x : 'a) (y : 'a) = ...

meaning (according to the old semantics) that x and y should have the
same type, this is now rejected, since neither x nor y can be assigned
the polymorphic type scheme Forall 'a. 'a.

If we really need this sharing semantics we can use a
conservative extension of the basic scheme above, as follows:

(III) Extension to free type variables:
=======================================

To express type sharing between expressions, we must be able to express
constraints involving types with free type variables (not quantified
in any type scheme): we already have a notation to express those type
variables, namely '_a:

let f (x : '_a) (y : '_a) = x + y;;

Now the constraint is not quantified: it simply means that x and y should
have the same type (more precisely, it exists a type ty such that x :
ty and y : ty).

(The scope of these free type variables should be global to the phrase they
appear into and they can be assigned any type).

Pierre Weis

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

PS: We may also consider explicit Forall quantification in type
schemes. This is less conservative than this proposal but is
definitively clearer (furthermore, we get rid of this strange '_a
notation). Anyway, we may think we should have to introduce this
explicit quantification to support future extensions of the type
system to inner quantification; so it simpler to wait for these
extensions to introduce explicit quantification.

Re: polymorphic recursion

[Xavier Leroy]

[On the scope and binding location of type variables in type constraints:]

> This has already been solved in the SML standard and even if it is not 
> necessarily easy to understand when formalized, this is quite intuitive :

[SML'90 rule snipped]

Actually, SML'97 adds explicit scoping of type variables if desired.
The syntax is something like

        let 'a val x = ...

(This is from memory, I don't have the '97 Definition here.)
Although those declarations are optional and the old rule is used
if they are omitted, it shows that maybe the old rule is a little too
subtle to be understood by all.

IT is amusing to notice that SML, Caml and Haskell implement three
different semantics for type variables in constraints:
  - SML: bind at "let" enclosing all mentions of the variable
  - Caml: bind at nearest "struct ... let x = ... end";
  - Haskell: bind immediately in type expression itself (I think).

This is one of those little dark spots in ML-style languages that I
hope will be cleaned some day by drastic simplifications (as the
problem with polymorphic refs was drastically simplified by the value
restriction).  (Argumented) suggestions are welcome.

- Xavier Leroy

Re: polymorphic recursion

[Pierre Weis]

> right, but there is no polymorphic recursion in Ocaml, is there?

As mentioned earlier there is some form of polymorphic recursion in
objects. A (limited form of) polymorphic recursion could be added to
the core language in the future if we find a simple way to do so.

> > We may need explicit Forall keywords to express type schemes in constraints.
> 
> Indeed, this is a problem. Standard ML solves this by defining some
> explicit rules for free type variables (section 4.6 of the definition -
> p18).

As far as I know this rules do not allow the simple expression of polymorphic
type scheme in type constraints, since you have to figure out which
type variables are quantified and where they are bound (as far as I
remember this quantification implicitely occurs at the outermost level
of the construct where the type variable appears ?). Explicit
quantification would be simple and more explicit.

Pierre Weis

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

Re: polymorphic recursion

[Pierre CREGUT - FT.BD/CNET/DTL/MSV]

Quoting Pierre Weis (Pierre.Weis@inria.fr):
> > This might be the case for OCaml, but note that SML97 disallows more
> > general type-constraints than the type apparent in the expression without
> > the constraint (cf. rule (9) and comment in the 97 Definition - p22) 
> 
> That's a good point. It's simple to state and understand.
This way of handling type constraints is inherited from Hope.

[...]
> Another problem is the scope of type variables in type
> constraints. What's the meaning of
> 
> let f (x : 'a) (y : 'a) = y;;
> 
> We may need explicit Forall keywords to express type schemes in constraints.
[...]

This has already been solved in the SML standard and even if it is not 
necessarily easy to understand when formalized, this is quite intuitive :

  First un occurrence of 'a in a value declaration [val valbind] is said to
  be unguarded if the occurrence is not part of a smaller value declaration
  within [valbind]. In this case we say that 'a occurs unguarded in the value
  declaration. 

  Then we say that 'a is scoped at a particular occurrence O of [val valbind]
  in a  program if (1) 'a occurs unguarded in this value declaration, and (2)
   'a does not occur unguarded in any larger value declaration containing
  the occurrence O.

			Old Definition of Standard ML p 20

According to this definition, the 'a's denote the same type variable in
your example.

let g (x : 'a) = let f (x:'a) = x in x
let h (x : 'a) = x

is equivalent to 

let g (x : 'a) = let f (x:'a) = x in x
let h (x : 'b) = x

but not to 

let g (x : 'a) = let f (x:'c) = x in x
let h (x : 'b) = x

The only risk of this solution is that you overconstrain an expression 
because one of your type variable got caught in the scope of another unrelated
variable and then you get stuck with your compiler complaining about
a constraint it cannot fulfill. This is a safe risk.

-- 
Pierre Cregut - pierre.cregut@cnet.francetelecom.fr - +33 2 96 05 16 28
FT.CNET - DTL/MSV - 2 avenue Pierre Marzin - 22307 Lannion Cedex - France

Re: polymorphic recursion

[Simon Helsen]

> > I don't know why Caml allows more general type constraints, but it might
> > be a good idea to follow SML on this matter (and I am interested to know
> > if there are good reasons for not doing this)
> 
> If we use it to get polymorphic recursion, there is a good reason to
> do this.

right, but there is no polymorphic recursion in Ocaml, is there?

> Another problem is the scope of type variables in type
> constraints. What's the meaning of
> 
> let f (x : 'a) (y : 'a) = y;;
> 
> We may need explicit Forall keywords to express type schemes in constraints.

Indeed, this is a problem. Standard ML solves this by defining some
explicit rules for free type variables (section 4.6 of the definition -
p18) But, admitted, it's ugly and difficult. It would probably be better
to forbid free variables in type constraints altogether.

	Simon

----------------------- Simon Helsen ------------------------ 
--       Wilhelm-Schickard-Institut fuer Informatik        --
--           Arbeitsbereich Programmierung (PU)            --
--            Universitaet Tuebingen, Germany              --
-------------------------------------------------------------
-- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

Re: polymorphic recursion

[Pierre Weis]

> This might be the case for OCaml, but note that SML97 disallows more
> general type-constraints than the type apparent in the expression without
> the constraint (cf. rule (9) and comment in the 97 Definition - p22) 

That's a good point. It's simple to state and understand.

> This makes sense in the filosophy that type constraints are only supposed
> to be programmer documentation or to help the type-inference engine to
> detect type-errors "earlier" (the latter is practical while debugging
> type-errors).

Yes, but furthermore it can be used to help the typechecker to find
types more general than it will normally find.

> Unfortunately, SML is not very consistent on this matter as well, since it
> might require type annotations to succeed its type inference (e.g. at
> top-level monomorphism and the resolution of variable record patterns) A
> SML type-constraint cannot be more general, but is allowed to be more
> specific. e.g:
> 
> - val (f : 'a -> 'a -> 'a) = fn x => fn y => y;
> val f = fn : 'a -> 'a -> 'a

This is necessary to ``constrain'' the types of programs, when you
want to obtain a type more specific than the one synthetized by
the typechecker, in order to get more precise typing
verifications. This is also useful to get rid of spurious type
unknowns at modules boundaries, since you cannot let them escape from
the module.

> And if SML "would" follow this filosophy properly, there is no room for
> polymorphic recursion in general since, as you indicate, type-inference
> for this is undecidable. 

Yes polymorphic recursion type-inference is undecidable.
No, ``exact'' type constraints do not preclude polymorphic recursion.

Starting with the ``exact'' type annotation as hypothesis, it is easy
to verify that the polymorphic recursion is sound. This is simple and
easy. The only drawback is that you have to find the type yourself,
and that you may indicate a too specific type.

> I don't know why Caml allows more general type constraints, but it might
> be a good idea to follow SML on this matter (and I am interested to know
> if there are good reasons for not doing this)

If we use it to get polymorphic recursion, there is a good reason to
do this.

Another problem is the scope of type variables in type
constraints. What's the meaning of

let f (x : 'a) (y : 'a) = y;;

We may need explicit Forall keywords to express type schemes in constraints.

Pierre Weis

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

Re: polymorphic recursion

[Simon Helsen]

> Unfortunately, the problem here is the semantics of type constraints
> in ML: type constraints are not mandatory type assigment declarations,
> but just annotations which should be compatible with the type infered
> for the given expression. This means that a type constraint has to be
> more general than the principal type of the annotated expression. For

This might be the case for OCaml, but note that SML97 disallows more
general type-constraints than the type apparent in the expression without
the constraint (cf. rule (9) and comment in the 97 Definition - p22) 

> let (f : 'a -> int) = function x -> x + 1;;
> val f : int -> int = <fun>

in SML/NJ 110 this yields:

- val (f : 'a -> int) = fn x => x + 1;
stdIn:1.1-2.31 Error: pattern and expression in val dec don't agree
[literal]
  pattern:    'a -> int
  expression:    int -> int
  in declaration:
    f : 'a -> int = (fn x => x + 1)

> This has many drawbacks, the most important being that no type
> annotation in a program is reliable to the reader (except if the type
> annotation does not posses any type variable at all).

I suppose that this is exactly why Standard ML wants the type annotation
to have the exact degree of polymorphism as present in the expression. 

This makes sense in the filosophy that type constraints are only supposed
to be programmer documentation or to help the type-inference engine to
detect type-errors "earlier" (the latter is practical while debugging
type-errors).

Unfortunately, SML is not very consistent on this matter as well, since it
might require type annotations to succeed its type inference (e.g. at
top-level monomorphism and the resolution of variable record patterns) A
SML type-constraint cannot be more general, but is allowed to be more
specific. e.g:

- val (f : 'a -> 'a -> 'a) = fn x => fn y => y;
val f = fn : 'a -> 'a -> 'a

And if SML "would" follow this filosophy properly, there is no room for
polymorphic recursion in general since, as you indicate, type-inference
for this is undecidable. 

I don't know why Caml allows more general type constraints, but it might
be a good idea to follow SML on this matter (and I am interested to know
if there are good reasons for not doing this)

	Simon

----------------------- Simon Helsen ------------------------ 
--       Wilhelm-Schickard-Institut fuer Informatik        --
--           Arbeitsbereich Programmierung (PU)            --
--            Universitaet Tuebingen, Germany              --
-------------------------------------------------------------
-- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

Re: polymorphic recursion

[Pierre Weis]

> To my knowledge, there is no direct way to do this. Part of the reason
> is that type signatures have a different role in Haskell and ML: in
[...]
> This does not matter very much in ML, since you explicitely decide
> which functions recurse with which (in Haskell all definitions in a
> module are a priori recursive), and there are only few examples really
> needing polymorphic recursion.

Yes, and for the excellent reason that you cannot use polymorphic
recursion in ML: this way it would be very surprising to find good
examples of its use, since nobody can write programs based on
polymorphic recursion!
 
> To be complete on this point, in Objective Label method calls can be
> polymorphically recursive:
> 
> # class r = object (self)
>     method virtual m : 'a. 'a -> 'a
>     method m x =
>       let q = self#m true in
>       let r = self#m 0 in
>       x
>   end;;
> class r : object method m : 'a. 'a -> 'a end
> 
> Thanks to the mechanisms use for this inference, it would be easy to
> provide polymorphic recursion for functions also, but we go back to
> the ML problem: where do we write the signature ?

Sintactically, it is easy: just the regular type constraint mechanism, writing:

let rec (f : 'a -> 'a) x =
 let q = f true in
 let r = f 0 in
 x;;

Unfortunately, the problem here is the semantics of type constraints
in ML: type constraints are not mandatory type assigment declarations,
but just annotations which should be compatible with the type infered
for the given expression. This means that a type constraint has to be
more general than the principal type of the annotated expression. For
instance, you can write:

let (f : 'a -> int) = function x -> x + 1;;
val f : int -> int = <fun>

Or :

let (f : 'a -> b) = function x -> x + 1;;
val f : int -> int = <fun>

Or even the most puzzling:

let (f : 'a) = function x -> x + 1;;
val f : int -> int = <fun>

This has many drawbacks, the most important being that no type
annotation in a program is reliable to the reader (except if the type
annotation does not posses any type variable at all).

If type constraints were mandatory, then the annotations will easily
give room to polymorphic recursion (the typechecker just acknowledges
the type annotation as the infered type and verifies the remaining
constraints). In my mind mandatory type annotations will be clearer
and more useful than the strange and almost useless semantics we have
now.

Polymorphic recursion via type annotations, while pratical and simple,
is not completely satisfactory: type inference of polymorphic
recursion would be much more in the spirit of ML. Unfortunately, this
problem, well-known as the ``mu-rule'' problem, has been proved
undecidable in general. However, a restricted kind of polymorphic
recursion inference is tractable (via semi-unification for
instance). Once upon a time, there were an old and wise Caml compiler
featuring such a restricted mechanism:

   CAML (sun4) (V3.1) by INRIA Fri Oct  1

#let rec f x =
# let q = f true in
# let r = f 0 in
# x;;
Value f is <fun> : 'a -> 'a

We still like this feature and we are still looking for a
tractable generalisation of this restricted polymorphic recursion
inference to add it to our new and strong compilers. Wait and see!

Pierre Weis

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

Re: polymorphic recursion

[Jacques GARRIGUE]

> In some languages (most notably Haskell and Miranda) it is possible
> to define a function that enjoys polymorphic recursion, i.e., the
> types of its recursive calls may be instances of the type scheme at
> which the function is defined.
> 
> Can you do the same in OCaml? I am aware of the tricks mentioned in
> the FAQ, but I would like to know if there is a cleaner way to do it,
> for example by providing a type signature.

To my knowledge, there is no direct way to do this. Part of the reason
is that type signatures have a different role in Haskell and ML: in
Haskell the type signature appears before its function, and restricts
it explicitely, while in ML you write it in an independent signature
file, which is not known when typing the function itself (signature
matching takes place after the type checking).

This does not matter very much in ML, since you explicitely decide
which functions recurse with which (in Haskell all definitions in a
module are a priori recursive), and there are only few examples really
needing polymorphic recursion.

To be complete on this point, in Objective Label method calls can be
polymorphically recursive:

# class r = object (self)
    method virtual m : 'a. 'a -> 'a
    method m x =
      let q = self#m true in
      let r = self#m 0 in
      x
  end;;
class r : object method m : 'a. 'a -> 'a end

Thanks to the mechanisms use for this inference, it would be easy to
provide polymorphic recursion for functions also, but we go back to
the ML problem: where do we write the signature ?

	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

polymorphic recursion

[Peter J Thiemann]

In some languages (most notably Haskell and Miranda) it is possible
to define a function that enjoys polymorphic recursion, i.e., the
types of its recursive calls may be instances of the type scheme at
which the function is defined.

For example:

let rec f x =
  let q = f true in
  let r = f 0 in
  x;;

is rejected by OCaml, but it is accepted by Haskell by saying

f :: a -> a
f x = let q = f True in
      let r = f 0 in
      x

Question:

Can you do the same in OCaml? I am aware of the tricks mentioned in
the FAQ, but I would like to know if there is a cleaner way to do it,
for example by providing a type signature.

-Peter