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

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

[Gregory Malecha]

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

Hello --

I've encountered a typing error that I'm not sure how to track down. I
assume that what I'm doing is running up against the limitations of the
type system, so I assume there is some technical detail that I am missing.
Here's my problem:

I have defined the following type:

(* essentially the eliminator for lists *)
type ('a,'b) result_stream =
  ('a -> ('a,'b) result_stream -> 'b) ->
  (unit -> 'b) -> 'b

(* I have the following function, which seems to type check *)
let stream_declarations (type a)
: (internal_result,a) result_stream = ...

(* I am unable to implement this function *)
let generic_search_stream (type b) (glnumopt : int option)
: (internal_result, b) result_stream =
  stream_declarations

Ocaml complains with the following error message:

Error: This expression has type
         (internal_result, b) result_stream =
           (internal_result -> (internal_result, b) result_stream -> b) ->
           (unit -> b) -> b
       but an expression was expected of type
         (internal_result, b) result_stream =
           (internal_result -> (internal_result, b) result_stream -> b) ->
           (unit -> b) -> b
       The type constructor b would escape its scope

Since the types match up exactly, I can only assume that this has something
to do with the type declaration (type b) but I can't see what is wrong. My
expectation is that the scope of [b] ends at the end of the
[generic_search_stream] function and is used as the type parameter to
[stream_declarations], this seems to not be the case though.

Wondering if OCaml requires arguments in order to instantiate polymorphic
functions, I tried to eta-expand the definition as follows:

let generic_search_stream (type b) (glnumopt : int option)
: (internal_result, b) result_stream =
  fun cons nil -> stream_declarations cons nil

With this code, the "error" is with 'cons' and says:

Error: This expression has type
         internal_result -> (internal_result, b) result_stream -> b
       but an expression was expected of type
         internal_result -> (internal_result, b) result_stream -> b
       Type
         (internal_result, b) result_stream =
           (internal_result -> (internal_result, b) result_stream -> b) ->
           (unit -> b) -> b
       is not compatible with type
         (internal_result, b) result_stream =
           (internal_result -> (internal_result, b) result_stream -> b) ->
           (unit -> b) -> b
       The type constructor b would escape its scope

Essentially the same error, but it doesn't seem to lead me to any potential
solutions.

Can someone explain this error to me?

Thanks.

-- 
gregory malecha

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

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

[Leo White]

This is a guess since you didn't include the definition of
stream_declarations, but I suspect that:

> (* I have the following function, which seems to type check *)
> let stream_declarations (type a)
> : (internal_result,a) result_stream = ...

is not polymorphic. The `(type a)` annotation ensures that `a` is
abstract in the body of `stream_declarations` but does not enforce
that the result is polymorphic -- in particular I suspect that you
are running up against the value restriction. An easy way to check
would be to change the definition to:

  let stream_declarations : 'a. (internal_result,'a) result_stream =
  ...

or

  let stream_declarations : type a. (internal_result,a) result_stream =
  ...

both of which enforce polymorphism, and so will give an error if your
definition is actually monomorphic.

If `stream_declarations` does have the monomorphic type
`(internal_result, '_a) result_stream` then any attempt to use it as
`(internal_result, b) result_stream` would cause `b` to be unified with
`'_a` and thus escape it's scope.

Regards,

Leo

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

[Gregory Malecha]

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

Thanks, Leo --

This is exactly what I needed to know. I thought that the (type a)
annotation was forcing the function to be polymorphic. For future
reference, is there any way to write the annotation (that forces the
function to be polymorphic) without having to write explicit 'fun's?

Thanks.

On Sun, Mar 27, 2016 at 12:04 AM, Leo White <leo@lpw25.net> wrote:

> This is a guess since you didn't include the definition of
> stream_declarations, but I suspect that:
>
> > (* I have the following function, which seems to type check *)
> > let stream_declarations (type a)
> > : (internal_result,a) result_stream = ...
>
> is not polymorphic. The `(type a)` annotation ensures that `a` is
> abstract in the body of `stream_declarations` but does not enforce
> that the result is polymorphic -- in particular I suspect that you
> are running up against the value restriction. An easy way to check
> would be to change the definition to:
>
>   let stream_declarations : 'a. (internal_result,'a) result_stream =
>   ...
>
> or
>
>   let stream_declarations : type a. (internal_result,a) result_stream =
>   ...
>
> both of which enforce polymorphism, and so will give an error if your
> definition is actually monomorphic.
>
> If `stream_declarations` does have the monomorphic type
> `(internal_result, '_a) result_stream` then any attempt to use it as
> `(internal_result, b) result_stream` would cause `b` to be unified with
> `'_a` and thus escape it's scope.
>
> Regards,
>
> Leo
>



-- 
gregory malecha

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

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

[Jacques Garrigue]

On 2016/03/28 03:52, Gregory Malecha wrote:
> 
> Thanks, Leo --
> 
> This is exactly what I needed to know. I thought that the (type a) annotation was forcing the function to be polymorphic. For future reference, is there any way to write the annotation (that forces the function to be polymorphic) without having to write explicit ‘fun's?

You should either write

  let generic_search_stream : ‘b. int option -> (internal_result, ‘b) result_stream = …

or
 
  let generic_search_stream : type b. int option -> (internal_result, b) result_stream = …

where the latter one both requires polymorphism and defines a locally abstract type,
i.e. probably the behavior you expect with (type b).

Jacques

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

[Gregory Malecha]

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

Thanks. I'm not sure I understand the difference between the two though. Is
there an example showing when they produce different results?

On Sun, Mar 27, 2016 at 6:12 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

> On 2016/03/28 03:52, Gregory Malecha wrote:
> >
> > Thanks, Leo --
> >
> > This is exactly what I needed to know. I thought that the (type a)
> annotation was forcing the function to be polymorphic. For future
> reference, is there any way to write the annotation (that forces the
> function to be polymorphic) without having to write explicit ‘fun's?
>
> You should either write
>
>   let generic_search_stream : ‘b. int option -> (internal_result, ‘b)
> result_stream = …
>
> or
>
>   let generic_search_stream : type b. int option -> (internal_result, b)
> result_stream = …
>
> where the latter one both requires polymorphism and defines a locally
> abstract type,
> i.e. probably the behavior you expect with (type b).
>
> Jacques
>
>


-- 
gregory malecha

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

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

[Gabriel Scherer]

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

Locally abstract types scope over the definition body where they can
be used as type names or to refine GADTs by pattern-matching.

module type Ty = sig type t end

(* we need the scoping of the locally abstract type in this example;
   note that (type a) would work as well *)
let mkTy : type a . unit -> (module Ty with type t = a) =
  fun () ->
    let module T = struct type t = a end in
    (module T)

> val mkTy : unit -> (module Ty with type t = 'a) = <fun>

(* a type variable 'a only scopes over the type annotation *)
let mkTy : 'a . unit -> (module Ty with type t = 'a) =
  fun () ->
    let module T = struct type t = 'a end in
    (module T)

>  let module T = struct type t = 'a end in
>                                 ^^
> Error: Unbound type parameter 'a


type _ tag = Int : int tag | Prod : 'a tag * 'b tag -> ('a * 'b) tag

(* we need the ability to be refined by GADT matching here *)
let rec default : type a . a tag -> a =
  function
  | Int -> 0
  | Prod (ta, tb) -> (default ta, default tb)

> val default : 'a tag -> 'a = <fun>

(* a type variable just unifies with the first case and fails on the second
*)
let rec default : 'a . 'a tag -> 'a =
  function
  | Int -> 0
  | Prod (ta, tb) -> (default ta, default tb)
>   ^^^^^^^^^^^^^
> Error: This pattern matches values of type ($0 * $1) tag
>        but a pattern was expected which matches values of type int tag
>        Type $0 * $1 is not compatible with type int

(* 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) *)
let rec default (type a) : a tag -> a =
  function
  | Int -> 0
  | Prod (ta, tb) -> (default ta, default tb)
>                             ^^
> Error: This expression has type $0 tag but an expression
> was expected of type 'a
> The type constructor $0 would escape its scope

On Mon, Mar 28, 2016 at 6:20 AM, Gregory Malecha <gmalecha@gmail.com> wrote:
> Thanks. I'm not sure I understand the difference between the two though.
Is
> there an example showing when they produce different results?
>
> On Sun, Mar 27, 2016 at 6:12 PM, Jacques Garrigue
> <garrigue@math.nagoya-u.ac.jp> wrote:
>>
>> On 2016/03/28 03:52, Gregory Malecha wrote:
>> >
>> > Thanks, Leo --
>> >
>> > This is exactly what I needed to know. I thought that the (type a)
>> > annotation was forcing the function to be polymorphic. For future
reference,
>> > is there any way to write the annotation (that forces the function to
be
>> > polymorphic) without having to write explicit ‘fun's?
>>
>> You should either write
>>
>>   let generic_search_stream : ‘b. int option -> (internal_result, ‘b)
>> result_stream = …
>>
>> or
>>
>>   let generic_search_stream : type b. int option -> (internal_result, b)
>> result_stream = …
>>
>> where the latter one both requires polymorphism and defines a locally
>> abstract type,
>> i.e. probably the behavior you expect with (type b).
>>
>> Jacques
>>
>
>
>
> --
> gregory malecha

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

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

[Gregory Malecha]

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

Thanks so much.

On Mon, Mar 28, 2016, 1:08 AM Gabriel Scherer <gabriel.scherer@gmail.com>
wrote:

> Locally abstract types scope over the definition body where they can
> be used as type names or to refine GADTs by pattern-matching.
>
> module type Ty = sig type t end
>
> (* we need the scoping of the locally abstract type in this example;
>    note that (type a) would work as well *)
> let mkTy : type a . unit -> (module Ty with type t = a) =
>   fun () ->
>     let module T = struct type t = a end in
>     (module T)
>
> > val mkTy : unit -> (module Ty with type t = 'a) = <fun>
>
> (* a type variable 'a only scopes over the type annotation *)
> let mkTy : 'a . unit -> (module Ty with type t = 'a) =
>   fun () ->
>     let module T = struct type t = 'a end in
>     (module T)
>
> >  let module T = struct type t = 'a end in
> >                                 ^^
> > Error: Unbound type parameter 'a
>
>
> type _ tag = Int : int tag | Prod : 'a tag * 'b tag -> ('a * 'b) tag
>
> (* we need the ability to be refined by GADT matching here *)
> let rec default : type a . a tag -> a =
>   function
>   | Int -> 0
>   | Prod (ta, tb) -> (default ta, default tb)
>
> > val default : 'a tag -> 'a = <fun>
>
> (* a type variable just unifies with the first case and fails on the
> second *)
> let rec default : 'a . 'a tag -> 'a =
>   function
>   | Int -> 0
>   | Prod (ta, tb) -> (default ta, default tb)
> >   ^^^^^^^^^^^^^
> > Error: This pattern matches values of type ($0 * $1) tag
> >        but a pattern was expected which matches values of type int tag
> >        Type $0 * $1 is not compatible with type int
>
> (* 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) *)
> let rec default (type a) : a tag -> a =
>   function
>   | Int -> 0
>   | Prod (ta, tb) -> (default ta, default tb)
> >                             ^^
> > Error: This expression has type $0 tag but an expression
> > was expected of type 'a
> > The type constructor $0 would escape its scope
>
>
> On Mon, Mar 28, 2016 at 6:20 AM, Gregory Malecha <gmalecha@gmail.com>
> wrote:
> > Thanks. I'm not sure I understand the difference between the two though.
> Is
> > there an example showing when they produce different results?
> >
> > On Sun, Mar 27, 2016 at 6:12 PM, Jacques Garrigue
> > <garrigue@math.nagoya-u.ac.jp> wrote:
> >>
> >> On 2016/03/28 03:52, Gregory Malecha wrote:
> >> >
> >> > Thanks, Leo --
> >> >
> >> > This is exactly what I needed to know. I thought that the (type a)
> >> > annotation was forcing the function to be polymorphic. For future
> reference,
> >> > is there any way to write the annotation (that forces the function to
> be
> >> > polymorphic) without having to write explicit ‘fun's?
> >>
> >> You should either write
> >>
> >>   let generic_search_stream : ‘b. int option -> (internal_result, ‘b)
> >> result_stream = …
> >>
> >> or
> >>
> >>   let generic_search_stream : type b. int option -> (internal_result, b)
> >> result_stream = …
> >>
> >> where the latter one both requires polymorphism and defines a locally
> >> abstract type,
> >> i.e. probably the behavior you expect with (type b).
> >>
> >> Jacques
> >>
> >
> >
> >
> > --
> > gregory malecha
>

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

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

[Arnaud Spiwack]

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

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

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

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

[Leo White]

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

If you don't need the polymorphism provided by `type a.` then `(type a)`
might be slightly preferable because you don't need to fully describe
the type of the value.

For example, if you are writing a function with type `'a -> 'a` then for
the first form you must write:

    let f : type a. a -> a = fun x -> x

you cannot write:

    let f : type a. a -> _ = fun x -> x

whereas with the second form you could write:

    let f (type a) (x : a) = x

which infers the return type as `a` without the need to annotate it.

This also illustrates what is difficult about reliably turning `(type
a)` into `type a. ...`. For the second form you must work out the entire
type involving `a`. Since `type a. ...` is for polymorphic recursion,
you must do this before you properly type-check the body of the
function.

For a simple case, like:

  let f (x : a) : a = x

it is not too bad as you can examine the argument pattern and constraint
to get the full type, but as the patterns and expressions get more
complicated this becomes more difficult, and at some point you are
forced to draw the line and give up. Finding a sensible place to draw
this line, without making inference unpredictable and confusing to
users, is difficult.

Regards,

Leo

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

[Gerd Stolpmann]

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