'_a

'_a

[Mike Hamburg]

The appearance of '_a in places where it shouldn't appear causes some 
annoyance, and a good deal of confusion among beginners to O'Caml.  In 
particular, List.map (fun x -> x) "ought to" have type 'a list -> 'a 
list, whereas it instead has type '_a list -> '_a list.

Some types are treated specially for creation of '_a, such as refs and 
arrays.  For instance, if you have the following two declarations:

# let a = let f x () = [x] in f [];;
val a : unit -> 'a list list = <fun>
# let b = let f x () = [|x|] in f [];;
val b : unit -> '_a list array = <fun>

Although I haven't read the code for O'Caml, I deduce from this that 
there is deep magic in place to determine when to turn 'a into '_a, and 
in many cases, the heuristic is wrong (in the conservative direction: 
in this case, 'a should not be turned into '_a until b is applied).

The cause of the problem is that programs may create a closure with a 
mutable variable of type 'a, which if we were to let 'a generalize 
could be replaced with a subtype 'b of 'a, and then used as another 
subtype 'c of 'a, which would be unsafe.

As a fix, I propose the following: the type system should keep track of 
where a mutable or immutable reference to a polymorphic variable with 
type parameter 'a is created on the stack.  Call these places [m'a] and 
[i'a].  For example, ref should have type 'a -> [m'a] 'a, and ref [] 
should have type [m'a] 'a (which is equivalent to the current '_a).  I 
don't propose that the printing should show this complexity, just as it 
hides whatever heuristic O'Caml is using now, except in the case where 
there is a mutable reference at top level, in which case it should 
convert 'a to '_a.

Of course, module interfaces shouldn't have to show when they keep 
references to things, so we probably can't do much about applying 
List.map to the identity without modifying List (for instance, what if 
List.map decided to memoize the function fed into it using a hash 
table?).

Is this a reasonable idea?  If so, can someone give me a pointer on how 
to go about implementing it (or proving that it is type-safe with 
appropriate unification rules?)?

Mike

Re: [Caml-list] '_a

[Jacques Garrigue]

From: Mike Hamburg <hamburg@fas.harvard.edu>
Subject: [Caml-list] '_a
Date: Wed, 26 Jan 2005 19:19:16 -0500

> The appearance of '_a in places where it shouldn't appear causes some 
> annoyance, and a good deal of confusion among beginners to O'Caml.  In 
> particular, List.map (fun x -> x) "ought to" have type 'a list -> 'a 
> list, whereas it instead has type '_a list -> '_a list.
> 
> Some types are treated specially for creation of '_a, such as refs and 
> arrays.  For instance, if you have the following two declarations:
> 
> # let a = let f x () = [x] in f [];;
> val a : unit -> 'a list list = <fun>
> # let b = let f x () = [|x|] in f [];;
> val b : unit -> '_a list array = <fun>
> 
> Although I haven't read the code for O'Caml, I deduce from this that 
> there is deep magic in place to determine when to turn 'a into '_a, and 
> in many cases, the heuristic is wrong (in the conservative direction: 
> in this case, 'a should not be turned into '_a until b is applied).

There is no deep magic, no heuristics. There is just a type system
which guarantees type soundness (i.e. "well typed programs cannot
produce runtime type errors").

If you want the type system and all the historical details, read my
paper "Relaxing the value restriction" at
  http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/

In a nutshell, ocaml uses an improvement of the value restriction.
With the value restriction, only definitions which are syntactical
values (i.e. that do not call functions, etc when defined) are allowed
to contain polymorphic type variables.
This is improved by allowing covariant type variables to be
generalized in all cases. Your first example is ok, because list is a
covariant type, but your second fails, because array is not (you may
assign to an array, and you would have to look at the code to see that
each call to b creates a different array)

Of course, one could think of many clever tricks by looking
at what the code actually does. The above paper describes some of the
"crazy" things Xavier Leroy and others tried in the past, which
actually subsume your ideas, before they all decided this was too
complicated. The main reason is that, if something is going to break
at module boundaries, then it is not really useful.

Good reading,

Jacques Garrigue

Re: [Caml-list] '_a

[skaller]

On Thu, 2005-01-27 at 11:51, Jacques Garrigue wrote:

> There is no deep magic, no heuristics. There is just a type system
> which guarantees type soundness (i.e. "well typed programs cannot
> produce runtime type errors").

Unfortunately, 'soundness' as described is somewhat weaker
than one would like, since it depends on the expressivity
of the type system how useful soundness actually is.

Ocaml can still produce run time errors for situations
that 'should' have been considered type errors, except
the typing is not strong enough to allow it.

In the extreme, a fully dynamic type system in
which everything has type 'object' has a fully sound
static type system behind it, and there cannot be
any run time 'type' errors in the sense of 
the static type.

For less extreme circumstances, C++ programmers would
express surprise the typing is so weak that array length
is not part of an array type, so that a bounds violation
is technically not a type error in Ocaml whereas in a
language where the length was part of type information
the very same error would indicate unsound typing.

There are in fact quite a few incorrectly typed functions
as well, for example List.hd and List.tl can fail at 
run time, but this isn't considered a type error simply
because the function typing is actually wrong.

Thus, 'soundness' being ensured must be taken with a grain
of salt. The fact that 'well typed programs can't produce
runtime *type* errors' doesn't really tell you as much as
you'd like -- other errors can still occur which aren't
technically type errors, but in a less 'technical' interpretation
certainly are.

Exceptions are part of the evil here, since they permit
blatant uncontrolled lying about type. The 'real' type
of List.hd is

	hd: 'a list -> 'a option

considering it as a total function. The type

	hd: 'a stream -> 'a

is correct but only applies to streams, which lists are not.
An exception free implementation of List.hd would
always produce the correct typing:

	let hd x = function 
	| [] -> None 
	| h :: _ -> Some h

In effect, Ocaml first pretends unsound typing is actually sound,
and then enforces this at run time by throwing an exception
where one would otherwise accuse the type system of unsoundness,
but claims the error is not a type error.

It isn't clear whether this trick is enough to say the type
system is genuinely sound. One could argue dereferencing
a null pointer in C is, or is not, a type error -- either
way it is a nasty error which can't be easily tracked down
except by 'binary chop' on your code with diagnostics,
or a debugger -- and Ocaml is no different in character
when you find your code terminated with an uncaught
Not_found exception.

[A really nasty one is that polymorphic compare is not
polymorphic .. it can't handle abstract types eg BigInt
or functions .. but you'll only find out at run time ..]

In practice, Ocaml really does help detect errors early
that weaker languages like C++ would not, so this isn't
a criticism so much as a warning: it is still possible
to have a significant number of 'technical' errors in
an Ocaml program (quite apart from just getting your
encoding of some algorithm entirely wrong) -- and it 
is easy to be lulled into a false sense of security by
the very fact the basic typing is both expressive and
sound.

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Re: [Caml-list] '_a

[Alex Baretta]

skaller wrote:
> On Thu, 2005-01-27 at 11:51, Jacques Garrigue wrote:
> 
> 
>>There is no deep magic, no heuristics. There is just a type system
>>which guarantees type soundness (i.e. "well typed programs cannot
>>produce runtime type errors").
> 
> 
> Unfortunately, 'soundness' as described is somewhat weaker
> than one would like, since it depends on the expressivity
> of the type system how useful soundness actually is.
> ...

Sadly, this is very true. Camls are no genies capable of generating 
correct code when the programmer exerts friction against the computer's 
case. This is also the reason behind such DSLs as CDuce.

Of course, it is very reasonable to state that PXP is sound, but in now 
way does it guarantee the absence of runtime errors of the kind 
"required attributed not found". Here at DE&IT we are doing a good deal 
of work on extending the type system to handle XML well formedness 
constraints and possibly, to some extent, validity constraints.

Alex

-- 
*********************************************************************
http://www.barettadeit.com/
Baretta DE&IT
A division of Baretta SRL

tel. +39 02 370 111 55
fax. +39 02 370 111 54

Our technology:

The Application System/Xcaml (AS/Xcaml)
<http://www.asxcaml.org/>

The FreerP Project
<http://www.freerp.org/>

Re: '_a

[Vincenzo Ciancia]

skaller wrote:

> An exception free implementation of List.hd would
> always produce the correct typing:
> 
> let hd x = function
> | [] -> None
> | h :: _ -> Some h
> 
> In effect, Ocaml first pretends unsound typing is actually sound,
> and then enforces this at run time by throwing an exception
> where one would otherwise accuse the type system of unsoundness,
> but claims the error is not a type error.

What about the possibility to include possible exceptions into a function
signature (a la java)? Does this have problems with type inference? Also,
there is the ocamlexc tool:

http://caml.inria.fr/ocamlexc/ocamlexc.htm

what about it? 

V.

-- 
Please note that I do not read the e-mail address used in the from field but
I read vincenzo_ml at yahoo dot it
Attenzione: non leggo l'indirizzo di posta usato nel campo from, ma leggo
vincenzo_ml at yahoo dot it

RE: [Caml-list] Re: '_a

[Jacques Carette]

> What about the possibility to include possible exceptions into a 
> function signature (a la java)? Does this have problems with type 
> inference? 

I would love an (optional?) way to get the type signature of my functions to
reflect their non-totalness (exceptions + anything else), as well as
reflecting their 'imperative' content [ie which state variables are used].

In fact, any such 'monadic' information that can be automatically inferred
would be really useful to have (optionally).  I guess these are known as
'types and effects' systems.

Jacques

Re: [Caml-list] Re: '_a

[skaller]

On Fri, 2005-01-28 at 01:13, Vincenzo Ciancia wrote:
> skaller wrote:
> 
> > An exception free implementation of List.hd would
> > always produce the correct typing:
> > 
> > let hd x = function
> > | [] -> None
> > | h :: _ -> Some h
> > 
> > In effect, Ocaml first pretends unsound typing is actually sound,
> > and then enforces this at run time by throwing an exception
> > where one would otherwise accuse the type system of unsoundness,
> > but claims the error is not a type error.
> 
> What about the possibility to include possible exceptions into a function
> signature (a la java)? Does this have problems with type inference? 

Well I doubt the Java technique is any more meaningful
than the C++ one. There are three meanings of exceptions:

(a) the function domain was mis-specified, there is actually
an unstated constraint on it: the correct signature
for division is:

	divide: integer - { 0 } -> integer

(b) the codomain is mis-specified, we actually have

	List.hd: 'a list -> Some 'a

but enforce codomain 'a instead by throwing in the None case

(c) The function depends on some complex details
not considered part of the program, which can fail,
for example status of a file.

Documenting the exception instead of the constraint
on the signature doesn't seem very nice.

> Also,
> there is the ocamlexc tool:
> 
> http://caml.inria.fr/ocamlexc/ocamlexc.htm
> 
> what about it? 
> 

If I recall, this is a superb tool backed by some very smart
theory -- but in practice the output is extremely hard
to interpret.

Exceptions are often used where the constraint is expected
to be satisfied -- I myself say:

	.. Hashtbl.find table key ...

without any try/with wrapper when I 'know' the key is in
the table, and I may write 

	.. List.hd l ...

instead of 

	match l with | [] -> assert false | h :: _ -> h

However these uses of cast 'magic' are distinct from
alternate returns, where one sometimes has to cheat
the type system in the opposite direction, adding a dummy
value to code that will never be used just to get the type
right:

let x = 
	let rec f l -> | [] -> raise Not_found 
	| h :: t -> if h == v then (raise Found; 0) else f t
	in try f l with Found -> 1 | Not_found -> 2
in print_endline (string_of_int x)
;;

where the compiler doesn't know f l cannot return,
so it needs a useless '0' after the Found case
to get the typing correct. (Or you could add it after 
the 'try f l', either way it's equivalent to a safe use
of Obj.magic, safe since the cast will never be applied).

I guess some of these cases would be better handled
with a monadic technique, static exceptions, or just
doing the nasty testing: in many ways, exceptions
are *worse* than gotos, since at least the latter
in ISO C require the target to be visible.

BTW: Felix actually uses goto to replace exceptions,
and makes you pass handler into the code if necessary:

	proc error() { goto endoff; }
	fun g(e:unit->void) { ... error(); ... }
	...
	endoff:> // error found ..

Thus if you can't see the handler target in the code,
you can pass a closure which can. This guarrantees
you cannot fail to catch an exception. It is still
flawed though.

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Re: '_a

[Stefan Monnier]

> (b) the codomain is mis-specified, we actually have
> 	List.hd: 'a list -> Some 'a

Funny, I always assumed that the domain of List.hd was "'a list - []".


        Stefan

Re: [Caml-list] Re: '_a

[skaller]

On Sat, 2005-01-29 at 00:25, Stefan Monnier wrote:
> > (b) the codomain is mis-specified, we actually have
> > 	List.hd: 'a list -> Some 'a
> 
> Funny, I always assumed that the domain of List.hd was "'a list - []".

That would work too!


-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Re: [Caml-list] Re: '_a

[Keith Wansbrough]

Stefan Monnier <monnier@iro.umontreal.ca> writes:

> > (b) the codomain is mis-specified, we actually have
> > 	List.hd: 'a list -> Some 'a
> 
> Funny, I always assumed that the domain of List.hd was "'a list - []".

Yes, indeed.  Were List.hd of type 'a list -> 'a option, we'd be stuck
if we ever wanted actually to _use_ the value: any function that
attempted to extract it (say f : 'a option -> 'a) would have to have a
similar type (f : 'a option -> 'a option).

The same problem would ensue if we had explicit exception typing:

List.hd : 'a list -> 'a with_possible_exception

extract : 'a with_possible_exception -> 'a option

really_extract : 'a option -> 'a with_possible_exception

and so on...!

The only way out of this mess is to add a monad.  OCaml already has
one: return is implicit, bind is called ";", and the monad operations
include "raise" and "try ... with ...".

HTH.

--KW 8-)

Re: [Caml-list] Re: '_a

[skaller]

On Sat, 2005-01-29 at 01:46, Keith Wansbrough wrote:
> Stefan Monnier <monnier@iro.umontreal.ca> writes:
> 
> > > (b) the codomain is mis-specified, we actually have
> > > 	List.hd: 'a list -> Some 'a
> > 
> > Funny, I always assumed that the domain of List.hd was "'a list - []".
> 
> Yes, indeed.  Were List.hd of type 'a list -> 'a option, we'd be stuck
> if we ever wanted actually to _use_ the value: any function that
> attempted to extract it (say f : 'a option -> 'a) would have to have a
> similar type (f : 'a option -> 'a option).

Of course! That's what destructors are for.
Ultimately, there's no choice, no matter how you factor
it you cannot have a List.hd function returning a non sum:
destructors are the *only* way to analyse sums.

The data summation *must* be dualised by a destructor
to convert that data into control branches.

Note that List.hd actually does that .. but one
of the control paths is implicit (the one carried
by the exception).

> The only way out of this mess is to add a monad. 

That isn't the only way. I have a fairly large
project that only throw an exception in *one*
essential place (to get out of a really deep
complex recursion).

With one exception -- i do use 'monadic'
failwith () like functions to terminate 
when I detect an error (and I do use that a lot),
these are all caught at the top level (and they're
not allowed to be caught anywhere else).

Otherwise .. I find the 'pain' of using
destructors everywhere preferable to throwing
exceptions -- the additional complexity of
the control paths is a small price to pay
for their localisation. Meaning -- I sometimes
have trouble holding enough of a picture in my
head to understand my code, but with exceptions
I'm completely lost because half the code 
isn't even visible :)

>  OCaml already has
> one: return is implicit, bind is called ";", and the monad operations
> include "raise" and "try ... with ...".

Indeed, but that isn't necessarily a good monad
for all purposes (otherwise Haskell would be Ocaml
and wouldn't have any typeclasses .. LOL :)

In particular, raise is very nasty -- I can't say this
very well, but 'the monad is too global'. It's way too
powerful -- and thus too hard to reason about.

I think this is because it crosses abstraction boundaries.
You can't predict what a function will throw from its
interface, so you basically have lost control of your program.

As I understand it, Haskell style monads provide
better localisation (is that right?)

The problem with using destructors left, right, and centre,
is that you need heaps of extremely localised code to handle
all the cases. However going from that to total globality
is no solution. (In the first case the error handling
is too tighly coupled to the error detection, and in
the second too loosely coupled).

Exception specs try to relieve this but they don't work.
To me the solution appears to require some kind of
'static exceptions'.

Felix uses a non-local goto. This is definitely better
for some purpose than dynamic EH, since it ensures
every 'throw' has a matching 'catch'. The goto can be
wrapped in a closure and passed explicitly anywhere
inside the closures abstraction, allowing both
static and dynamic control path to be constructed:
either way the path is either manifest (by locality)
or explicit (by argument passing).

However this solution is not modular.
EG: you can provide a handler for division by zero,
by there's no guarrantee the client you pass it to
actually calls it for the correct error .. :)

Monads provide better modularity?

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Re: [Caml-list] Re: '_a

[Michael Walter]

On 29 Jan 2005 02:48:20 +1100, skaller <skaller@users.sourceforge.net> wrote:
> [...]
> >  OCaml already has
> > one: return is implicit, bind is called ";", and the monad operations
> > include "raise" and "try ... with ...".
> 
> Indeed, but that isn't necessarily a good monad
> for all purposes (otherwise Haskell would be Ocaml
> and wouldn't have any typeclasses .. LOL :)
This is indeed pretty much the IO monad (AFAIK O'caml).

return: (implicit)
>>: ;
fail: raise

catch: try ... with ... (not part of the Monad type class)

> In particular, raise is very nasty -- I can't say this
> very well, but 'the monad is too global'. It's way too
> powerful -- and thus too hard to reason about.
Hum.

> You can't predict what a function will throw from its
> interface, so you basically have lost control of your program.
> 
> As I understand it, Haskell style monads provide
> better localisation (is that right?)
As you define binding by yourself, you have all possibilities to
propagate errors, such as implementation exceptions, etc. Simple
examples are Maybe and Either. And IO, obviously ;-)

Michael

Re: [Caml-list] Re: '_a

[Christophe TROESTLER]

On 28 Jan 2005, skaller <skaller@users.sourceforge.net> wrote:
> 
> let x = 
> 	let rec f l -> | [] -> raise Not_found 
> 	| h :: t -> if h == v then (raise Found; 0) else f t
> 	in try f l with Found -> 1 | Not_found -> 2
> in print_endline (string_of_int x)
> 
> where the compiler doesn't know f l cannot return, so it needs a
> useless '0' after the Found case to get the typing correct.

Not quite,

let find v l =
  let x = 
    let rec f = function
      | [] -> raise Not_found 
      | h :: t -> if h = v then raise Found else f t
    in try f l with Found -> 1 | Not_found -> 2
  in print_endline (string_of_int x)

has type "val find : 'a -> 'a list -> unit = <fun>".  (BTW, note that
the equality is "=" in Caml.)  Maybe you mean something like

let cl file =
  let fh = open_in file in
  let nl = ref 0 in
  try
    while true do
      let _ = input_line fh in
      incr nl
    done
  with End_of_file -> !nl

where the [while] has type [unit] while [!nl] has type [int] and the
two cannot be unified.  But this is because there is no way for the
compiler to know that a loop indeed never ends, so one has to tell:

let cl file =
  let fh = open_in file in
  let nl = ref 0 in
  try
    while true do
      let _ = input_line fh in
      incr nl
    done;
    assert false
  with End_of_file -> !nl

With that everything is fine.

Regards,
ChriS

Re: [Caml-list] Re: '_a

[skaller]

On Sat, 2005-01-29 at 00:42, Christophe TROESTLER wrote:
> On 28 Jan 2005, skaller <skaller@users.sourceforge.net> wrote:
> > 
> > let x = 
> > 	let rec f l -> | [] -> raise Not_found 
> > 	| h :: t -> if h == v then (raise Found; 0) else f t
> > 	in try f l with Found -> 1 | Not_found -> 2
> > in print_endline (string_of_int x)
> > 
> > where the compiler doesn't know f l cannot return, so it needs a
> > useless '0' after the Found case to get the typing correct.
> 
> Not quite,

[]

> Maybe you mean something like
> 
> let cl file =
>   let fh = open_in file in
>   let nl = ref 0 in
>   try
>     while true do
>       let _ = input_line fh in
>       incr nl
>     done
>   with End_of_file -> !nl

Thanks for a better example (well a right one has to better :)

> where the [while] has type [unit] while [!nl] has type [int] and the
> two cannot be unified.  But this is because there is no way for the
> compiler to know that a loop indeed never ends, so one has to tell:
> 
> let cl file =
>   let fh = open_in file in
>   let nl = ref 0 in
>   try
>     while true do
>       let _ = input_line fh in
>       incr nl
>     done;
>     assert false
>   with End_of_file -> !nl
> 
> With that everything is fine.

Yes, that's a better solution too.

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Re: [Caml-list] Re: '_a

[Richard Jones]

On Thu, Jan 27, 2005 at 03:13:40PM +0100, Vincenzo Ciancia wrote:
> What about the possibility to include possible exceptions into a function
> signature (a la java)?

That's one of the most annoying features of Java.  Let's not copy it.

Rich.

-- 
Richard Jones, CTO Merjis Ltd.
Merjis - web marketing and technology - http://merjis.com
Team Notepad - intranets and extranets for business - http://team-notepad.com

Re: [Caml-list] Re: '_a

[Alex Baretta]

Richard Jones wrote:
> On Thu, Jan 27, 2005 at 03:13:40PM +0100, Vincenzo Ciancia wrote:
> 
>>What about the possibility to include possible exceptions into a function
>>signature (a la java)?
> 
> 
> That's one of the most annoying features of Java.  Let's not copy it.
> 
> Rich.
> 

The misfeature is the complexity explosion which tracing exceptions in 
function signatures causes. I don't want to have to deal with that.

Alex


-- 
*********************************************************************
http://www.barettadeit.com/
Baretta DE&IT
A division of Baretta SRL

tel. +39 02 370 111 55
fax. +39 02 370 111 54

Our technology:

The Application System/Xcaml (AS/Xcaml)
<http://www.asxcaml.org/>

The FreerP Project
<http://www.freerp.org/>

Re: [Caml-list] '_a

[Dave Berry]

Jacques,

That's a very interesting paper.  I note that you ask

"Our examples with constructor functions and abstract datatypes were 
expressible in
systems predating the value restriction, and are refused by the strict 
value restriction.
This makes one wonder why this didn't cause more problems during the 
transition."

At the time that SML'97 was being defined, I was working on Harlequin's SML 
compiler and programming environment (which has long since vanished into 
legal limbo).  The Harlequin team initially opposed the adoption of the 
value polymorphism rule for precisely the reasons you give.  Eventually we 
gave in because the other advantages outweighed the disadvantages.  (All 
these discussions took place in private e-mail).

Basically, the touted advantages of adopting the value polymorphism rule were:

1. The formal semantics became simpler.
2. Eliminating the different types of type variable made the language 
easier to explain, without affecting expressibility in practice.
3.  It enabled typeful compilation (as you note in your paper).

I have never believed either half of point 2.  The value polymorphism rule 
means that you have to explain about references and their effect on type 
inference even for some simple programs that don't use references at all, 
such as the example that Mike gave.  This "raises the bar" for explaining 
type inference to beginners.  Furthermore, expressiveness is affected for 
the examples that you give in your paper.  We had to change several parts 
of our code when we adopted the value polymorphism rule.  However, we felt 
(and I still think) that points 1 and 3, particularly point 3, outweigh 
these disadvantages.

 From a practical point of view, I like your approach.  However, it does 
negate point 1 above, because it makes the formal semantics more complex 
again - although this is less of a problem in O'Caml, because its semantics 
are already so complicated compared to SML97.  (I do not intend that remark 
as an insult). It will be interesting to see how your approach affects 
point 2 - novices may still encounter the value restriction in a simple 
program, and the new system will be more complicated to explain.

I sometimes wonder whether it would help to have a "pure" annotation for 
function types that would require the implementation to not use references 
nor to raise exceptions.  I don't mean a detailed closure analysis, just a 
simple flag.  Most practical functions would not be pure, but many simple 
ones could be, and these could be used to introduce people to the basics of 
functional programming without raising the complication of the value 
polymorphism rule.  (You wouldn't get a theory paper out of it 
though).  Unfortunately I'm no longer working on programming languages and 
so I don't have the capability to explore this.   It may be a half-baked 
idea that doesn't work in practice.

Best wishes,

Dave.



At 00:51 27/01/2005, Jacques Garrigue wrote:
>From: Mike Hamburg <hamburg@fas.harvard.edu>
>Subject: [Caml-list] '_a
>Date: Wed, 26 Jan 2005 19:19:16 -0500
>
> > The appearance of '_a in places where it shouldn't appear causes some
> > annoyance, and a good deal of confusion among beginners to O'Caml.  In
> > particular, List.map (fun x -> x) "ought to" have type 'a list -> 'a
> > list, whereas it instead has type '_a list -> '_a list.
> >
> > Some types are treated specially for creation of '_a, such as refs and
> > arrays.  For instance, if you have the following two declarations:
> >
> > # let a = let f x () = [x] in f [];;
> > val a : unit -> 'a list list = <fun>
> > # let b = let f x () = [|x|] in f [];;
> > val b : unit -> '_a list array = <fun>
> >
> > Although I haven't read the code for O'Caml, I deduce from this that
> > there is deep magic in place to determine when to turn 'a into '_a, and
> > in many cases, the heuristic is wrong (in the conservative direction:
> > in this case, 'a should not be turned into '_a until b is applied).
>
>There is no deep magic, no heuristics. There is just a type system
>which guarantees type soundness (i.e. "well typed programs cannot
>produce runtime type errors").
>
>If you want the type system and all the historical details, read my
>paper "Relaxing the value restriction" at
>   http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/
>
>In a nutshell, ocaml uses an improvement of the value restriction.
>With the value restriction, only definitions which are syntactical
>values (i.e. that do not call functions, etc when defined) are allowed
>to contain polymorphic type variables.
>This is improved by allowing covariant type variables to be
>generalized in all cases. Your first example is ok, because list is a
>covariant type, but your second fails, because array is not (you may
>assign to an array, and you would have to look at the code to see that
>each call to b creates a different array)
>
>Of course, one could think of many clever tricks by looking
>at what the code actually does. The above paper describes some of the
>"crazy" things Xavier Leroy and others tried in the past, which
>actually subsume your ideas, before they all decided this was too
>complicated. The main reason is that, if something is going to break
>at module boundaries, then it is not really useful.
>
>Good reading,
>
>Jacques Garrigue
>
>_______________________________________________
>Caml-list mailing list. Subscription management:
>http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>Archives: http://caml.inria.fr
>Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] '_a

[Jacques Garrigue]

Dave,

Thanks for your comments.

> Basically, the touted advantages of adopting the value polymorphism
> rule were:
> 
> 1. The formal semantics became simpler.
> 2. Eliminating the different types of type variable made the language 
> easier to explain, without affecting expressibility in practice.
> 3.  It enabled typeful compilation (as you note in your paper).

I personally believe that the main advantage is

0. Keep the typing abstract from implementation details.

This limits one very strongly when seeking alternatives.

> I have never believed either half of point 2.  The value polymorphism rule 
> means that you have to explain about references and their effect on type 
> inference even for some simple programs that don't use references at all, 
> such as the example that Mike gave.  This "raises the bar" for explaining 
> type inference to beginners.  Furthermore, expressiveness is affected for 
> the examples that you give in your paper.  We had to change several parts 
> of our code when we adopted the value polymorphism rule.  However, we felt 
> (and I still think) that points 1 and 3, particularly point 3, outweigh 
> these disadvantages.
> 
>  From a practical point of view, I like your approach.  However, it does 
> negate point 1 above, because it makes the formal semantics more complex 
> again - although this is less of a problem in O'Caml, because its semantics 
> are already so complicated compared to SML97.  (I do not intend that remark 
> as an insult). It will be interesting to see how your approach affects 
> point 2 - novices may still encounter the value restriction in a simple 
> program, and the new system will be more complicated to explain.

I agree with your first remark on point 2: while it avoids introducing
a new kind of variables, the value restriction is really confusing for
beginners. The theoretical rule may be simple, but it is not
intuitive, so one only understands it through a series of
approximations.
So my argument goes as: avoid introducing a new kind of variables (for
the sake of abstraction), but get as much polymorphism as possible, as
the non-generalizable case should be the exception.
Even if the rule for what to generalize is more complex, in some ways
it is closer to intuition. In "most" cases, it is just okay to
generalize the result of function applications.
Basically, non-generalizable cases with the relaxed restriction end up
belonging to two categories:
  * partial applications
  * mutable data structures
I believe this is easy to understand why they have to be restricted.

For the semantics, this should not be too hard. You just need to
introduce subtyping. And ocaml already has subtyping for evident
reasons.

Typed compilation shall also be ok. Note that we only allow
generalization of covariant variables (meaning "bottom"), not
contravariant ones (meaning "top"). By definition the covariant
variables correspond to no value, so you shouldn't need them to
determine the data representation. If we were also to generalize
purely contravariant variables, then we need a top object, meaning
that the representation would have to be uniform.

> I sometimes wonder whether it would help to have a "pure" annotation for 
> function types that would require the implementation to not use references 
> nor to raise exceptions.  I don't mean a detailed closure analysis, just a 
> simple flag.  Most practical functions would not be pure, but many simple 
> ones could be, and these could be used to introduce people to the basics of 
> functional programming without raising the complication of the value 
> polymorphism rule.  (You wouldn't get a theory paper out of it 
> though).  Unfortunately I'm no longer working on programming languages and 
> so I don't have the capability to explore this.   It may be a half-baked 
> idea that doesn't work in practice.

This is also an idea that crosses my mind once in a while, but I never
tried to formalize it further.
Looks like the main problem would be to decide where to use this
annotation. You can quickly get back into the above abstraction
problem, if purity is not considered as an essential part of the
semantics.
So this looks like an idea hard to apply in practice.

   Jacques Garrigue

Re: [Caml-list] '_a

[Florian Hars]

Jacques Garrigue wrote:
> From: Mike Hamburg <hamburg@fas.harvard.edu>
>># let b = let f x () = [|x|] in f [];;
>>val b : unit -> '_a list array = <fun>
 >
> but your second fails, because array is not [covariant] (you may
> assign to an array, and you would have to look at the code to see that
> each call to b creates a different array)

Of course, in this case the usual trick of some greek letter-expansion (was
it eta?) works:

# let b () = let f x () = [|x|] in f [] ();;
val b : unit -> 'a list array = <fun>

Maybe this should be mentioned in the "A type variable starts with _?" part of
the FAQ, like:

| In this case the type checker errs on the conservative side, as the function
| map_id could be fully polymorphic. This is caused by the fact that the
| definition is given in the so called eta-reduced form, and you can recover
| the full polymorphism by giving it in eta-expanded form, which the type
| checker handles more gracefully:
|
| # let map_id l = List.map (function x -> x) l;;
| val map_id : 'a list -> 'a list = <fun>

Yours, Florian.
-- 
#!/bin/sh -
set - `type -p $0` 'tr [a-m][n-z]RUXJAKBOZ [n-z][a-m]EH$W/@OBM' fu XUBZRA.fvt\
angher echo;while [ "$5" != "" ];do shift;done;$4 "gbhpu $3;znvy sKunef.qr<$3\
&&frq -a -rc "`$4 "$0"|$1`">$3;rpub 'Jr ner Svtangher bs Obet.'"|$1|`$4 $2|$1`