Weak types ?

Weak types ?

[Pierre CASTERAN]

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



 Hello, all.

 I suppose the following problem concerns "weak" types, but i don't see
 the reason (I have no assignment at all in this definitions !)

let toto =
  let id x = x
  in id id;;
(*
 val toto : '_a -> '_a = <fun>
             ^      ^

             why not " 'a " ?  
             
*)

toto 5;;
(* ok *)

toto (fun z -> z);;

(*
This expression has type 'a -> 'a but is here used with type int
*)

If i  remember Xavier's works, the "weak" types were necessary for
dealing with references, continuations/exceptions, and i/o streams,....

What's the problem with these gentle purely functional top-level 
definitions  ?



Pre Scriptum :

 I (still )  work with Objective Caml version 1.03

-- 
Pierre Casteran,

LaBRI, Universite Bordeaux-I      |    12 place Puy Paulin
351 Cours de la Liberation        |    33000 Bordeaux
F-33405 TALENCE Cedex             |    France
France                            |    (+ 33) 5 56 81 15 80
tel : (+ 33) 5 56 84 69 31
fax : (+ 33) 5 56 84 66 69
email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white space)
www: http://dept-info.labri.u-bordeaux.fr/~casteran

"Combien de petites violences la verité et l'analyse  subissent-elles 
quotidiennement dans le silence de nos pensées engourdies ?"

[Serge Halimi, in "Les nouveaux chiens de garde" (Liber, ed.)]

Re: Weak types ?

[Simon Helsen]

>  I suppose the following problem concerns "weak" types, but i don't see
>  the reason (I have no assignment at all in this definitions !)
> 
> let toto =
>   let id x = x
>   in id id;;
> (*
>  val toto : '_a -> '_a = <fun>
>              ^      ^
> 
>              why not " 'a " ?  
>              
> *)

the problem is due to the polymorphic application (id id). Caml uses
something which is called "value polymorphism", a restriction which is
also adopted in SML'97, although Caml still allows you to use this
pseudo-polymorphic function (i.e. it allows you to instantiate the
poly-variable once and then fixing it). It has absolutely nothing to do
with the use of assignments or anything alike. As far as I know, a
variable (e.g. toto) can only be given a (true) polymorphic type scheme if
the exp (e.g. id id) is "non-expansive" (Standard ML terminology).
However, every application *is* expansive. This is just a syntactic
restriction which definitely avoids the known problems with polymorphic
references, but is indeed sometimes a bit to restrictive, although it
appears to be rarely a problem in practice. This scheme is now also
adopted in SML because other more semantic based approaches (like tracing
references etc.) turned out to be ugly and could mess up the signatures of
modules.

> toto 5;;
> (* ok *)
> 
> toto (fun z -> z);;
> 
> (*
> This expression has type 'a -> 'a but is here used with type int
> *)

Exactly. The pseudo-poly var. has been already instantiated with an
integer and is now fixed to that, meaning it can't be used otherwise. This
exactly avoids the type-problems in case of references. Note that in SML
your definition of toto would be refused in the first place.

cheers,

Simon

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

Re: Weak types ?

[Juan J. Quintela]

Pierre CASTERAN <Pierre.Casteran@labri.u-bordeaux.fr> wrote:

> let toto =
>   let id x = x
>   in id id;;
> (*
>  val toto : '_a -> '_a = <fun>
>              ^      ^
> 
>              why not " 'a " ?  
>              
> *)

Hi,
	I really dont remember the reason, but I remember one solution,
to put explicity the varibles in the binbidng, i. e.:

# let toto y = 
    let id x = x
    in (id id) y;;
val toto : 'a -> 'a = <fun>

Now it works with the normal values:

# toto 5;;
- : int = 5
# toto true;;
- : bool = true

But the identity function returns again the extrange type variables:
# toto (fun z -> z);;
- : '_a -> '_a = <fun>


You can solve this again using the same technique:

# let f y = (toto (fun z -> z)) y;;
val f : 'a -> 'a = <fun>

 
I remember some mail (I think in this list) about this matter. It turs
to be problem with the eta reduction but I don't remind the details, I
remember the solution, to put the varibles in the bindings.

I hope this helps.

Cheers, Juan.

PS. Someone knows the details for this behaviour?

Re: Weak types ?

[Pierre Weis]

>  I suppose the following problem concerns "weak" types, but i don't see
>  the reason (I have no assignment at all in this definitions !)

This is an excerpt from the ``expert'' part of the Caml FAQ

that explains the problem, its solution in Caml, and why it is considered a
good solution.

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

You could read it in french as well in the FAQ, at URL:

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

How to introduce polymorphism ?
Polymorphism appears when we introduce type schemes, that is types
with universally quantified type variables. These type scheme
parameters are denoted by the prefix ' (for instance 'a). All type
scheme parameters are universally quantified at the head of the
schema: so 'a -> 'a means: For all types 'a, 'a -> 'a. This
quantification of type parameters is implicit in Caml:

#map;;
- : ('a -> 'b) -> 'a list -> 'b list = <fun>

The type (schema) of map means For all types 'a, 'b, ('a -> 'b) -> 'a
list -> 'b list.
The polymorphism is only introduced by the definition of names during
a let construct (either local, or global).

The problem and its solution:
The original rule for the local definition 
let name = expr1 in expr2

states that you have to type check expr1 first, then give name a type
scheme (a polymorphic type) according to the type obtained for expr1,
then type-check expr2, taking a copy of the type scheme of name for
each occurrence of name. The schema of name is obtained by finding
type parameters, that is all the type variables that have been
introduced during the type-checking of expr1, and that remain
unconstrained at the end of the type-checking of expr1. For instance:

let id = function x -> x in ...

id gets the type scheme: For all 'a. 'a -> 'a, and can be used with
several incompatible types in the rest of the program, for instance
with types int -> int and bool -> bool, if the in part is id 1; id
true.
Unfortunately this simple rule is not correct in the presence of
mutable values (such as references, arrays, or records with mutable
fields). Consider:

let bad_ref = ref [] in ...

With the original let rule, bad_ref has the type schema ``For all
'a. 'a list ref''. So the reference can be used with different
incompatible types in the rest of the program, which is erroneous
(lists must be homogeneous in Caml). For instance, if you use bad_ref
with types int list ref and bool list ref, then you can write: 

let bad_ref = ref [] in
    bad_ref := [1];
    if hd (!bad_ref) then ...

(bad_ref := [1] is correctly type-checked, since bad_ref can be used
with type int list ref, hd (!bad_ref) is correctly type-checked, since
bad_ref can be used with type type bool list ref. But this program
leads to a fatal error at run-time, since after the assignment,
bad_ref contains an integer list not a boolean list.  

The new rule to define names:
In short, a secure type system for Caml must forbid the existence of
polymorphic mutable values at run-time. This has been extensively
studied, and many complex systems have been proposed. It appears now
that a very simple modification of the original rule is almost
completely satisfactory. When type-checking 

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

Which programs are now monomorphic ?
The new rule implies that if expr1 is a function application, then the
identifier name is monomorphic. For instance

let bad_ref = ref [] in ...

bad_ref is not polymorphic, and that's what we want. In contrast: 
let map_id = map (function x -> x) in ...

Since map_id is defined by an application, its type is not generalized
and map_id cannot be used with several different types. So:

#let map_id = map (function x -> x) in
map_id [1]; map_id [true];;
Toplevel input:
>map_id [1]; map_id [true];;
>                   ^^^^^^
This expression has type bool list,
but is used with type int list.

is ill-typed (the first use of map_id, that is map_id [1] implies that
map_id has type int list -> int list, and map_id [true] is
ill-typed). The next section explains how to get a polymorphic
definition for map_id, and how to get a polymorphic result when a
polymorphic function is partially applied.

My function is not polymorphic (enough) ?

How to allow polymorphic definitions obtained via partial application ?
The more common case to get a ``not polymorphic enough'' definition is
when defining a function via partial application of a general
polymorphic function. In this case, you recover a fully polymorphic
definition by clearly exhibiting the functionality to the
type-checker: define the function with an explicit functional
abstraction, that is, add a function construct or an extra parameter
(this rewriting is known as eta-expansion):

let map_id l = map (function x -> x) l in ...

or alternatively 

let map_id = function l -> map (function x -> x) l in ...

The new definition is semantically equivalent and can be assigned a
polymorphic type scheme, since it is no more a function application.

A type variable starts with _ ?
When an identifier is defined by an expression which cannot be
generalized, the identifier can have a type with unknowns (that is
type variables which cannot be generalized) which will be determined
(that is assigned a type value) by the usage of the identifier in the
rest of the program. These unknown types are special type variables,
prefixed by an underscore (e.g. '_a). Beware, these variables stand
for unknown types to be determined by the type checking process:
that's why these variables may disappear, precisely because their type
value has been discovered.

let map_id = map (function x -> x) in
map_id [1];;

After its definition map_id has type '_a list -> '_a list, where '_a
means some type a. When typing map_id [1] this unknown type gets bound
to int (and map_id has type int list -> int list for the rest of the
program).
This phenomenon appears even more clearly if we break the let in
construct in two phrases:

#let map_id = map (function x -> x);;
map_id : '_a list -> '_a list = <fun>
#map_id [1];;
- : int list = [1]

Now the unknown '_a in the type of map_id is determined, and map_id
has a type without unknowns:

#map_id;;
- : int list -> int list = <fun>

The following section 

My program is not polymorphic (enough)?
Semantically, the definition of an identifier by a let construct is
equivalent to a function application. More exactly, let ident = e1 in
e2 is equivalent to (function ident -> e2) e1. This means that the two
programs produce the same results and the same effects.

However, the two programs are not completely equivalent as far as type
checking is concerned: in effect, the let version may introduce some
polymorphism, while the function application does not, and forces
ident to be completely monomorphic when typing the expression
e2. Thus:

#let id = function x -> x in id id;;
- : '_a -> '_a = <fun>

But: 

#(function id -> id id) (function x -> x);;
Toplevel input:
>(function id -> id id) (function x -> x);;
>                   ^^
This expression has type 'a -> 'b,
but is used with type 'a.

Pierre Weis

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

Re: Weak types ?

[Simon Helsen]

> >  I suppose the following problem concerns "weak" types, but i don't see
> >  the reason (I have no assignment at all in this definitions !)
> 
> This is an excerpt from the ``expert'' part of the Caml FAQ
> 
> that explains the problem, its solution in Caml, and why it is considered a
> good solution.

yes, but it doesn't say much on the history of the problem. The Paulson
book does, but doesn't mention Caml. What I wonder is when Caml
adopted value polymorphism, what system was used before that and whether
the INRIA researchers did seek for (perhaps alternative) solutions
themselves. In the Standard ML community, the standard reference to this
problem is a paper of Andrew Wright (1995)... 

Simon

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

Re: Weak types ?

[Pierre Weis]

> yes, but it doesn't say much on the history of the problem. The Paulson
> book does, but doesn't mention Caml. What I wonder is when Caml
> adopted value polymorphism, what system was used before that and whether
> the INRIA researchers did seek for (perhaps alternative) solutions
> themselves. In the Standard ML community, the standard reference to this
> problem is a paper of Andrew Wright (1995)... 
> 
> Simon
> 
> ----------------------- Simon Helsen ------------------------ 
> --       Wilhelm-Schickard-Institut fuer Informatik        --
> --           Arbeitsbereich Programmierung (PU)            --
> --            Universitaet Tuebingen, Germany              --
> -------------------------------------------------------------
> -- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

I've no time to describe old type systems that have been adopted in
ancient versions of Caml since 1984. Let's just say that they were not
that satisfactory, since we start studying the subject and writing
papers in 1990:

1991:
----
Publications available online
Xavier Leroy, Pierre Weis. "Polymorphic type inference and
assignment". Proceedings POPL 91.

This paper present a new approach to the polymorphic typing of data
accepting in-place modification in ML-like languages. This approach is
based on restrictions over type generalization, and a refined typing
of functions. The type system given here leads to a better integration
of imperative programming style with the purely applicative kernel of
ML. In particular, generic functions that allocate mutable data can
safely be given fully polymorphic types. We show the soundness of this
type system, and give a type reconstruction algorithm.

1992:
-----
Publications available online
Xavier Leroy. "Polymorphic typing of an algorithmic
language". Research report 1778, INRIA, 1992. (PhD thesis. French
original also available.)

The polymorphic type discipline, as in the ML language, fits well
within purely applicative languages, but does not extend naturally to
the main feature of algorithmic languages: in-place update of data
structures. Similar typing difficulties arise with other extensions of
applicative languages: logical variables, communication channels,
continuation handling. This work studies (in the setting of relational
semantics) two new approaches to the polymorphic typing of these
non-applicative features. The first one relies on a restriction of
generalization over types (the notion of dangerous variables), and on
a refined typing of functional values (closure typing). The resulting
type system is compatible with the ML core language, and is the most
expressive type systems for ML with imperative features proposed so
far. The second approach relies on switching to ``by-name'' semantics
for the constructs of polymorphism, instead of the usual ``by-value''
semantics. The resulting language differs from ML, but lends itself
easily to polymorphic typing. Both approaches smoothly integrate
non-applicative features and polymorphic typing.

1993:
-----
Le langage Caml, Pierre Weis et Xavier Leroy, InterEditions, Paris
1993, ISBN 2-7296-0493-6. The restriction of let polymorphism to non
expansive expressions is described in pages 389-390.

1995:
-----
The restriction of polymorphism to non expansive expressions is
implemented in version Caml-Light 0.7.

The paper you cited by Andrew Wright is still a good reference, and he
really has proved that this approach could be feasible for ML-like
languages, whereas we (the Caml team) were looking for an extension of
the ML type-system that would preserve the typing of purely functional
programs. Xavier gets such an extension in his thesis, but the type
system was more complex (and more difficult to implement efficiently)
than the simple ``non expansive'' restriction. Furthermore, this
restriction is easy to understand and trivial to prove correct. Thus
it has been adopted in the Caml compilers.

By the way, there is no ``weak type variables'' in the Caml type
system. The '_a notation denotes pure type variables that have not
been universally quantified in a type scheme. There is no
quantification over these '_a type variables, as opposed to weak type
variables.

Best regards,

Pierre Weis

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