[Caml-list] simple typing question

[Caml-list] simple typing question

[Michael Vanier]

I imagine this has been asked and answered before, so I apologize in
advance.

Compare these two functions:

# let f x = List.map (fun y -> y) x ;;
val f : 'a list -> 'a list = <fun>

and

# let f = List.map (fun y -> y) ;;
val f : '_a list -> '_a list = <fun>

Why does the second use the '_a type variable instead of 'a?  I thought
that special type variables only had to do with polymorphic references.
The FAQ states that the latter expression can't be generalized, but I don't
really understand why.

Mike
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Pierre Weis]

> 
> I imagine this has been asked and answered before, so I apologize in
> advance.
> 
> Compare these two functions:
> 
> # let f x = List.map (fun y -> y) x ;;
> val f : 'a list -> 'a list = <fun>
> 
> and
> 
> # let f = List.map (fun y -> y) ;;
> val f : '_a list -> '_a list = <fun>
> 
> Why does the second use the '_a type variable instead of 'a?  I thought
> that special type variables only had to do with polymorphic references.
> The FAQ states that the latter expression can't be generalized, but I don't
> really understand why.
> 
> Mike

This is explained in the FAQ of the language either in english

http://pauillac.inria.fr/caml/FAQ/FAQ_EXPERT-eng.html#polymorphisme

ou en français:

http://pauillac.inria.fr/caml/FAQ/FAQ_EXPERT-fra.html#polymorphisme

If you don't understand the explanations, please let me know.

Cordialement,

Pierre Weis

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


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Michael Vanier]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2142 bytes --]

> From: Pierre Weis <pierre.weis@inria.fr>
> Date: Tue, 2 Jul 2002 11:14:58 +0200 (MET DST)
> Cc: caml-list@inria.fr
> Content-Type: text/plain; charset=ISO-8859-1
> 
> > 
> > I imagine this has been asked and answered before, so I apologize in
> > advance.
> > 
> > Compare these two functions:
> > 
> > # let f x = List.map (fun y -> y) x ;;
> > val f : 'a list -> 'a list = <fun>
> > 
> > and
> > 
> > # let f = List.map (fun y -> y) ;;
> > val f : '_a list -> '_a list = <fun>
> > 
> > Why does the second use the '_a type variable instead of 'a?  I thought
> > that special type variables only had to do with polymorphic references.
> > The FAQ states that the latter expression can't be generalized, but I don't
> > really understand why.
> > 
> > Mike
> 
> This is explained in the FAQ of the language either in english
> 
> http://pauillac.inria.fr/caml/FAQ/FAQ_EXPERT-eng.html#polymorphisme
> 
> ou en français:
> 
> http://pauillac.inria.fr/caml/FAQ/FAQ_EXPERT-fra.html#polymorphisme
> 
> If you don't understand the explanations, please let me know.
> 
> Cordialement,
> 
> Pierre Weis
> 
> INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/
> 
> 
> 

I *almost* understand.  I understand the need for restrictions with
polymorphic references.  The stated rule is that for

  let name = expr1 ...

  The type of expr1 is generalized when expr1 is a function, an identifier
  or a constant. Otherwise the identifier name is not polymorphic (type
  variables are not generalized).

And later it's stated that when expr1 is "map (function x -> x)" it's an
application, so it isn't generalized.  However, it's an application that
evaluates to a function, so it seems like it would meet the stated
criteria.  Also, I'm not sure why such a restrictive rule is needed.  If
expr1 doesn't manipulate references, why can't it be generalized?  Sorry to
belabor this.

Mike

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Daniel de Rauglaudre]

Hi,

On Tue, Jul 02, 2002 at 02:49:26AM -0700, Michael Vanier wrote:

> And later it's stated that when expr1 is "map (function x -> x)" it's an
> application, so it isn't generalized.  However, it's an application that
> evaluates to a function, so it seems like it would meet the stated
> criteria.

let r = ref [] in map (function x -> r)

also evaluates to a function.

-- 
Daniel de RAUGLAUDRE
daniel.de_rauglaudre@inria.fr
http://cristal.inria.fr/~ddr/
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Xavier Leroy]

> I *almost* understand.  I understand the need for restrictions with
> polymorphic references.  The stated rule is that for
> 
>   let name = expr1 ...
> 
>   The type of expr1 is generalized when expr1 is a function, an identifier
>   or a constant. Otherwise the identifier name is not polymorphic (type
>   variables are not generalized).
> 
> And later it's stated that when expr1 is "map (function x -> x)" it's an
> application, so it isn't generalized.  However, it's an application that
> evaluates to a function, so it seems like it would meet the stated
> criteria.

No, it doesn't.  There is a major difference between a literal
function "fun x -> ..." and an expression that evaluates to a
function.  The latter can create and hide polymorphic references, as
shown below.

> Also, I'm not sure why such a restrictive rule is needed.  If
> expr1 doesn't manipulate references, why can't it be generalized?

Because very similar expressions do manipulate references.  In
particular, consider that a (polymorphic) function can "hide" a
(polymorphic) reference.  For instance:

# let make_toggle () =
    let r = ref [] in fun x -> let old = !r in r := x; old
val make_toggle : unit -> 'a -> 'a list = <fun>

The result of make_toggle() is a function with type _a list -> _a list
that returns the argument that it received the last time it was called.

# let f = make_toggle();;
val f : '_a list -> '_a list = <fun>

# f [1;2;3];;
- : int list = []
# f [4;5;6];;
- : int list = [1; 2; 3]

Now, consider what happens if we were to generalize '_a in the type of f:

# let f = make_toggle();;
val f : 'a list -> 'a list = <fun>

# f [1;2;3];;
- : int list = []
# f ["hello"; "world"];;
- : string list = [1; 2; 3]    <--- crash! (wrong value for the type)

The gist of this example is that "make_toggle()" looks a lot like
"List.map (fun x -> x)" :  both are function applications that return
a function from '_a list to '_a list.  Yet, one is safe to generalize
and not the other.

No reasonably simple type system can distinguish both examples.  Many
have been proposed -- this was a hot research topic in the 1980-1993
time frame, and I even did my PhD on this very topic -- but none was
found to be really usable in practice.  The value restriction on
polymorphism (i.e. what Caml implements) is far from perfect, but is
the "least bad" of the known solutions.

- Xavier Leroy

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Pierre Weis]

[...]
> I *almost* understand.  I understand the need for restrictions with
> polymorphic references.  The stated rule is that for
> 
>   let name = expr1 ...
> 
>   The type of expr1 is generalized when expr1 is a function, an identifier
>   or a constant. Otherwise the identifier name is not polymorphic (type
>   variables are not generalized).
> 
> And later it's stated that when expr1 is "map (function x -> x)" it's an
> application, so it isn't generalized.  However, it's an application that
> evaluates to a function, so it seems like it would meet the stated
> criteria.

No, it does not meet the criterium, since this criterium is ``expr1 is
a function, an identifier, or a constant'', which is evidently
syntactical in nature. Note that the words are ``expr1 is'', not
``expr1 seems to be'', ``expr1 could be considered as'', ``expr1 has a
type that is'', or whatever; hence, the criterium is NOT ``when expr1
EVALUATES to a function, an identifier, or a constant''; it could not
be since this modified rule would have no meaning at all (just
consider that no Caml expression can evaluate to an identifier, and
that all Caml expressions evaluate to constants or functions!).

Furthermore, the FAQ explicitely states afterwards that
"map (function x -> x)" is not a function, but an application!

>  Also, I'm not sure why such a restrictive rule is needed.  If
> expr1 doesn't manipulate references, why can't it be generalized?  Sorry to
> belabor this.

You are perfectly right. This rule is not needed.

More generally, you may find a lot of cases where an expression is not
generalized when it could be: you just discovered that the Caml type
system has some limitations. Hence, it is an interesting research
topic to overcome these limitations. In particular, we would be very
interesting at learning a more lenient typing discipline for
references (and more generally mutable values), if you could find a
new one that avoids the need for the drastic restriction we are now
using. It is an interesting (but extremely difficult) subject to look
at.

For a deeper discussion about the necessity for a special rule for let
in presence of mutable values, see for instance:

http://pauillac.inria.fr/~xleroy/publi/polymorphic-assignment.dvi.gz

The paper is rather old and the proposed solution has been abandoned,
but the examples given there, and the discussion about polymorphic
typing of mutable values are still inspiring, I think.

Best regards,

Pierre Weis

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


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Pixel]

Xavier Leroy <xavier.leroy@inria.fr> writes:

> No reasonably simple type system can distinguish both examples.  Many
> have been proposed -- this was a hot research topic in the 1980-1993
> time frame, and I even did my PhD on this very topic -- but none was
> found to be really usable in practice.  The value restriction on
> polymorphism (i.e. what Caml implements) is far from perfect, but is
> the "least bad" of the known solutions.

what about changing the semantic of partial application, restoring
eta-equivalence: a function is not evaluated unless every arguments
are given:

make_toggle()  <=>  fun x -> make_toggle () x


of course this makes functions like "make_toggle" quite useless:

# let make_toggle () =
    let r = ref [] in fun x -> let old = !r in r := x; old

would be semantically equivalent to

# let make_toggle () x =
    let r = ref [] in let old = !r in r := x; old

To get back the power of "make_toggle"-like functions, a special
function call could be added that would break eta-equivalence:
  call_now(make_toggle, ())
would have the semantic "make_toggle()" has in today's caml.


The rationale for this change would be that "make_toggle"-like
functions are seldom used, whereas "map"-like are used a lot.
Differentiating syntactically them would be nice.

But i don't think such a big change would do caml any good:
- are "make_toggle"-like functions really seldom used?
- performance drawbacks?


(i've been toying around the syntactical pb of partial application:
 http://merd.net/choices_syntax.html)
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Pierre Weis]

> what about changing the semantic of partial application, restoring
> eta-equivalence: a function is not evaluated unless every arguments
> are given:

Could you precisely state this notion ? In the presence of higher
order functions and imperative features, this does not appear to be
simple and evident to me...

(Let alone recursive functions and types as in
$ ocaml -rectypes
        Objective Caml version 3.04+15 (2002-06-18)

# let rec print x = print_int x; print;;
val print : int -> 'a as 'a = <fun>
# print 1 2 3;;
123- : int -> 'a as 'a = <fun>
)

Best regards,

Pierre Weis

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


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Pixel]

Pierre Weis <pierre.weis@inria.fr> writes:

> > what about changing the semantic of partial application, restoring
> > eta-equivalence: a function is not evaluated unless every arguments
> > are given:
> 
> Could you precisely state this notion ? In the presence of higher
> order functions and imperative features, this does not appear to be
> simple and evident to me...

well, wrap every functions:

# let make_toggle_ () =
    let r = ref [] in fun x -> let old = !r in r := x; old

with

# let make_toggle a b = make_toggle_ a b

based on the number of parameters of functions (given by the type).

This disables evaluation of a function until every parameters are
provided.


The program transformation involved is something like:
  let t = foo in fun x -> bar
gives
  fun x -> let t = foo in bar

ie
  (fun t -> (fun x -> bar)) foo
gives
  (fun x -> (fun t -> bar) foo)

> (Let alone recursive functions and types as in
> $ ocaml -rectypes
> # let rec print x = print_int x; print;;
> val print : int -> 'a as 'a = <fun>
> # print 1 2 3;;
> 123- : int -> 'a as 'a = <fun>

of course it doesn't work nicely for this since the "number of
parameters" doesn't mean anything, so you can't know when you can
start evaluating.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Jacques Garrigue]

From: Pixel <pixel@mandrakesoft.com>
> Pierre Weis <pierre.weis@inria.fr> writes:
> > > what about changing the semantic of partial application, restoring
> > > eta-equivalence: a function is not evaluated unless every arguments
> > > are given:
> > 
> > Could you precisely state this notion ? In the presence of higher
> > order functions and imperative features, this does not appear to be
> > simple and evident to me...
> 
> well, wrap every functions:
> 
> # let make_toggle_ () =
>     let r = ref [] in fun x -> let old = !r in r := x; old
> 
> with
> 
> # let make_toggle a b = make_toggle_ a b
> 
> based on the number of parameters of functions (given by the type).
> 
> This disables evaluation of a function until every parameters are
> provided.

Let's make it a bit clearer: what you're asking for is that everything
with a function type should be a value.
This is not completely unreasonable, but changes the semantics in a
not completely intuitive way, and would disallow some nice tricks.
Not completely trivial to implement either: as Pierre pointed out,
some functions returning a polymorphic result have by nature a
variable arity.  One should rewrap every time the arity changes, which
could be costly.

Another problem is that it is asymmetric: partial applications could
be polymorphic, but not results containing several functions:

let both f = (List.map f, List.iter f)

> The program transformation involved is something like:
>   let t = foo in fun x -> bar
> gives
>   fun x -> let t = foo in bar

This one is actually used for default values in optional parameters,
to make them more efficient (hence there should be no side-effects in
defaults).
Note that this rule alone would not be enough to do the needed
transformation:

let toggle r x = let old = !r in r := x; old
let make_toggle () = let r = ref [] in toggle r

You really have to look at the type, which is not very clean.
(Currently the semantics of Caml is completely independent of inferred
types)

So, this seems unlikely such changes would go through.

Without changing the semantics, there are ways to refine the current
typing, but you cannot allow List.map (fun x -> x) to be polymorphic
without giving a special typing to mutable values or side effects
(which has been shown to be a pain in ML).

Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Francois Pottier]

On Wed, Jul 03, 2002 at 02:39:02AM +0200, Pixel wrote:
> 
> based on the number of parameters of functions (given by the type).

There is no such thing as the `number of parameters of a function'
in ML. Consider the following example:
  
  # let apply f x = f x;;
  val apply : ('a -> 'b) -> 'a -> 'b = <fun>
  # apply (fun x -> x) 1;;
  - : int = 1
  # apply (fun x y -> x + y) 1 2;;
  - : int = 3

... and so on. You can write applications of `apply' with any
numbers of arguments. Its type doesn't help, because it ends
with a quantified type variable 'b, which can be instantiated
with an arrow type of arbitrary length.

Besides, your restriction amounts to preventing functions from returning
functions, which doesn't make much sense in a functional language, in my
opinion. Jacques has given other arguments.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Pixel]

Francois Pottier <francois.pottier@inria.fr> writes:

> On Wed, Jul 03, 2002 at 02:39:02AM +0200, Pixel wrote:
> > 
> > based on the number of parameters of functions (given by the type).
> 
> There is no such thing as the `number of parameters of a function'
> in ML. Consider the following example:
>   
>   # let apply f x = f x;;
>   val apply : ('a -> 'b) -> 'a -> 'b = <fun>
>   # apply (fun x -> x) 1;;
>   - : int = 1
>   # apply (fun x y -> x + y) 1 2;;
>   - : int = 3
> 
> ... and so on. You can write applications of `apply' with any
> numbers of arguments.

you're right... but this isn't a problem for the stuff i'm talking.

If "wrapping-restoring-eta-equivalence" is done based on the number of
parameters *before* instanciation of type variables, it will do.

[...]

> Besides, your restriction amounts to preventing functions from returning
> functions, which doesn't make much sense in a functional language, in my
> opinion.

First of all i don't say it's practical/useful/whatever.

But it doesn't prevent returning functions. It *does* change the
evaluation strategy for functions returning functions. This changes
the semantic:
  in "let f() = let v = foo in fun x -> bar"
- if "foo" doesn't terminate, the semantic is different
- if "foo" has side-effects, the semantic is different
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Lauri Alanko]

On Tue, Jul 02, 2002 at 01:42:26PM +0200, Xavier Leroy wrote:
> No reasonably simple type system can distinguish both examples.

I take it that effect systems don't count as "reasonably simple". :)
Btw, is anyone aware of any work on adding effects as a user-level
typing discipline to ML?


Lauri Alanko
la@iki.fi
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] simple typing question

[Pixel]

Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp> writes:

[...]

> Another problem is that it is asymmetric: partial applications could
> be polymorphic, but not results containing several functions:
> 
> let both f = (List.map f, List.iter f)

sorry, i don't understand that pb.


[...]

> let toggle r x = let old = !r in r := x; old
> let make_toggle () = let r = ref [] in toggle r

or worse:

let make_toggle toggle = let r = ref [] in toggle r

no way to know how many parameters toggle can have, so no easy way to
eta-expand. I think it *can* be done at evaluation time, but I'm not
sure.

so my response to Francois Pottier was wrong:

>> >   # let apply f x = f x;;
>> >   val apply : ('a -> 'b) -> 'a -> 'b = <fun>
>> > 
>> > ... You can write applications of `apply' with any
>> > numbers of arguments.
>> 
>> you're right... but this isn't a problem for the stuff i'm talking.
>> 
>> If "wrapping-restoring-eta-equivalence" is done based on the number of
>> parameters *before* instanciation of type variables, it will do.

which was wrong: (even if Francois didn't bother telling :)

# let id f = print_string "foo" ; f

no simple way to eta-expand. Once again, I think it *can* be done at
evaluation time...

[...]

> So, this seems unlikely such changes would go through.

i'm aware of this :)


I wanted to note that partial application semantic is somewhat nasty
when combined with eager evaluation, and that syntactically &
typefully separating functions-returning-functions and
partially-applied-functions could ease understanding.

One way to do this is to add sugar for partial application of tuples,
and having tuples the *default* way of passing parameters.
(once again http://merd.net/choices_syntax.html :)


Thanks!
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners