caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] ocaml considered dangerous
@ 2014-01-16 23:00 Jürgen Pfitzenmaier
  2014-01-16 23:27 ` Milan Stanojević
                   ` (4 more replies)
  0 siblings, 5 replies; 16+ messages in thread
From: Jürgen Pfitzenmaier @ 2014-01-16 23:00 UTC (permalink / raw)
  To: caml-list

[-- Attachment #1: Type: text/plain, Size: 316 bytes --]

Dear Ocaml users,
I found some serious errors in the compiler e.g. in line 28 of
typing/includecore.ml
and line 499 of typing/ctype.ml of version 3.12.1.

A longer list of errors with explanations and possible fixes will be under
      www.pfitzenmaier.de/ocaml-considered-dangerous.html

regards,
Jürgen

[-- Attachment #2: Type: text/html, Size: 840 bytes --]

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-16 23:00 [Caml-list] ocaml considered dangerous Jürgen Pfitzenmaier
@ 2014-01-16 23:27 ` Milan Stanojević
  2014-01-16 23:33 ` Daniel Bünzli
                   ` (3 subsequent siblings)
  4 siblings, 0 replies; 16+ messages in thread
From: Milan Stanojević @ 2014-01-16 23:27 UTC (permalink / raw)
  To: Jürgen Pfitzenmaier; +Cc: Caml List

Your url returns 404

On Thu, Jan 16, 2014 at 6:00 PM, Jürgen Pfitzenmaier
<pfitzen@pfitzenmaier.de> wrote:
> Dear Ocaml users,
> I found some serious errors in the compiler e.g. in line 28 of
> typing/includecore.ml
> and line 499 of typing/ctype.ml of version 3.12.1.
>
> A longer list of errors with explanations and possible fixes will be under
>       www.pfitzenmaier.de/ocaml-considered-dangerous.html
>
> regards,
> Jürgen
>

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-16 23:00 [Caml-list] ocaml considered dangerous Jürgen Pfitzenmaier
  2014-01-16 23:27 ` Milan Stanojević
@ 2014-01-16 23:33 ` Daniel Bünzli
  2014-01-17  0:43 ` Nicolas Braud-Santoni
                   ` (2 subsequent siblings)
  4 siblings, 0 replies; 16+ messages in thread
From: Daniel Bünzli @ 2014-01-16 23:33 UTC (permalink / raw)
  To: Jürgen Pfitzenmaier; +Cc: caml-list

No need to make sensationalist headlines. Bugs exist and they are being tracked here:

http://caml.inria.fr/mantis/

You can report there any problems you may have found. Besides quite some work has been going on since 3.12.1. You may want to check if your problem still exists in the latest version. Here's a comprehensive list of what changed since then:

http://caml.inria.fr/pub/distrib/ocaml-4.01/notes/Changes

Best,

Daniel



^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-16 23:00 [Caml-list] ocaml considered dangerous Jürgen Pfitzenmaier
  2014-01-16 23:27 ` Milan Stanojević
  2014-01-16 23:33 ` Daniel Bünzli
@ 2014-01-17  0:43 ` Nicolas Braud-Santoni
  2014-01-20 10:07   ` Goswin von Brederlow
  2014-01-17  2:12 ` Jeff Meister
  2014-01-17  2:38 ` Jacques Garrigue
  4 siblings, 1 reply; 16+ messages in thread
From: Nicolas Braud-Santoni @ 2014-01-17  0:43 UTC (permalink / raw)
  To: caml-list

[-- Attachment #1: Type: text/plain, Size: 835 bytes --]

Dear Jürgen,

First, for completeness' sake, the correct URL is
http://www.pfitzenmaier.de/posts/ocaml-considered-dangerous.html

It seems that most of the points in this blog post boil down to your
confusion regarding the signification of 'a in types.
Consider the following:
let x : 'a = 0;;
val x : int = 0

whereas
let x: 'a. 'a = 0;;
Error: This definition has type int which is less general than 'a. 'a

In the first case, 'a is a unification variable, which the compiler may
unify with int.
In the second case, we quantify universally over 'a.

As such, I would say that your claims of unsoundness were rather hasty,
especially given that you follow-up by advertising your services.
Moreover, as Daniel Bünzli pointed out, problem reports are usually done
on the bugtracker.

Kind regards,
Nicolas


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-16 23:00 [Caml-list] ocaml considered dangerous Jürgen Pfitzenmaier
                   ` (2 preceding siblings ...)
  2014-01-17  0:43 ` Nicolas Braud-Santoni
@ 2014-01-17  2:12 ` Jeff Meister
  2014-01-17  2:38 ` Jacques Garrigue
  4 siblings, 0 replies; 16+ messages in thread
From: Jeff Meister @ 2014-01-17  2:12 UTC (permalink / raw)
  To: Jürgen Pfitzenmaier; +Cc: Caml List

[-- Attachment #1: Type: text/plain, Size: 1074 bytes --]

I don't have time to evaluate and respond to all your points, but your
first entry under "frightening discoveries" really jumped out at me. On
line 499:

try closed_type ty with Non_closed (ty0, real) ->

The name "ty0" is a pattern capture variable, which the pattern matching
construct binds to the first argument of the caught exn value with
constructor Non_closed. It doesn't need a prior declaration... you are
declaring it right there. Surely you were simply mistaken? I find it
unbelievable that someone could write OCaml for years, even hacking on the
compiler, without understanding basic pattern matching.


On Thu, Jan 16, 2014 at 3:00 PM, Jürgen Pfitzenmaier <
pfitzen@pfitzenmaier.de> wrote:

>   Dear Ocaml users,
>  I found some serious errors in the compiler e.g. in line 28 of typing/
> includecore.ml
>  and line 499 of typing/ctype.ml of version 3.12.1.
>
>  A longer list of errors with explanations and possible fixes will be
> under
>        www.pfitzenmaier.de/ocaml-considered-dangerous.html
>
>  regards,
>  Jürgen
>
>

[-- Attachment #2: Type: text/html, Size: 1843 bytes --]

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-16 23:00 [Caml-list] ocaml considered dangerous Jürgen Pfitzenmaier
                   ` (3 preceding siblings ...)
  2014-01-17  2:12 ` Jeff Meister
@ 2014-01-17  2:38 ` Jacques Garrigue
  2014-01-17  9:01   ` Gabriel Scherer
  2014-01-18  0:39   ` Jon Harrop
  4 siblings, 2 replies; 16+ messages in thread
From: Jacques Garrigue @ 2014-01-17  2:38 UTC (permalink / raw)
  To: OCaML List Mailing

Let me repost here the answer I sent to Jurgen on the developer’s list.
I wonder why he posted simultaneously to both lists.


First remark, rather than posting such a (broken) link, it would be better
to file a report in the bug tracking system at
	http://caml.inria.fr/mantis/

Second, I’ve read your post (fortunately going to  http://www.pfitzenmaier.de/ let
me access it), and this appears to be a misunderstanding of the meaning of type
annotations in OCaml.
Namely, while type annotations in signatures are universally quantified
(which is why ‘a list = forall ‘a. ‘a list is more general than int list, and your first
example is not accepted), type annotations in expressions are existentially
quantified, i.e. the variables may be instantiated, and as a result your second
example is accepted (int list ref is an instance of ‘a list ref).
Same thing in your third example: the annotation ‘a list -> ‘a just means that
there should be some type a such that get_sum has type a list -> a, and here
that type is int.

If you want annotations in expressions to be universally quantified, you must be
explicit:

 let get_sum : 'a. 'a list -> 'a = A.sum

This one requires get_sum to be polymorphic, and will report an error.

Of course changing line 28 in includecore.ml solves nothing, since this line is
correct from the beginning.

Your examples with polymorphic variants are again a misunderstanding of
how typing works. Namely, in OCaml subtyping is always explicit.
So in F1 you should write:
	let get_count :> [`A] list -> 'a = A.count
(Note that in some case you also need to give the original type of the expression
for subtyping to work properly. Here this is not needed because the target type is
simple enough)

For your frightening discoveries, the definition of ty0 is on line 499… maybe too close
to see.

Last, the current implementation of Printf relies heavily on Obj.magic, which means
that you cannot tell much about the typing by what you see inside the implementation.
To my best knowledge, the exported interface is type safe.
By the way, there is now an implementation of Printf that avoids most of the Obj.magic
by using GADTs. It should be merged soon.

Finally I would suggest not to post such a blog before you discuss the problems
you encountered with somebody (not necessarily the developers, just somebody
knowledgeable enough in OCaml) as this may confuse people in a useless way.
This would also have avoided you to part from OCaml for inexistent reasons...

Best regards,

Jacques Garrigue

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-17  2:38 ` Jacques Garrigue
@ 2014-01-17  9:01   ` Gabriel Scherer
  2014-01-18  0:39   ` Jon Harrop
  1 sibling, 0 replies; 16+ messages in thread
From: Gabriel Scherer @ 2014-01-17  9:01 UTC (permalink / raw)
  To: Jacques Garrigue; +Cc: OCaML List Mailing

> After some investigations it turned out that the Ocaml compiler shows a questionable understanding of type checking.

After immediate reading it turned out that the post author shows a
complete misunderstanding of the type system he's talking about.

It's great that he felt motivated to look at the internals of the
admittedly-complex type checker and experiment with language
extensions. The problem is the arrogance in assuming other people are
wrong.

For anyone interested in understanding the core of the type checker,
there is a very nice presentation by Oleg at
  http://okmij.org/ftp/ML/generalization.html
(It does not cover the issues that are treated here, rather the simple
ML fragment on let-generalization, but it's a start and it helps
understand the way mutation is used in the implementation, which
indeed makes it not a piece of cake.)


On Fri, Jan 17, 2014 at 3:38 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> Let me repost here the answer I sent to Jurgen on the developer’s list.
> I wonder why he posted simultaneously to both lists.
>
>
> First remark, rather than posting such a (broken) link, it would be better
> to file a report in the bug tracking system at
>         http://caml.inria.fr/mantis/
>
> Second, I’ve read your post (fortunately going to  http://www.pfitzenmaier.de/ let
> me access it), and this appears to be a misunderstanding of the meaning of type
> annotations in OCaml.
> Namely, while type annotations in signatures are universally quantified
> (which is why ‘a list = forall ‘a. ‘a list is more general than int list, and your first
> example is not accepted), type annotations in expressions are existentially
> quantified, i.e. the variables may be instantiated, and as a result your second
> example is accepted (int list ref is an instance of ‘a list ref).
> Same thing in your third example: the annotation ‘a list -> ‘a just means that
> there should be some type a such that get_sum has type a list -> a, and here
> that type is int.
>
> If you want annotations in expressions to be universally quantified, you must be
> explicit:
>
>  let get_sum : 'a. 'a list -> 'a = A.sum
>
> This one requires get_sum to be polymorphic, and will report an error.
>
> Of course changing line 28 in includecore.ml solves nothing, since this line is
> correct from the beginning.
>
> Your examples with polymorphic variants are again a misunderstanding of
> how typing works. Namely, in OCaml subtyping is always explicit.
> So in F1 you should write:
>         let get_count :> [`A] list -> 'a = A.count
> (Note that in some case you also need to give the original type of the expression
> for subtyping to work properly. Here this is not needed because the target type is
> simple enough)
>
> For your frightening discoveries, the definition of ty0 is on line 499… maybe too close
> to see.
>
> Last, the current implementation of Printf relies heavily on Obj.magic, which means
> that you cannot tell much about the typing by what you see inside the implementation.
> To my best knowledge, the exported interface is type safe.
> By the way, there is now an implementation of Printf that avoids most of the Obj.magic
> by using GADTs. It should be merged soon.
>
> Finally I would suggest not to post such a blog before you discuss the problems
> you encountered with somebody (not necessarily the developers, just somebody
> knowledgeable enough in OCaml) as this may confuse people in a useless way.
> This would also have avoided you to part from OCaml for inexistent reasons...
>
> Best regards,
>
> Jacques Garrigue
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 16+ messages in thread

* RE: [Caml-list] ocaml considered dangerous
  2014-01-17  2:38 ` Jacques Garrigue
  2014-01-17  9:01   ` Gabriel Scherer
@ 2014-01-18  0:39   ` Jon Harrop
  2014-01-18  2:22     ` Jeremy Yallop
  1 sibling, 1 reply; 16+ messages in thread
From: Jon Harrop @ 2014-01-18  0:39 UTC (permalink / raw)
  To: 'Jacques Garrigue', 'OCaML List Mailing'

> By the way, there is now an implementation of Printf that avoids most of the Obj.magic by using GADTs. It should be merged soon.

Just curious: is that a drop-in replacement?

Cheers,
Jon.

-----Original Message-----
From: caml-list-request@inria.fr [mailto:caml-list-request@inria.fr] On Behalf Of Jacques Garrigue
Sent: 17 January 2014 02:39
To: OCaML List Mailing
Subject: Re: [Caml-list] ocaml considered dangerous

Let me repost here the answer I sent to Jurgen on the developer’s list.
I wonder why he posted simultaneously to both lists.


First remark, rather than posting such a (broken) link, it would be better to file a report in the bug tracking system at
	http://caml.inria.fr/mantis/

Second, I’ve read your post (fortunately going to  http://www.pfitzenmaier.de/ let me access it), and this appears to be a misunderstanding of the meaning of type annotations in OCaml.
Namely, while type annotations in signatures are universally quantified (which is why ‘a list = forall ‘a. ‘a list is more general than int list, and your first example is not accepted), type annotations in expressions are existentially quantified, i.e. the variables may be instantiated, and as a result your second example is accepted (int list ref is an instance of ‘a list ref).
Same thing in your third example: the annotation ‘a list -> ‘a just means that there should be some type a such that get_sum has type a list -> a, and here that type is int.

If you want annotations in expressions to be universally quantified, you must be
explicit:

 let get_sum : 'a. 'a list -> 'a = A.sum

This one requires get_sum to be polymorphic, and will report an error.

Of course changing line 28 in includecore.ml solves nothing, since this line is correct from the beginning.

Your examples with polymorphic variants are again a misunderstanding of how typing works. Namely, in OCaml subtyping is always explicit.
So in F1 you should write:
	let get_count :> [`A] list -> 'a = A.count (Note that in some case you also need to give the original type of the expression for subtyping to work properly. Here this is not needed because the target type is simple enough)

For your frightening discoveries, the definition of ty0 is on line 499… maybe too close to see.

Last, the current implementation of Printf relies heavily on Obj.magic, which means that you cannot tell much about the typing by what you see inside the implementation.
To my best knowledge, the exported interface is type safe.
By the way, there is now an implementation of Printf that avoids most of the Obj.magic by using GADTs. It should be merged soon.

Finally I would suggest not to post such a blog before you discuss the problems you encountered with somebody (not necessarily the developers, just somebody knowledgeable enough in OCaml) as this may confuse people in a useless way.
This would also have avoided you to part from OCaml for inexistent reasons...

Best regards,

Jacques Garrigue

--
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs=


^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-18  0:39   ` Jon Harrop
@ 2014-01-18  2:22     ` Jeremy Yallop
  2014-01-18  7:04       ` Gabriel Scherer
  0 siblings, 1 reply; 16+ messages in thread
From: Jeremy Yallop @ 2014-01-18  2:22 UTC (permalink / raw)
  To: Jon Harrop; +Cc: Jacques Garrigue, OCaML List Mailing

Jacques Garrigue wrote:
>> By the way, there is now an implementation of Printf that avoids most of the Obj.magic by using GADTs. It should be merged soon.

Jon Harrop <jon@ffconsultancy.com> wrote:
> Just curious: is that a drop-in replacement?

Yes, except for some tiny incompatibilities, mostly fixes for bugs
that the development of the GADT version uncovered in the original
implementation.  The patch is here, along with a description and some
discussion:

   http://caml.inria.fr/mantis/view.php?id=6017

The author, Benoît Vaugon, presented the design along with some
performance figures at OCaml 2013:

   http://ocaml.org/meetings/ocaml/2013/proposals/formats-as-gadts.pdf
   http://ocaml.org/meetings/ocaml/2013/slides/vaugon.pdf

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-18  2:22     ` Jeremy Yallop
@ 2014-01-18  7:04       ` Gabriel Scherer
  2014-01-18  9:11         ` David Allsopp
  2014-01-19  6:09         ` oleg
  0 siblings, 2 replies; 16+ messages in thread
From: Gabriel Scherer @ 2014-01-18  7:04 UTC (permalink / raw)
  To: Jeremy Yallop; +Cc: Jon Harrop, Jacques Garrigue, OCaML List Mailing

I guess one could also mention that the no-magic implementation is
notably faster than the current implementation (as it avoids any
format string parsing at runtime), which is not necessarily a concern
for printf (for large output you're probably killed by I/O overhead
anyway) but can be for sprintf or bprintf.

Note that while the current proposal uses GADTs, Benoît also
experimented with reasonable similar designs using higher-order
function (this is the usual initial vs. final tagless interpreter
choice) that would have been implementable before 4.00.

On Sat, Jan 18, 2014 at 3:22 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> Jacques Garrigue wrote:
>>> By the way, there is now an implementation of Printf that avoids most of the Obj.magic by using GADTs. It should be merged soon.
>
> Jon Harrop <jon@ffconsultancy.com> wrote:
>> Just curious: is that a drop-in replacement?
>
> Yes, except for some tiny incompatibilities, mostly fixes for bugs
> that the development of the GADT version uncovered in the original
> implementation.  The patch is here, along with a description and some
> discussion:
>
>    http://caml.inria.fr/mantis/view.php?id=6017
>
> The author, Benoît Vaugon, presented the design along with some
> performance figures at OCaml 2013:
>
>    http://ocaml.org/meetings/ocaml/2013/proposals/formats-as-gadts.pdf
>    http://ocaml.org/meetings/ocaml/2013/slides/vaugon.pdf
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 16+ messages in thread

* RE: [Caml-list] ocaml considered dangerous
  2014-01-18  7:04       ` Gabriel Scherer
@ 2014-01-18  9:11         ` David Allsopp
  2014-01-18  9:28           ` Gabriel Scherer
  2014-01-19  6:09         ` oleg
  1 sibling, 1 reply; 16+ messages in thread
From: David Allsopp @ 2014-01-18  9:11 UTC (permalink / raw)
  To: OCaML List Mailing

Does this new version fix positional specifiers? (http://caml.inria.fr/mantis/view.php?id=4204) or has that rather useful (if never working!) feature been consigned to history?

> -----Original Message-----
> From: caml-list-request@inria.fr [mailto:caml-list-request@inria.fr] On
> Behalf Of Gabriel Scherer
> Sent: 18 January 2014 07:05
> To: Jeremy Yallop
> Cc: Jon Harrop; Jacques Garrigue; OCaML List Mailing
> Subject: Re: [Caml-list] ocaml considered dangerous
> 
> I guess one could also mention that the no-magic implementation is notably
> faster than the current implementation (as it avoids any format string
> parsing at runtime), which is not necessarily a concern for printf (for
> large output you're probably killed by I/O overhead
> anyway) but can be for sprintf or bprintf.
> 
> Note that while the current proposal uses GADTs, Benoît also experimented
> with reasonable similar designs using higher-order function (this is the
> usual initial vs. final tagless interpreter
> choice) that would have been implementable before 4.00.
> 
> On Sat, Jan 18, 2014 at 3:22 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> > Jacques Garrigue wrote:
> >>> By the way, there is now an implementation of Printf that avoids most
> of the Obj.magic by using GADTs. It should be merged soon.
> >
> > Jon Harrop <jon@ffconsultancy.com> wrote:
> >> Just curious: is that a drop-in replacement?
> >
> > Yes, except for some tiny incompatibilities, mostly fixes for bugs
> > that the development of the GADT version uncovered in the original
> > implementation.  The patch is here, along with a description and some
> > discussion:
> >
> >    http://caml.inria.fr/mantis/view.php?id=6017
> >
> > The author, Benoît Vaugon, presented the design along with some
> > performance figures at OCaml 2013:
> >
> >    http://ocaml.org/meetings/ocaml/2013/proposals/formats-as-gadts.pdf
> >    http://ocaml.org/meetings/ocaml/2013/slides/vaugon.pdf
> >
> > --
> > Caml-list mailing list.  Subscription management and archives:
> > https://sympa.inria.fr/sympa/arc/caml-list
> > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> > Bug reports: http://caml.inria.fr/bin/caml-bugs
> 
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-18  9:11         ` David Allsopp
@ 2014-01-18  9:28           ` Gabriel Scherer
  2014-01-18  9:43             ` David Allsopp
  0 siblings, 1 reply; 16+ messages in thread
From: Gabriel Scherer @ 2014-01-18  9:28 UTC (permalink / raw)
  To: David Allsopp; +Cc: OCaML List Mailing

No, it does not. It makes the printf codebase easier to work with (if
you know your GADTs), but lately the tendency has rather been to hope
for *less* complex stuff in formats, rather than more.

On Sat, Jan 18, 2014 at 10:11 AM, David Allsopp <dra-news@metastack.com> wrote:
> Does this new version fix positional specifiers? (http://caml.inria.fr/mantis/view.php?id=4204) or has that rather useful (if never working!) feature been consigned to history?
>
>> -----Original Message-----
>> From: caml-list-request@inria.fr [mailto:caml-list-request@inria.fr] On
>> Behalf Of Gabriel Scherer
>> Sent: 18 January 2014 07:05
>> To: Jeremy Yallop
>> Cc: Jon Harrop; Jacques Garrigue; OCaML List Mailing
>> Subject: Re: [Caml-list] ocaml considered dangerous
>>
>> I guess one could also mention that the no-magic implementation is notably
>> faster than the current implementation (as it avoids any format string
>> parsing at runtime), which is not necessarily a concern for printf (for
>> large output you're probably killed by I/O overhead
>> anyway) but can be for sprintf or bprintf.
>>
>> Note that while the current proposal uses GADTs, Benoît also experimented
>> with reasonable similar designs using higher-order function (this is the
>> usual initial vs. final tagless interpreter
>> choice) that would have been implementable before 4.00.
>>
>> On Sat, Jan 18, 2014 at 3:22 AM, Jeremy Yallop <yallop@gmail.com> wrote:
>> > Jacques Garrigue wrote:
>> >>> By the way, there is now an implementation of Printf that avoids most
>> of the Obj.magic by using GADTs. It should be merged soon.
>> >
>> > Jon Harrop <jon@ffconsultancy.com> wrote:
>> >> Just curious: is that a drop-in replacement?
>> >
>> > Yes, except for some tiny incompatibilities, mostly fixes for bugs
>> > that the development of the GADT version uncovered in the original
>> > implementation.  The patch is here, along with a description and some
>> > discussion:
>> >
>> >    http://caml.inria.fr/mantis/view.php?id=6017
>> >
>> > The author, Benoît Vaugon, presented the design along with some
>> > performance figures at OCaml 2013:
>> >
>> >    http://ocaml.org/meetings/ocaml/2013/proposals/formats-as-gadts.pdf
>> >    http://ocaml.org/meetings/ocaml/2013/slides/vaugon.pdf
>> >
>> > --
>> > Caml-list mailing list.  Subscription management and archives:
>> > https://sympa.inria.fr/sympa/arc/caml-list
>> > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> > Bug reports: http://caml.inria.fr/bin/caml-bugs
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 16+ messages in thread

* RE: [Caml-list] ocaml considered dangerous
  2014-01-18  9:28           ` Gabriel Scherer
@ 2014-01-18  9:43             ` David Allsopp
  2014-01-18  9:59               ` Gabriel Scherer
  0 siblings, 1 reply; 16+ messages in thread
From: David Allsopp @ 2014-01-18  9:43 UTC (permalink / raw)
  To: OCaML List Mailing

Gabriel Scherer wrote:
> David Allsopp wrote:
> > Does this new version fix positional specifiers?
> No, it does not. It makes the printf codebase easier to work with (if you
> know your GADTs),

Shame - it's an absence I find regularly irritating!

	Printf.printf "long-perfectly-readable-multi-line-format-string" id id id id date id id date date id :o)

> but lately the tendency has rather been to hope for *less* complex stuff in formats, rather than more.

Well, for me, the hope was that things that were supposed to have been there (in the docs) might be fixed! The comments closing PRs 3992, 4204, 4290 and 4321 all suggested that a rewrite would hope reintroduce positional specifiers. From the printf perspective, I thought the objective was to match all the implementable parts of ISO C's printf (i.e. skipping only the things which are not type-safe).


David 

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-18  9:43             ` David Allsopp
@ 2014-01-18  9:59               ` Gabriel Scherer
  0 siblings, 0 replies; 16+ messages in thread
From: Gabriel Scherer @ 2014-01-18  9:59 UTC (permalink / raw)
  To: David Allsopp; +Cc: OCaML List Mailing

Right now (in the following weeks) the priority is to finish a
thorough review of the (quite large) proposed patch, and integrate it
in trunk.
After that, you will be welcome to experiment with implementing
propositional parameter and proposing it for integration. Assuming
maintainers are ready to take the feature back (which is not a given),
my intuition is that it would be doable, but you would have to be
careful to have an implementation that does not degrade performances
for formats that do not use the feature.

On Sat, Jan 18, 2014 at 10:43 AM, David Allsopp <dra-news@metastack.com> wrote:
> Gabriel Scherer wrote:
>> David Allsopp wrote:
>> > Does this new version fix positional specifiers?
>> No, it does not. It makes the printf codebase easier to work with (if you
>> know your GADTs),
>
> Shame - it's an absence I find regularly irritating!
>
>         Printf.printf "long-perfectly-readable-multi-line-format-string" id id id id date id id date date id :o)
>
>> but lately the tendency has rather been to hope for *less* complex stuff in formats, rather than more.
>
> Well, for me, the hope was that things that were supposed to have been there (in the docs) might be fixed! The comments closing PRs 3992, 4204, 4290 and 4321 all suggested that a rewrite would hope reintroduce positional specifiers. From the printf perspective, I thought the objective was to match all the implementable parts of ISO C's printf (i.e. skipping only the things which are not type-safe).
>
>
> David
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-18  7:04       ` Gabriel Scherer
  2014-01-18  9:11         ` David Allsopp
@ 2014-01-19  6:09         ` oleg
  1 sibling, 0 replies; 16+ messages in thread
From: oleg @ 2014-01-19  6:09 UTC (permalink / raw)
  To: gabriel.scherer; +Cc: yallop, jon, garrigue, caml-list


> Jacques Garrigue wrote:
> By the way, there is now an implementation of Printf that avoids
> most of the Obj.magic by using GADTs. It should be merged soon.

Perhaps it may be worth mentioning a (quite old actually) paper
        http://okmij.org/ftp/typed-formatting/index.html#derivation

that attempts to _derive_ various typed scanf and printf
implementation, including a couple of new ones. All the code is in
OCaml. Perhaps also relevant is
        http://okmij.org/ftp/typed-formatting/index.html#C-like
which uses Template Haskell to convert a C-like format string into the
proper combinator format. The conversion is syntax-directed rather
than type directed (that is, a simple preprocessor, like ppx). 

In the above developments, the types seem to have fewer type
parameters than what I've seen presented at the OCaml workshop. I am
still not clear about the source of that difference.



^ permalink raw reply	[flat|nested] 16+ messages in thread

* Re: [Caml-list] ocaml considered dangerous
  2014-01-17  0:43 ` Nicolas Braud-Santoni
@ 2014-01-20 10:07   ` Goswin von Brederlow
  0 siblings, 0 replies; 16+ messages in thread
From: Goswin von Brederlow @ 2014-01-20 10:07 UTC (permalink / raw)
  To: caml-list

On Fri, Jan 17, 2014 at 01:43:21AM +0100, Nicolas Braud-Santoni wrote:
> Dear Jürgen,
> 
> First, for completeness' sake, the correct URL is
> http://www.pfitzenmaier.de/posts/ocaml-considered-dangerous.html
> 
> It seems that most of the points in this blog post boil down to your
> confusion regarding the signification of 'a in types.
> Consider the following:
> let x : 'a = 0;;
> val x : int = 0
> 
> whereas
> let x: 'a. 'a = 0;;
> Error: This definition has type int which is less general than 'a. 'a
> 
> In the first case, 'a is a unification variable, which the compiler may
> unify with int.
> In the second case, we quantify universally over 'a.
> 
> As such, I would say that your claims of unsoundness were rather hasty,
> especially given that you follow-up by advertising your services.
> Moreover, as Daniel Bünzli pointed out, problem reports are usually done
> on the bugtracker.
> 
> Kind regards,
> Nicolas

It should also be noted that he claims the compiler produces faulty
programms. But all his examples are about the compiler rejecting some
bit of code that he thinks should be accepted.

So his code, which the compiler currently accepts or he couldn't run
it, crashes and he blames the compiler because other code doesn't get
accepted. Does that make any sense?

Seems to me that the crashes are more likely caused by his tinkering
with the compiler trying to get code accepted that the compiler
currently rejects because they are (or could be) unsound. Punhcing
holes in the type system like that obviously can cause crashes as can
use of Obj.magic to work around the type system.

Dear Jürgen,

Your first half seems to be, as mentioned, about misunderstanding the
type system. You might want to read up on universal and existential
types and unification. I also recommend reading up on the value
restriction, which explains why you sometimes loose polymorphism
unless you lift arguments.

As for your "Frightening discoveries" in the second half of your post:
Ocaml inferes types. Some types are infered by how the function is
declared and some types are infered by how the function (or method) is
USED, esspecially within objects. In the full example the use of the
method lets the compiler infere the right type so everything works.
But when you simplify the example to the point where the use case
disapears that is no longer possible and the compiler tells you so.

This can be surprising and anoying at times but that is how it works.
It does not mean the compiler accepted something in the longer example
that was unsound.

MfG
	Goswin



^ permalink raw reply	[flat|nested] 16+ messages in thread

end of thread, other threads:[~2014-01-20 10:07 UTC | newest]

Thread overview: 16+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-01-16 23:00 [Caml-list] ocaml considered dangerous Jürgen Pfitzenmaier
2014-01-16 23:27 ` Milan Stanojević
2014-01-16 23:33 ` Daniel Bünzli
2014-01-17  0:43 ` Nicolas Braud-Santoni
2014-01-20 10:07   ` Goswin von Brederlow
2014-01-17  2:12 ` Jeff Meister
2014-01-17  2:38 ` Jacques Garrigue
2014-01-17  9:01   ` Gabriel Scherer
2014-01-18  0:39   ` Jon Harrop
2014-01-18  2:22     ` Jeremy Yallop
2014-01-18  7:04       ` Gabriel Scherer
2014-01-18  9:11         ` David Allsopp
2014-01-18  9:28           ` Gabriel Scherer
2014-01-18  9:43             ` David Allsopp
2014-01-18  9:59               ` Gabriel Scherer
2014-01-19  6:09         ` oleg

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).