Type from local module would escape its scope?

Type from local module would escape its scope?

[Bruno De Fraine]

Hello list,

I don't quite understand this behavior regarding local modules (in  
OCaml 3.09.2):

The following is accepted:

module type FOO =
sig
   type t
   val value : t
end ;;

let foo () =
   let module Foo : FOO =
   struct
     type t = int
     let value = 1
   end in
   ignore Foo.value
;;

While the following is rejected:

let foo (ignore: 'a -> unit) =
   let module Foo : FOO =
   struct
     type t = int
     let value = 1
   end in
   ignore Foo.value
;;

With an error on the expression "Foo.value" stating that "The type  
constructor Foo.t would escape its scope". Reading about the typical  
case for this error message in http://caml.inria.fr/pub/ml-archives/ 
caml-list/2002/10/0cf087feab3ef8dc5ccba5a8592472fb.en.html didn't  
really help me. Why does it make a difference whether ignore is an  
argument?

Thanks,
Bruno

Re: [Caml-list] Type from local module would escape its scope?

[Jonathan Roewen]

> The following is accepted:
>
> module type FOO =
> sig
>   type t
>   val value : t
> end ;;
>
> let foo () =
>   let module Foo : FOO =
>   struct
>     type t = int
>     let value = 1
>   end in
>   ignore Foo.value
> ;;
>
> While the following is rejected:
>
> let foo (ignore: 'a -> unit) =
>   let module Foo : FOO =
>   struct
>     type t = int
>     let value = 1
>   end in
>   ignore Foo.value
> ;;
>
> With an error on the expression "Foo.value" stating that "The type
> constructor Foo.t would escape its scope". Reading about the typical
> case for this error message in http://caml.inria.fr/pub/ml-archives/
> caml-list/2002/10/0cf087feab3ef8dc5ccba5a8592472fb.en.html didn't
> really help me. Why does it make a difference whether ignore is an
> argument?

Because the type isn't visible (ignore returns unit, not Foo.t).

Jonathan

Re: [Caml-list] Type from local module would escape its scope?

[Jean-Marie Gaillourdet]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hello,

On 03.07.2006, at 15:19, Bruno De Fraine wrote:
> While the following is rejected:
>
> let foo (ignore: 'a -> unit) =
>   let module Foo : FOO =
>   struct
>     type t = int
>     let value = 1
>   end in
>   ignore Foo.value
> ;;
>
> With an error on the expression "Foo.value" stating that "The type  
> constructor Foo.t would escape its scope". Reading about the  
> typical case for this error message in http://caml.inria.fr/pub/ml- 
> archives/caml-list/2002/10/0cf087feab3ef8dc5ccba5a8592472fb.en.html  
> didn't really help me. Why does it make a difference whether ignore  
> is an argument?

Let us extend your example with the following code:

> let foo (ignore: 'a -> unit) =
>   let module Foo : FOO =
>   struct
>     type t = int
>     let value = 1
>   end in
>   ignore Foo.value

> ;;

let bar (ignore: 'b -> unit) =
   let module Foo : FOO =
   struct
     type t = float
     let value = 1.0
   end in
   ignore Foo.value

let baz () =
   let x = ignore in begin
     foo x;
     bar x
   end

Which type should x have?

Best Regards,
   Jean-Marie

PS: didn't compile that code

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.1 (Darwin)

iD8DBQFEqR28NIUNP/I5YOgRAoRcAKDKWlxVFBKYfdmBvPJ/T2LYrwKu+ACfYJnK
LUIeev+RCMoifUFF5ZNJVK0=
=mEs/
-----END PGP SIGNATURE-----

Re: [Caml-list] Type from local module would escape its scope?

[Alain Frisch]

Bruno De Fraine wrote:
> While the following is rejected:
> 
> let foo (ignore: 'a -> unit) =
>   let module Foo : FOO =
>   struct
>     type t = int
>     let value = 1
>   end in
>   ignore Foo.value
> ;;

The 'a variable is existential and it must be instantiated (because
functional arguments are used monomorphically). Clearly, it will be
unified with Foo.t, which is abstract, and so the type for foo, if it
were well-typed, would be:

val foo: (Foo.t -> unit) -> unit

Foo.t would escape its scope, which is not ok.

-- Alain

Re: [Caml-list] Type from local module would escape its scope?

[Virgile Prevosto]

Le lun 03 jui 2006 15:19:35 CEST,
Bruno De Fraine <Bruno.De.Fraine@vub.ac.be> a écrit :

> module type FOO =
> sig
>    type t
>    val value : t
> end ;;
> let foo (ignore: 'a -> unit) =
>    let module Foo : FOO =
>    struct
>      type t = int
>      let value = 1
>    end in
>    ignore Foo.value
> ;;
> 
> With an error on the expression "Foo.value" stating that "The type  
> constructor Foo.t would escape its scope". Reading about the typical  
> case for this error message in http://caml.inria.fr/pub/ml-archives/ 
> caml-list/2002/10/0cf087feab3ef8dc5ccba5a8592472fb.en.html didn't  
> really help me. Why does it make a difference whether ignore is an  
> argument?
> 

Because "'a -> unit" does not mean the same thing in both cases. In the
case of Pervasives.ignore, it is a type scheme which denotes all the
types you can obtain by instantiating 'a. On the contrary, when used as
a type annotation to your argument, "'a -> unit" only tells ocaml that
there exists an 'a such that the argument ignore has this type: you can
see that with the following code:

# let foo (ignore: 'a -> unit) = ignore 1;;
val foo : (int -> unit) -> unit = <fun>

where 'a is instantiated by int in the inferred type.

IIRC arguments can not have a generalized type of the form
"forall 'a, 'a -> unit", but methods and record fields support such
types: for instance, you can have:

# module type FOO =
sig
   type t
   val value : t
end ;;
        module type FOO = sig type t val value : t end
# let foo (ignore: <call: 'a.'a -> unit>) =
  let module Foo: FOO = struct type t = int let value = 1 end in
  ignore#call Foo.value;;
val foo : < call : 'a. 'a -> unit > -> unit = <fun>

-- 
E tutto per oggi, a la prossima volta.
Virgile

Re: [Caml-list] Type from local module would escape its scope?

[skaller]

On Mon, 2006-07-03 at 15:51 +0200, Virgile Prevosto wrote:

> Because "'a -> unit" does not mean the same thing in both cases. In the
> case of Pervasives.ignore, it is a type scheme 

[]

> IIRC arguments can not have a generalized type of the form
> "forall 'a, 'a -> unit", but methods and record fields support such
> types

Nice explanation! Interesting comparison of
type schema vs. type variables.

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

Re: [Caml-list] Type from local module would escape its scope?

[Bruno De Fraine]

On 03 Jul 2006, at 15:51, Virgile Prevosto wrote:
> IIRC arguments can not have a generalized type of the form
> "forall 'a, 'a -> unit", but methods and record fields support such
> types: for instance, you can have:

Thanks for your explanations! To get closer to the problem that  
caused me to investigate the error: so there is no way to make f1  
into an argument in the following function iter_uniques (other than  
as a method or record field)?

let f1 add empty = List.fold_right add ["foo"; "bar"; "bar"] empty ;;
let f2 = print_endline ;;

let iter_uniques comparison_fun =
   let module StringSet =
   Set.Make(struct
     type t = string
     let compare = comparison_fun
   end) in StringSet.iter f2 (f1 StringSet.add StringSet.empty)
;;

Because in case I didn't require a dynamic comparison function, I  
would simply write:

module StringSet = Set.Make(String) ;;

let iter_uniques f1 f2 =
   StringSet.iter f2 (f1 StringSet.add StringSet.empty)
;;

Regards,
Bruno

Re: [Caml-list] Type from local module would escape its scope?

[Jonathan Roewen]

> Thanks for your explanations! To get closer to the problem that
> caused me to investigate the error: so there is no way to make f1
> into an argument in the following function iter_uniques (other than
> as a method or record field)?
>
> let f1 add empty = List.fold_right add ["foo"; "bar"; "bar"] empty ;;
> let f2 = print_endline ;;
>
> let iter_uniques comparison_fun =
>   let module StringSet =
>   Set.Make(struct
>     type t = string
>     let compare = comparison_fun
>   end) in StringSet.iter f2 (f1 StringSet.add StringSet.empty)
> ;;

Hmm, you could use a ref (which yes, is a record type).

let dyn_comparer = ref compare
let dyn_compare a b = !dyn_comparer a b

module SS = Set.Make(struct type t = string let compare = dyn_compare end);;

let iter_uniques f1 f2 = SS.iter f2 (f1 SS.add SS.empty);;

Petty complaint (Was Re: [Caml-list] Type from local module would escape its )scope?

[brogoff]

On Mon, 3 Jul 2006, Virgile Prevosto wrote:
> IIRC arguments can not have a generalized type of the form
> "forall 'a, 'a -> unit", but methods and record fields support such
> types: for instance, you can have:

It makes me wonder, if OCaml is to be a functional language, why
functions are second class citizens of the language with regards
to typing? By various encodings you can get this higher rank
polymorphism, it's been there for years, but we can't write the function
directly. Is it because we'd have to write it's type?

-- Brian

Re: Petty complaint (Was Re: [Caml-list] Type from local module would escape its )scope?

[Etienne Miret]

Le 3 juil. 06 à 19:30, brogoff a écrit :

> On Mon, 3 Jul 2006, Virgile Prevosto wrote:
>> IIRC arguments can not have a generalized type of the form
>> "forall 'a, 'a -> unit", but methods and record fields support such
>> types: for instance, you can have:
>
> It makes me wonder, if OCaml is to be a functional language, why
> functions are second class citizens of the language with regards
> to typing? By various encodings you can get this higher rank
> polymorphism, it's been there for years, but we can't write the  
> function
> directly. Is it because we'd have to write it's type?
>
> -- Brian

It is because you would be using another type system, called "system F",
wich is much stronger, but infortunately not decidable.

Still, D. Le Botlan and D. Rémy have made a Caml extension
that allow this, but you need to add explicit anotations, as you
have guessed. See http://cristal.inria.fr/~lebotlan/mlf/mlf.html

Etienne

Re: Petty complaint (Was Re: [Caml-list] Type from local module would escape its )scope?

[Boris Yakobowski]

On Mon, Jul 03, 2006 at 10:30:38AM -0700, brogoff wrote:
> It makes me wonder, if OCaml is to be a functional language, why
> functions are second class citizens of the language with regards
> to typing? By various encodings you can get this higher rank
> polymorphism, it's been there for years, but we can't write the function
> directly. Is it because we'd have to write it's type?

As Étienne Miret mentionned, what you're basically asking for is the
expressivity of System F. Unfortunately, type inference in that system is
undecidable, and its practicality as a programming langage is more than
doubtful. Below is the map function on lists in an hypothetical F-based
language. Notice that map must be fully annotated, incuding type
abstractions and type applications; this is why the recursive call is map A
B f q instead of map f q in ML.

let rec map : forall A B. (A -> B) -> A list -> B list =
 fun A B (l : list A) -> match l with
   | [] -> []
   | cons h q  -> cons B (f h) (map A B f q)

Numerous attempts at finding intermediary langages which would require less
annotations exist. However, few of them have found their ways in mainstream
programming languages. In fact, the only practical system I'm aware of is an
extension of Haskell which can be found in Ghc ; see
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#universal-quantification
for some examples. Annotations are quite light : you only need to annotate
functions which have an F type (ML types are infered as usual).

The only problem with this approach is that the system used is predicative:
polymorphic instantiation is limited to simple types. Given a function with
type forall A. \sigma -> \sigma', it can only be applied with a type t which
is a monotype. For example, given the function app defined by app f x = f x,
it is not always the case that app f x is typable, even if f x is. Hence,
the system can sometimes lack compositionnality.
Also, it is not possible to write lists of polymorphic functions without
encapsulating the element inside polymorphic variants or records; this is
similar to the current situation in OCaml.


MLF is another attempt at taming the power of system F. The amount of type
annotations is similar to the one required for the GHC extension:
annotations on arguments which are used really polymorphically. On the plus
side, MLF is impredicative, hence more expressive; in particular, none of
the problems I mentionned above occur. Unfortunately, there are some
downsides. Types of MLF are less readable than those of System F, although
some solutions to mitigate this problem exist. Also, it was not obvious that
the algorithms for type inference in MLF would scale to large-scale
programs; this is on the verge of being resolved.

More problematic is the fact that MLF does not yet support recursive types.
Hence, adding it in OCaml would mean it would not be usable with objects, in
which higher-order polymorphism is often useful. More generally, adding a
new type feature to the OCaml compiler requires understanding its
interactions with the myriad of existing extensions (objects, polymorphic
variants, optional arguments, boxed polymorphism...), a non-trivial task.

-- 
Boris