Re: [Caml-list] "Type constructor b would escape its scope"

[Gerd Stolpmann <info@gerd-stolpmann.de>]

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

Am Montag, den 28.03.2016, 21:20 +0200 schrieb Arnaud Spiwack:
> 
> On 28 March 2016 at 10:07, Gabriel Scherer <gabriel.scherer@gmail.com>
> wrote:
>         (* the difference by "(type a) ..." and "type a . ..." is that
>         the latter
>            allows polymorphic recursion (just as "'a . ..."), so this
>         example fails
>            with just (type a) *)
>         
>  
> 
> So here's a question which has been nagging me for a while: is there
> any occasion where one may prefer to use the `(type a)` or the `'a.`
> forms over the `type a.` (apart for syntactical reasons)? If there is
> I'd be really interested in seeing an example, for I can't come up
> with one (especially for `(type a)`). If there aren't, what are the
> obstacles to turn the `(type a)` syntax into a synonymous to the `type
> a.` syntax? (I'm guessing that the `'a.` variant would be
> significantly harder).

Originally, I thought (type a) is just like plain 'a, only that the
variable appears inside the function as abstract type. At least the
manual suggests that. But looking closer, there are restrictions, and
these make (type a) unattractive. E.g.

# let f (x:'a) : 'a = match x with (p,q) -> (p,q);;       
val f : 'a * 'b -> 'a * 'b = <fun>

but

# let f (type a) (x:a) : a = match x with (p,q) -> (p,q);;
Error: This pattern matches values of type 'a * 'b
       but a pattern was expected which matches values of type a

so you cannot push any constraint to it, as if it was all-quantified.
Given that, the question is really whether there is any application left
that could not also be expressed by "type a.". But maybe I just don't
know? What about regular recursions? Tried to construct something, and I
was hoping that "type a." would force me to add hinting, but to no
avail:

# type 'a mylist = Nil | Cons of 'a * 'a mylist;;
# let rec last (type t) l = match l with Nil -> raise Not_found |
Cons(x,Nil) -> x | Cons(x,l') -> last l';;
val last : 'a mylist -> 'a = <fun>
# let rec last : type t . t mylist -> t = fun l -> match l with Nil ->
raise Not_found | Cons(x,Nil) -> x | Cons(x,l') -> last l';;
val last : 'a mylist -> 'a = <fun>

(Not that this is a good example at all, because it doesn't exploit the
type name t anywhere.)

Gerd

-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]