headers
Jon Harrop | 1 Nov 2008 02:08

Re: RE: understanding weak

On Thursday 30 October 2008 18:48:26 CUOQ Pascal wrote:
> Warren Harris <warren <at> metaweb.com> wrote:
> > I'd like to understand better how ocaml's weak pointers operate.
>
> You will be interested in the following important article:
> http://portal.acm.org/citation.cfm?id=1411308

Is this freely available anywhere?

--

-- 
Dr Jon Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?e

_______________________________________________
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
Permalink | Reply | 2 comments |
headers
Jon Harrop | 1 Nov 2008 02:41

Re: What does Jane Street use/want for an IDE? What about you?

On Monday 20 October 2008 14:19:40 Kuba Ober wrote:
> what do you guys use for your development environment?

I use Emacs but I hate it.

> What would be the minimal set of functionality that would make you happy for
> an IDE?

. Written in OCaml using OCaml's own lexer and parser to save effort and make 
it possible for others to help develop it without losing their hair.

. A proper GUI (where options can be set using the mouse).

. Mainstream key bindings, e.g. CTRL+S for save.

. Jump to definition.

. Graphical throwback of the type of the subexpression under the mouse pointer 
or in the current selection.

. Graphical throwback of the documentation related to what is under the mouse 
pointer.

. Graphical throwback of errors and, in the case of type errors, optional 
highlighting of previous unification points.

. Refactoring, e.g. changing the name of a definition in all occurrences.

. Autocompletion that handles structural types in LablGTK code and operators, 
i.e. when the user types "+" present options for int "+", float "+.",
(Continue reading)

Permalink | Reply | 33 comments |
headers
Edgar Friendly | 1 Nov 2008 02:52
Picon
Gravatar

Re: Private types

Jacques Garrigue wrote:

> Your intuition is correct that it would theoretically be possible to
> try subtyping in place of unification in some cases. The trouble is
> that thoses cases are not easy to specify (so that it would be hard
> for the programmer to known when he can remove a coercion), 

Does the compiler really get any information from an explicit cast that
it can't figure out already?  I can't come up with any example.

> and that
> subtyping is potentially very costly (structural subtyping is much
> harder to check than the nominal subtyping you have in Java.)

As the compiler needs to check that explicit casts are valid, I don't
see any performance difference between explicit and implicit subtype casts.

> So the current approach is to completely separate subtyping and type
> inference, and require coercions everywhere subtyping is needed.
> 
Would it be particularly difficult to, in the cases where type [x] is
found but type [y] is expected, to try a (foo : x :> y) cast?

> You can also compare that to the situation between int and float.
> For most uses, int can be viewed as a subtype of float. However ocaml
> separates the two, and requires coercion functions whenever you want
> to use an int as a float.
> 
Code isn't produced by a :> cast.  As the internal representation of int
and float differs, a coercion function isn't required.  The internal
(Continue reading)

Permalink | Reply | 8 comments |
headers
David Allsopp | 1 Nov 2008 09:19

RE: Private types

Edgar Friendly wrote:
> Jacques Garrigue wrote:
>
> > Your intuition is correct that it would theoretically be possible to
> > try subtyping in place of unification in some cases. The trouble is
> > that thoses cases are not easy to specify (so that it would be hard
> > for the programmer to known when he can remove a coercion), 
>
> Does the compiler really get any information from an explicit cast that
> it can't figure out already?  I can't come up with any example.

Polymorphic variants. Consider:

type t = [ `A of int ]

let f (x : t) =
  let `A n = x
  in
    if n mod 2 = 0
    then (x : t :> [> t ])
    else `B (2 * n)

Without the full coercion for x you'll get a type error because the type
checker infers that the type of the [if] expression is [t] from the [then]
branch and then fails to unify [> `B of int ] with [t] unless the type of
[x] is first coerced to [> t ]. If the compiler were to try (x : t : [> t ])
in all those instances I think that would render polymorphic variants pretty
unusable ... the type checker needs to know that you meant to do that or
everything will unify!
(Continue reading)

Permalink | Reply | 3 comments |
headers
Jacques Garrigue | 1 Nov 2008 10:52
Picon

Re: Private types

Dear Dario,

Since you use a private abbreviation, extraction from the private type
must be explicit before you can do anything on its representation.
So the solution is simple enough:

module Mymod =
  struct
    let is_foo2 x =
      match (x : _ Foobar.t :> [> ]) with `A -> true | `B -> false
  end

The [> ] as target type just says that you expect a polymorphic
variant, which is incompatible with Foobar.t, and triggers its
expansion.

If you want to avoid this explicit coercion, you must use a private
row type in place of a private abbreviation. However, you loose the
ability to distinguish between values created by make_a and make_b at
the type level.

module Foobar: sig
  type foo_t = [ `A ]
  type bar_t = [ `B ]
  type foobar_t = [ foo_t | bar_t ]
  type t = private [< foobar_t]

  val make_a: unit -> t
  val make_b: unit -> t
  val is_foo: t -> bool
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jacques Garrigue | 1 Nov 2008 11:00
Picon

Re: Private types

From: Edgar Friendly <thelema314 <at> gmail.com>

> > So the current approach is to completely separate subtyping and type
> > inference, and require coercions everywhere subtyping is needed.
> > 
> Would it be particularly difficult to, in the cases where type [x] is
> found but type [y] is expected, to try a (foo : x :> y) cast?

If we limit ourselves to the case where both [x] and [y] contrain no
type variables, this si not particularly difficult. However whether
they will contain type variables or not depends heavily on how the
type inference algorithm proceeds.

If they contain type variables, then the situation becomes much more
muddled, as these type variables may get instantiated by the subtyping
check, and not necessarily as expected. So typing becomes rather
unpredictable...

> > You can also compare that to the situation between int and float.
> > For most uses, int can be viewed as a subtype of float. However ocaml
> > separates the two, and requires coercion functions whenever you want
> > to use an int as a float.
> > 
> Code isn't produced by a :> cast.  As the internal representation of int
> and float differs, a coercion function isn't required.  The internal
> representation of [private int] and [int] is the same, not to mention
> one is exactly the [private] of the other.

This was not intended as a complete comparison :-)
However, since the coercion function is canonical, I don't think that
(Continue reading)

Permalink | Reply | 1 comment |
headers
Stefano Zacchiroli | 1 Nov 2008 11:37

Re: RE: understanding weak

On Sat, Nov 01, 2008 at 01:08:17AM +0000, Jon Harrop wrote:
> > You will be interested in the following important article:
> > http://portal.acm.org/citation.cfm?id=1411308
> Is this freely available anywhere?

<rant>

Seriously, you SPAM everybody here with periodical announces of
non-free issues of the OCaml journal and don't even have access to a
random lab with an ACM subscription?

</rant>

SCNR.

Do as we all do: look on authors' homepage, mail them, try citeseer
cache, ...

--

-- 
Stefano Zacchiroli -*- PhD in Computer Science \ PostDoc  <at>  Univ. Paris 7
zack <at> {upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Dietro un grande uomo c'è sempre /oo\ All one has to do is hit the right
uno zaino        -- A.Bergonzoni \__/ keys at the right time -- J.S.Bach

_______________________________________________
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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Daniel Bünzli | 1 Nov 2008 11:40
Picon

Re: let rec and environment sharing


Le 31 oct. 08 à 22:17, Zheng Li a écrit :

> AFAIK, the answer is yes.
>
> - I once saw this on a teaching slide of Xavier Leroy (I don't  
> remember which one, but you can probably find it on his webpage)

Maybe your thinking about this [1]. It states that ocaml uses minimal  
environments hence my second example shouldn't leak.

> Btw, it is called infix pointers, and there's a "infix" tag for  
> OCaml block value.

If this corresponds to what is described in the same document. Then  
the mutually recursive definitions should share the same environment.

Thanks,

Daniel

[1] http://pauillac.inria.fr/~xleroy/dea/compil/fermetures

_______________________________________________
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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Rémi Vanicat | 1 Nov 2008 14:01
Picon
Favicon
Gravatar

Re: Private types

Edgar Friendly <thelema314 <at> gmail.com> writes:

> Jacques Garrigue wrote:
>
>> Your intuition is correct that it would theoretically be possible to
>> try subtyping in place of unification in some cases. The trouble is
>> that thoses cases are not easy to specify (so that it would be hard
>> for the programmer to known when he can remove a coercion), 
>
> Does the compiler really get any information from an explicit cast that
> it can't figure out already?  I can't come up with any example.

you mean as in the following function ? 
let f x = (x : t :> t')

--

-- 
Rémi Vanicat

_______________________________________________
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
Permalink | Reply | 1 comment |
headers
Edgar Friendly | 1 Nov 2008 14:30
Picon
Gravatar

Re: Re: Private types

Rémi Vanicat wrote:
> Edgar Friendly <thelema314 <at> gmail.com> writes:
> 
>> Does the compiler really get any information from an explicit cast that
>> it can't figure out already?  I can't come up with any example.
> 
> you mean as in the following function ? 
> let f x = (x : t :> t')
> 
Well, yes and no.  That function in a vacuum doesn't have enough
information to infer types t and t', but within a larger program, if it
gets used in a manner other than ('a -> 'a), the cast should be obvious, no?

E.

_______________________________________________
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
Permalink | Reply | 0 comments |

Gmane