Type annotations

Type annotations

[Ohad Rodeh]

Dear List, 
  I've previously sent a message, for which I got no replies, so
I'm resending it. 

> ... stuff removed ...
> 
> > Also, I am a bit curious why it doesn't help to type explicitely,
> > i.e. to
> > write
> > let x:point_3d={x=10.;y=20.;z=30.} ???
> > 
> 
> Because this is not the way it works. Labels are defined as are values
> or constructors, this is only afterwards that the compiler checks that
> they all belong to the same type. That is, the type cannot influence the
> choice between x(point_3d) and x(point_2d), only the order of
> definition can.
> 
> There has been already various proposals for allowing types to be taken
> into account when typing record labels. The difficulty is that as soon
> as you make it into something useful, you loose the principal type
> property, and that some theoreticians working on ocaml wouldn't like
> it.

The loss of the pricipal type theorem has also recently been discussed in
comp.lang.ml and comp.lang.functional. Using type-annotation by the
compiler prior (call this the PRIOR approach) to unification can help
typing expression that cannot be typed otherwise. For example, cases of
polymoriphic recursion. In fact, this is the way this is handled in
Haskell (this topic has also appeared in this list previously). 
Although I wouldn't go running to implement all my code in Haskell :-), I
do think that using PRIOR could be an improvement. 

Is there a problem with PRIOR? 

	Ohad.

Re: Type annotations

[Jacques Garrigue]

> > There has been already various proposals for allowing types to be taken
> > into account when typing record labels. The difficulty is that as soon
> > as you make it into something useful, you loose the principal type
> > property, and that some theoreticians working on ocaml wouldn't like
> > it.
> 
> The loss of the pricipal type theorem has also recently been discussed in
> comp.lang.ml and comp.lang.functional. Using type-annotation by the
> compiler prior (call this the PRIOR approach) to unification can help
> typing expression that cannot be typed otherwise. For example, cases of
> polymoriphic recursion. In fact, this is the way this is handled in
> Haskell (this topic has also appeared in this list previously). 
> Although I wouldn't go running to implement all my code in Haskell :-), I
> do think that using PRIOR could be an improvement. 
> 
> Is there a problem with PRIOR? 

There are a few things that work well with this approach, polymorphic
recursion being one. But it is not as general as it seems.
A simple scheme is to assume that you can give explicitely a type to
an identifier, use this type to resolve ambiguities, and check
afterwards that this type is correct.
With such a scheme,
     let w : t = {x=1;y=2} in w.x
will indeed be correctly handled.
However, this breaks as soon as an annotation is lacking:
     let w : t = {x=1;y=2} in
     let v = w in
     w.x
Similarly, pairs won't work
     let w : t * int = ({x=1;y=2}, 3) in (fst w).x
Indeed, while w was given a special "assumed" type, propagating such
assumed types through definitions and function calls is much more
subtle.
In a paper by Didier Remy and myself [1], we designed a system that
could do a fair amount of "assumed" type propagation. This was
intended for providing first class polymorphism and polymorphic
methods, and was implemented in Objective Label. This could also be
used for typing records, while some might see it as an overkill.
But this is much more complex than what you are calling PRIOR.
And this is not principal in the strict meaning (due to a mischevious
side-effect of the value only prolymorphism rule).

I am currently working on reintegrating this feature in ocaml. However
it is not yet clear whether it can be made cheap enough to make it
into the main stream version (type inference becomes slower).
And then some might discuss the fact it would require people to learn
yet another set of rules about how assumed types are propagated.

Cheers,

Jacques

[1] Extending ML with semi-explicit higher order polymorphism,
    Information and Computation 155, december 1999, pages 134-171.

---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Ref syntax

[Ohad Rodeh]

List,
  I have a modest syntax request as we are approaching
the release of OCaml-3.01. Currently, if x is a
reference, one must use the assignment operator (:=) to
update it. Can array assignment (<-) be used also? 

  Thanks, 
     Ohad.	

Re: Ref syntax

[Jacques Garrigue]

From: Ohad Rodeh <orodeh@cs.huji.ac.il>

>   I have a modest syntax request as we are approaching
> the release of OCaml-3.01. Currently, if x is a
> reference, one must use the assignment operator (:=) to
> update it. Can array assignment (<-) be used also? 

Sorry, but this does not work: this may be confused with record assignment.

       type t = {mutable x : int ref};;
       let r = {x = ref 1};;
       r.x <- ref 2;;
       r.x := 3;;

So here is also my wishlist for Santa Xavier.

* addition of let mutable ... in
       let mutable x = 0 in
       for i = 1 to do x <- x + i done;
       x
  The idea is to have references which are certified not to be
  returned or passed to functions. Easy.
  Makes lots of thing clearer, but it might be a good idea to allow
  only the let ... in form, since toplevel let mutable is rather
  opposed to functional programming.

* addition of let open ... in
       module P2d = struct type t = {x:int;y:int} end
       module P3d = struct type t = {x:int;y:int;z:int} end
       let f2d p1 p2 =
         let open P2d in
         {x = p1.x + p2.x; y = p1.y + p2.y}
  Extremely easy.

* allow #labels in programs
  avoids subtle makefiles when you have both files with and without
  labels, also avoid to check the mode before compiling a file.

* have a notation to abbreviate the OCAMLLIB directory in include
  paths. One could write
       ocamlc -c -I +labltk -I +lablGL gears.ml
  rather than
       ocamlc -c -I `ocamlc -where`/labltk -I `ocamlc -where`/lablgGL gears.ml

I would be already satisfied with only one of these...

Cheers,

Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Re: Ref syntax

[Sven LUTHER]

On Fri, Dec 22, 2000 at 12:29:38PM +0900, Jacques Garrigue wrote:
> * have a notation to abbreviate the OCAMLLIB directory in include
>   paths. One could write
>        ocamlc -c -I +labltk -I +lablGL gears.ml
>   rather than
>        ocamlc -c -I `ocamlc -where`/labltk -I `ocamlc -where`/lablgGL gears.ml

Yes this is extremely usefull, and would be a necessity if you don't want
people to simply install all their stuff in the $OCAMLLIB directory, possibly
overwritting some future addition to the what is put in there by ocaml.

Also, what is the reason the current system does search in the $OCAMLLIB as
well as the current directory for files ? if this was so, we could simply
write :

    ocamlc -c -I labltk -I lablGL gears.ml

and have ocamlc search in the following places (and in this order ?) :

    $OCAMLLIB
    $PWD
    $PWD/labltk
    $PWD/lablGL
    $OCAMLLIB/labltk
    $OCAMLLIB/lablGL

C does something similar with his include files ?

Also another related issue would be to be able to append a modules path
element to libraries when building them. (or maybe this is already possible
?).

It would go like this :

    ocamlc -<some special flag> XXX -a foo.cmo bar.cmo -o xxx.cma 

which would give would put the modules in the xxx.cma library as follows :

   XXX.Bar
   XXX.Foo

instead of :

   Bar
   Foo

Thus permitting people to reuse modules names in their libraries whitout
needing to be carefull with conflict with other similar module names.

Friendly,

Sven Luther

Re: Ref syntax

[John Prevost]

>>>>> "sl" == Sven LUTHER <luther@dpt-info.u-strasbg.fr> writes:

    sl> Also another related issue would be to be able to append a
    sl> modules path element to libraries when building them. (or
    sl> maybe this is already possible ?).

It's not, without writing something like:

XXX.ml:
module Foo = Foo
module Bar = Bar
module ...

and of course that also leaves Foo and Bar at the top level.

    sl> Thus permitting people to reuse modules names in their
    sl> libraries whitout needing to be carefull with conflict with
    sl> other similar module names.

Count me in voting for this.  Namespace management continues to be
messy in O'Caml.  We need *something* better.  This would make
libraries, anyway, a little nicer.

John.

Re: Ref syntax

[Pierre Weis]

> From: Ohad Rodeh <orodeh@cs.huji.ac.il>
> 
> >   I have a modest syntax request as we are approaching
> > the release of OCaml-3.01. Currently, if x is a
> > reference, one must use the assignment operator (:=) to
> > update it. Can array assignment (<-) be used also? 
> 
> Sorry, but this does not work: this may be confused with record assignment.
> 
>        type t = {mutable x : int ref};;
>        let r = {x = ref 1};;
>        r.x <- ref 2;;
>        r.x := 3;;

When I introduced mutable fields in Caml, I considered having the same
:= operator than for references (the symetric situation of Ohad's
suggestion). I found this ambiguity problem, and also found that it
can be easily disambiguated, if you just consider that assignment to a
mutable field with a reference in it is not a common practice in Caml,
and accept an extra syntactic burden to handle this case: you must
add an extra couple of parens.

So, if you want to treat reference assignment with the same construct
as record assignment, you just have to implement the <- assigment by
adding to the main expr rule of the Caml parser, those two lines

| simple_expr0 LESSMINUS expr
    { mkinfix $1 ":=" $3 }

where simple_expr0 is even simpler than the actual simple_expr, since
it does not include field access.

This modification forces the addition of extra parens to assign any
reference that is not just a simple name.

Hence, your program would read

r.x <- ref 2;;
(r.x) <- 3;;

We also considered an even more drastic rule: reference assignment
must be done to a mere ident

| val_longident LESSMINUS expr
    { mkinfix $1 ":=" $3 }

Then your program should be written:

let my_ref = r.x in
my_ref <- 3

This last construct has been considered not ``compositional enough''
and was rejected.

I consider the ``| simple_expr0 LESSMINUS expr'' rule as perfectly
acceptable, but I decided to keep this syntactic construct ident <-
expr for ``variables'' assignment, i.e. for a future reintroduction of
good old letref lvalues of the original ML (alias your ``references
certified not to be returned or passed to functions. Easy.'', wish No
1 of your presonal wish list).

> So here is also my wishlist for Santa Xavier.
> 
> * addition of let mutable ... in
>        let mutable x = 0 in
>        for i = 1 to do x <- x + i done;
>        x
>   The idea is to have references which are certified not to be
>   returned or passed to functions. Easy.
>   Makes lots of thing clearer, but it might be a good idea to allow
>   only the let ... in form, since toplevel let mutable is rather
>   opposed to functional programming.

You forgot to mentioned that this feature also adds a lot of
complexity: as a kind of witness of this extra difficulty, we can
observe that you immediately suggest to restrict the construct to
local forms. I suppose that this is not for the vague philosophical
reason you mentioned (``let mutable is rather opposed to functional
programming''), but more seriously to avoid real difficulties, such as
complex typechecking problems (with value polymorphism restriction ?),
or even compilation and semantics problems. For instance, what do we
do if such a letref variable is assigned to, from within the body of a
function (that could be exported) ? (This is the original bug in the
LCF system that justified the introduction of first class references,
and then triggered the ``typechecking polymorphic imperative
languages'' quest). Furthermore, this construct would add an entirely
new notion to Caml: lvalues. This is not so easy to explain and
justify, when we now have a simple and regular semantics scheme that
only requires right values in the language (with explicit operators on
right values to implement mutation: explicit access and mutation
operation). So, I really do think that the qualification you gave for
this addition, ``Easy.'', has to be justified with rules and
proofs. (Remember that Robin Milner admitted that this construct just
beat him, since the implementation of letref introduced a flaw in the
LCF theorem prover assistant).

> * addition of let open ... in
>        module P2d = struct type t = {x:int;y:int} end
>        module P3d = struct type t = {x:int;y:int;z:int} end
>        let f2d p1 p2 =
>          let open P2d in
>          {x = p1.x + p2.x; y = p1.y + p2.y}
>   Extremely easy.

I hope it is ``Extremely easy''. Remember that Pascal has been
criticised for its ``with'' construct that locally introduces new
names in programs in a completely silent way. Are you sure this is a
desirable feature ?

> * allow #labels in programs
>   avoids subtle makefiles when you have both files with and without
>   labels, also avoid to check the mode before compiling a file.
>
> * have a notation to abbreviate the OCAMLLIB directory in include
>   paths. One could write
>        ocamlc -c -I +labltk -I +lablGL gears.ml
>   rather than
>        ocamlc -c -I `ocamlc -where`/labltk -I `ocamlc -where`/lablgGL gears.ml
> 
> I would be already satisfied with only one of these...

So you are already satisfied, since you can write

  ocamlc -c -I +camltk -I +camlimages ocaml_unreal_t.ml

in the current development version!

Cheers,

Pierre Weis

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

Re: Ref syntax

[Jacques Garrigue]

From: Pierre Weis <Pierre.Weis@inria.fr>

> I consider the ``| simple_expr0 LESSMINUS expr'' rule as perfectly
> acceptable, but I decided to keep this syntactic construct ident <-
> expr for ``variables'' assignment, i.e. for a future reintroduction of
> good old letref lvalues of the original ML (alias your ``references
> certified not to be returned or passed to functions. Easy.'', wish No
> 1 of your presonal wish list).

In fact they are already here, with fields in objects.
Just that you can only use them inside objects.
So you were clever to keep it :-)

> > So here is also my wishlist for Santa Xavier.
> > 
> > * addition of let mutable ... in
> >        let mutable x = 0 in
> >        for i = 1 to do x <- x + i done;
> >        x
> >   The idea is to have references which are certified not to be
> >   returned or passed to functions. Easy.
> >   Makes lots of thing clearer, but it might be a good idea to allow
> >   only the let ... in form, since toplevel let mutable is rather
> >   opposed to functional programming.
> 
> You forgot to mentioned that this feature also adds a lot of
> complexity: as a kind of witness of this extra difficulty, we can
> observe that you immediately suggest to restrict the construct to
> local forms. I suppose that this is not for the vague philosophical
> reason you mentioned (``let mutable is rather opposed to functional
> programming''), but more seriously to avoid real difficulties, such as
> complex typechecking problems (with value polymorphism restriction ?),
> or even compilation and semantics problems.

Really, I don't think it would be useful at toplevel.
I view let mutable .. in as a way to provide some state, but
immediately cleanly wrapped, either by only being used locally, or
in exported functions.
This is completely similar to mutable object fields; both the goal and
the method.

> For instance, what do we
> do if such a letref variable is assigned to, from within the body of a
> function (that could be exported) ?

This is just syntactic sugar for references, which is why I said it
was easy. Similarly typing is just the typing of references.

> Furthermore, this construct would add an entirely
> new notion to Caml: lvalues.

As stated above: they are already here, object fields.
You may think of it as a good or bad idea, but the distinction
between it and the fact a.x behaves differently when there is a <- and
when there is none is subtle.

But well, this was only first in my wish list because I was answering
to a message related to that. My personal priority is much lower.

> > * addition of let open ... in
> >        module P2d = struct type t = {x:int;y:int} end
> >        module P3d = struct type t = {x:int;y:int;z:int} end
> >        let f2d p1 p2 =
> >          let open P2d in
> >          {x = p1.x + p2.x; y = p1.y + p2.y}
> >   Extremely easy.
> 
> I hope it is ``Extremely easy''. Remember that Pascal has been
> criticised for its ``with'' construct that locally introduces new
> names in programs in a completely silent way. Are you sure this is a
> desirable feature ?

I think this is different: modules are already a way to organize the
namespace, and this allows you to do it more locally. You can already do
it with camlp4, so what?

> > * have a notation to abbreviate the OCAMLLIB directory in include
> >   paths. One could write
> >        ocamlc -c -I +labltk -I +lablGL gears.ml
> >   rather than
> >        ocamlc -c -I `ocamlc -where`/labltk -I `ocamlc -where`/lablgGL gears.ml
> > 
> > I would be already satisfied with only one of these...
> 
> So you are already satisfied, since you can write
> 
>   ocamlc -c -I +camltk -I +camlimages ocaml_unreal_t.ml
> 
> in the current development version!

Great! I had seen the introduction of -where, but didn't catch this
one.
Thanks, Papa Weis !

Jacques

Re: Ref syntax

[Pierre Weis]

> Really, I don't think it would be useful at toplevel.
> I view let mutable .. in as a way to provide some state, but
> immediately cleanly wrapped, either by only being used locally, or
> in exported functions.
> This is completely similar to mutable object fields; both the goal and
> the method.

I hope this is effectively simple to type check, and ensure correct.

> > For instance, what do we
> > do if such a letref variable is assigned to, from within the body of a
> > function (that could be exported) ?
> 
> This is just syntactic sugar for references, which is why I said it
> was easy. Similarly typing is just the typing of references.

So you mean, that if we define x with let mutable x = 1, the variable
x has in fact type int ref ?

> > Furthermore, this construct would add an entirely
> > new notion to Caml: lvalues.
> 
> As stated above: they are already here, object fields.
> You may think of it as a good or bad idea, but the distinction
> between it and the fact a.x behaves differently when there is a <- and
> when there is none is subtle.

Sorry, but for field mutations the syntactic construct is not
 expr <- new_val
but
 expr.label <- new_val
which is semantically assign_to_label (expr, new_val), as
 expr.(i) <- new_val
is a short-hand for assign_to_vector (expr, i, new_val).

In both constructs there is no notion of left values.

I really don't know if the corresponding notion for objects needs
lvalues or not.

> But well, this was only first in my wish list because I was answering
> to a message related to that. My personal priority is much lower.

I think exactly the same: the let mutable (or var construct as we used
to call it) is desirable, but may not be worth the implementation
effort.

[...]
> > So you are already satisfied, since you can write
> > 
> >   ocamlc -c -I +camltk -I +camlimages ocaml_unreal_t.ml
> > 
> > in the current development version!
> 
> Great! I had seen the introduction of -where, but didn't catch this
> one.
> Thanks, Papa Weis !
> 
> Jacques

Hey, this is your ``Santa Xavier's'' work. Thanks to him.

Cheers,

Pierre Weis

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

Re: Ref syntax

[Marcin 'Qrczak' Kowalczyk]

Fri, 22 Dec 2000 10:07:07 +0100 (MET), Pierre Weis <Pierre.Weis@inria.fr> pisze:

> Furthermore, this construct would add an entirely new notion to
> Caml: lvalues.

It would not necessarily cause troubles. "let mutable x = init_value
in expr" would be equivalent to "let ref_x = ref init_value in expr",
where x is a *macro* visible inside expr, expanding to ref_x.contents
in all contexts, before desugaring expressions of the form
variable.field <- something.

So for example "let y = x in ..." placed inside expr would bind the
snapshot of x's value to y, and "let y () = x in ..." would create
a function which retrieves the current x's value each time it is
called. No more confusing than usual eager evaluation order.

There is no direct access to ref_x itself.

IMHO it's perfectly consistent with mutable record fields.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK

Re: Ref syntax

[Pascal Brisset]

> * addition of let mutable ... in
>        let mutable x = 0 in
>        for i = 1 to do x <- x + i done;
>        x

 Unfortunately, it violates the simple ``rule'' which says that there
must be a dot (.) on the left side of a left arrow (<-). I like this
kind of simple rule which can be taught to beginners and help
debugging their programs.

 On my wish list, I put a "-strict" option for ocamlc which would
remove freedom in the syntax. For example
 - ";" means "sequence" and not "end of expr" (it is currently allowed
before "end" in a block)
 - "|" means "or" or "start of pattern" but not both
 - ";;" is compulsory
 - deprecated "&" and "or" operators removed
 - ...

--Pascal

Re: Ref syntax

[John Prevost]

>>>>> "pb" == Pascal Brisset <brisset@recherche.enac.fr> writes:

    pb> On my wish list, I put a "-strict" option for ocamlc which
    pb> would remove freedom in the syntax. For example

    pb> - ";" means "sequence" and not "end of expr" (it is currently
    pb>   allowed before "end" in a block)

    pb> - "|" means "or" or "start of pattern" but not both

What do you mean?  In terms of "or patterns"?

    pb> - ";;" is compulsory

Oh god no.  Please, no.  I believe that if anything, strict syntax
should not allow ";;".  It's only necessary if you write imperative
things at the top level, and even then, I believe it's preferable to
use "let _ = ...".  If you're aiming to make things clearer, get rid
of it totally.

    pb> - deprecated "&" and "or" operators removed

So only && and ||?  That's somewhat reasonable.

But please, no, never encourage anybody to use ;;!

John.

Re: Ref syntax

[Marcin 'Qrczak' Kowalczyk]

Thu, 21 Dec 2000 14:50:38 +0200 (IST), Ohad Rodeh <orodeh@cs.huji.ac.il> pisze:

>   I have a modest syntax request as we are approaching
> the release of OCaml-3.01. Currently, if x is a
> reference, one must use the assignment operator (:=) to
> update it. Can array assignment (<-) be used also? 

It would be inconsistent. With <- the same "level of deredeferencing"
is on both sides: "r.x <- r.x" is legal. With := the lhs is a reference
and rhs is a dereferenced value, and the identity assignment is "x := !x".

The only consistent syntax would be "!x <- new_contents_of_x". Note
that the revised syntax uses "x.val <- new_contents_of_x", with x.val
being equivalent to old !x on both sides of <- and without the need
of any magic syntax for references in addition to what is available
anyway for mutable fields.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK

Re: Ref syntax

[John Prevost]

>>>>> "mk" == Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> writes:

    mk> The only consistent syntax would be "!x <-
    mk> new_contents_of_x". Note that the revised syntax uses "x.val
    mk> <- new_contents_of_x", with x.val being equivalent to old !x
    mk> on both sides of <- and without the need of any magic syntax
    mk> for references in addition to what is available anyway for
    mk> mutable fields.

Of course, in the standard syntax you can write "x.contents <- 1" in
the same way.  Though that's quite a bit more verbose.

John.

Re: Ref syntax

[Pierre Weis]

> >>>>> "mk" == Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> writes:
> 
>     mk> The only consistent syntax would be "!x <-
>     mk> new_contents_of_x". Note that the revised syntax uses "x.val
>     mk> <- new_contents_of_x", with x.val being equivalent to old !x
>     mk> on both sides of <- and without the need of any magic syntax
>     mk> for references in addition to what is available anyway for
>     mk> mutable fields.
> 
> Of course, in the standard syntax you can write "x.contents <- 1" in
> the same way.  Though that's quite a bit more verbose.
> 
> John.

This is already possible in the current version of Objective Caml.

        Objective Caml version 3.00

# let x = ref 2;;
val x : int ref = {contents=2}
# x.contents;;
- : int = 2
# x.contents <- 1;;
- : unit = ()

If you don't like operators ! and :=, just don't use them, and use the
regular filed acces instead!

Merry Christmas,

Pierre Weis

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