Why is guile still so slow?

Why is guile still so slow?

[John Lewis]

I don't understand while Guile is so slow. According to these
benchmarks http://www.cs.utah.edu/~mflatt/benchmarks-20100126/log3/Benchmarks.html
GNU Guile is running about a order of magnitude slower than Bigloo,
Chicken, Gambit, Ikarus, Larceny, MIT, and Racket(PLT) with most task.
I am asking why? Are the benchmarks wrong? Is it to keep it portable
and embeddable? No matter the reason, unless the benchmarks aren't
accurate and Guile is faster than it seems, the sluggishness of Guile
is going to make it impossible to use to for application development
no matter how Ubiquitous Guile currently is.

Re: Why is guile still so slow?

[rixed]

-[ Wed, Oct 12, 2011 at 10:54:11AM -0400, John Lewis ]----
> I don't understand while Guile is so slow. According to these
> benchmarks http://www.cs.utah.edu/~mflatt/benchmarks-20100126/log3/Benchmarks.html
> GNU Guile is running about a order of magnitude slower than Bigloo,
> Chicken, Gambit, Ikarus, Larceny, MIT, and Racket(PLT) with most task.

Bigloo, Chicken and Gambit compiles to native code (through C).
I can't tell for the others. This simple fact certainly accounts
for most of the difference.

Also, some (Bigloo for sure, maybe others) have type annotations while
guile currently have not (although this was discussed recently).

Also, as guile now relies on bdwgc for the GC it might suffer from
conservative GC (while other scheme might use a dedicated GC, which
can additionally perform some life span analysis to reduce useless
collection - IIRC Gambit does this... or is it Stalin?). bdwgc is
certainly a big win with regard to code complexity, though.

> the sluggishness of Guile
> is going to make it impossible to use to for application development
> no matter how Ubiquitous Guile currently is.

If so, then there is no application written in Python, Ruby,
Javascript... :-)
Joking aside, maybe guile is too slow for writing whole apps in it,
but it's primary goal is to be an extension language, a companion for
another C/C++ program, or at best an orchestrator of business oriented
code. So performance is not the primary objective. For instance, I'm
using guile as an extension language for a low-level commercial product
for which speed matters, and it's perfect for what it does (configuring
the software, mostly). Using another scheme app would have been less
convenient since they are less easy to link with C code.

Re: Why is guile still so slow?

[Jose A. Ortega Ruiz]

On Wed, Oct 12 2011, rixed@happyleptic.org wrote:

[...]

> Joking aside, maybe guile is too slow for writing whole apps in it,
> but it's primary goal is to be an extension language, a companion for
> another C/C++ program, or at best an orchestrator of business oriented
> code.

I really hope that that's not Guile's primary goal these days (and my
understanding is that it is not): i wouldn't be much interested if those
were its goals ("orchestrator of business oriented code" sounds
particularly dreadful :-)).

Goals aside, Guile 2.x looks to me as a perfectly fine platform to
implement a wide range of applications, and, IMHO, it should be promoted
and developed as such.

But IANAGD :-D

Cheers,
jao
-- 
Substitute damn every time you're inclined to write very; your editor will
delete it and the writing will be just as it should be.
 -Mark Twain, author and humorist (1835-1910)

Re: Why is guile still so slow?

[rixed]

> > but it's primary goal is to be an extension language, a companion for
> > another C/C++ program, or at best an orchestrator of business oriented
> > code.
> 
> I really hope that that's not Guile's primary goal these days (and my
> understanding is that it is not): i wouldn't be much interested if those
> were its goals ("orchestrator of business oriented code" sounds
> particularly dreadful :-)).

By "business oriented code" I meant "business logic", ie. the actual
low level and specialized part of the program. For instance I do system
programming and cannot do it in scheme (whatever the implementation),
although scheme is perfect to control the higher levels of abstraction or
interaction with the user.

"business oriented code" sounds indeed dreadful. I need some vacation
(in an English speaking country for instance). :)

Re: Why is guile still so slow?

[Jose A. Ortega Ruiz]

On Thu, Oct 13 2011, rixed@happyleptic.org wrote:

[...]

>> I really hope that that's not Guile's primary goal these days (and my
>> understanding is that it is not): i wouldn't be much interested if those
>> were its goals ("orchestrator of business oriented code" sounds
>> particularly dreadful :-)).
>
> By "business oriented code" I meant "business logic", ie. the actual
> low level and specialized part of the program. For instance I do system
> programming and cannot do it in scheme (whatever the implementation),
> although scheme is perfect to control the higher levels of abstraction or
> interaction with the user.

Couldn't you use the FFI? I haven't used Guile's yet, but hooking to
inotify in Racket was a breeze...  Of course, if C-level performance is
a requirement, you'd need to switch to a CL compiler ;-)

> "business oriented code" sounds indeed dreadful. I need some vacation
> (in an English speaking country for instance). :)

Barcelona is sunny most of the year, and Wingo speaks quite idiomatic
American and Scheme :)

Cheers,
jao
-- 
To kill time is not murder, it's suicide. -William James (1842-1910)

Re: Why is guile still so slow?

[rixed]

-[ Thu, Oct 13, 2011 at 01:56:32AM +0200, Jose A. Ortega Ruiz ]----
> Couldn't you use the FFI?

While FFI makes indeed things simplier, it's only one part of the story.
Scheme/C integration involves also:

- main() func can be C or Scheme (in order to slowly goes from C to Scheme)
- Scheme runtime must support posix threads so that the important C threads
  are not interrupted by evaluation/compilation/GC

> I haven't used Guile's yet, but hooking to
> inotify in Racket was a breeze...

Nor do I have used FFI from guile myself, but I've seen it used in Andy's
guile-sqlite3 bindings and it's nice. See it here for instance:

https://gitorious.org/guile-sqlite3/guile-sqlite3/blobs/master/sqlite3.scm

> Of course, if C-level performance is
> a requirement, you'd need to switch to a CL compiler ;-)

Many CL compilers are wonderful but there is no reason why a Scheme
compiler can't be made faster. Anyway, you'd have to get rid of the
dynamic type checks and the GC to match C speed, so we won't see this
happen soon.

Re: Why is guile still so slow?

[Andy Wingo]

On Wed 12 Oct 2011 20:56, "Jose A. Ortega Ruiz" <jao@gnu.org> writes:

> On Wed, Oct 12 2011, rixed@happyleptic.org wrote:
>
>> Joking aside, maybe guile is too slow for writing whole apps in it,
>> but it's primary goal is to be an extension language, a companion for
>> another C/C++ program, or at best an orchestrator of business oriented
>> code.
>
> I really hope that that's not Guile's primary goal these days (and my
> understanding is that it is not): i wouldn't be much interested if those
> were its goals ("orchestrator of business oriented code" sounds
> particularly dreadful :-)).
>
> Goals aside, Guile 2.x looks to me as a perfectly fine platform to
> implement a wide range of applications, and, IMHO, it should be promoted
> and developed as such.

FWIW, I agree with Jao here :)  Consider Guile to be a portable Scheme
implementation that works well with existing C code.  Personally, I
write many more Scheme modules and applications than I write C code.

Much respect to the late Ritchie, but C is a dangerous language that has
negative impacts on the real world.  We need to stop writing code that
launches the missiles (or, more likely, installs malicious keylogging
darknets) if your program has an out-of-bounds array write.  Guile helps
people move from C to safe languages, at their own pace :)

Andy
-- 
http://wingolog.org/

A bit further toward the flamewar

[rixed]

-[ Thu, Oct 13, 2011 at 12:22:46PM +0200, Andy Wingo ]----
> Much respect to the late Ritchie, but C is a dangerous language that has
> negative impacts on the real world.  We need to stop writing code that
> launches the missiles (or, more likely, installs malicious keylogging
> darknets) if your program has an out-of-bounds array write.  Guile helps
> people move from C to safe languages, at their own pace :)

Scheme is safer than C, because:

- It has garbage collection, which solves many trivial memory management bugs;
- A buggy program that performs an out-of-bound array access will crash
  at runtime, which is sometime better than to proceed.
- It's much more portable than C, so that porting a program from its
  developer machine to another one is very unlikely to introduce a
  bug.

C is safer than Scheme, because:

- It has no automatic memory management, which avoids a few tricky
  memory leaks;
- A buggy program that performs an out-of-bound array access may proceed
  with wrong data, which is sometime better than to crash at runtime;
- It has a type checker ; if not state of the art, it still stops you
  from using the wrong type in runtime most of the time.

I fail to see why Scheme is intrinsically safer than C, but as I just
learnt the death of Denis Ritchie it might be that I'm emotionally biased,
so to speak.

Re: A bit further toward the flamewar

[Ludovic Courtès]

Hello troll!  ;-)

rixed@happyleptic.org skribis:

> I fail to see why Scheme is intrinsically safer than C

Scheme is strongly, though dynamically typed.  A string is a string, a
number is a number, and they cannot change types anyhow.

C is weakly, though statically typed.  A pointer is a pointer, and it
can point to anything, or be uninitialized.  A pointer is also a number,
and so it can be forged.  Any object can be cast in almost any other
object.

And of course, this is not to mention the many other ways to shoot
oneself in the foot–manual memory management being among the most
prominent–nor the many missing features that prevent higher-level
programming.

My contribution to feeding the troll.  :-)

Ludo’.

Re: A bit further toward the flamewar

[Andy Wingo]

On Thu 13 Oct 2011 16:26, ludo@gnu.org (Ludovic Courtès) writes:

> Hello troll!  ;-)

I think that's a bit harsh ;)

> Scheme is strongly, though dynamically typed.  A string is a string, a
> number is a number, and they cannot change types anyhow.

As time goes on and I learn more things, I wonder how it is that "type"
has gotten so many conflations.  This one certainly has value, but I
guess the CS world uses it in a different way, that types are theorems
about programs.  A program that type-checks is has some corresponding
theorem that has a proof, and proving theorems about a program has value
in terms of reliability, &c.  (It turns out that it doesn't matter much
which theorems are proven!)

Anyway this second, proof side of types, is the side that Scheme does
not have.  C has a stronger story in that regard.

> And of course, this is not to mention the many other ways to shoot
> oneself in the foot–manual memory management being among the most
> prominent

This is what I meant when I said that C was dangerous.  Programs in
Guile have meanings, even seemingly ill-formed programs like

  ((lambda () x))

Because what happens here?  You get an exception.  What happens in C if
you invoke puts without its argument?  You might get a warning, but it
will compile, and at runtime /anything can happen/.

All programs of a sufficient size have bugs.  The question is, what
happens when there is a bug?  In Scheme, the answer isn't usually "the
Chinese/American/German government gets to read your email".  With C it
is.  That is why programming in C is dangerous.

Andy
-- 
http://wingolog.org/

Re: A bit further toward the flamewar

[Linas Vepstas]

On 13 October 2011 10:20, Andy Wingo <wingo@pobox.com> wrote:
> On Thu 13 Oct 2011 16:26, ludo@gnu.org (Ludovic Courtès) writes:
>
> Anyway this second, proof side of types, is the side that Scheme does
> not have.  C has a stronger story in that regard.

Lack of types in scheme has made me day-dream about learning
ocaml or haskell.  My pet peeve about scheme is that, when
maintaining old code, its very very hard to just "know" what type
some lambda is expecting.  And, to me, this makes scheme
sometimes very hard to read.

very-hard-to-read == bug-prone

> This is what I meant when I said that C was dangerous.  Programs in
> Guile have meanings, even seemingly ill-formed programs like
>
>  ((lambda () x))
>
> Because what happens here?  You get an exception.  What happens in C if
> you invoke puts without its argument?  You might get a warning, but it
> will compile, and at runtime /anything can happen/.
>
> All programs of a sufficient size have bugs.  The question is, what
> happens when there is a bug?  In Scheme, the answer isn't usually "the
> Chinese/American/German government gets to read your email".  With C it
> is.  That is why programming in C is dangerous.

If you remember java in 1993-1995, people kept saying that it was safe
because impossible to break out of a java "sandbox".  Of course, that was
wrong: turned out the java sandbox sometimes just had to make library
calls/system calls, and when there were incorrectly implemented, then one
could break out of the sandbox.  I don't see how *any* language can avoid
the same security pitfalls that the java "sandbox" suffered from.

--linas

Re: A bit further toward the flamewar

[Mike Gran]

>>  Anyway this second, proof side of types, is the side that Scheme does
>>  not have.  C has a stronger story in that regard.
> 
> Lack of types in scheme has made me day-dream about learning
> ocaml or haskell.  My pet peeve about scheme is that, when
> maintaining old code, its very very hard to just "know" what type
> some lambda is expecting.  And, to me, this makes scheme
> sometimes very hard to read.
> 
> very-hard-to-read == bug-prone
> 

It is hard to know what types a procedure expects.  I've wondered
why paradigms like the following weren't more popular.
 
(define (func a b)
  (assert-string a)
  (assert-list b)
   ...
 
In the great never-ending Lisp/Scheme flamewar, I always end up
on the "Lisp/Scheme lacks visual clues" side of the argument.  Scheme
is just hard to read.
 
(One project I never seem to get around to is figuring out
guile-reader so I code up Wheeler's sweet-expressions: a better
version of SRFI-49.  That helps the "visual clues" problem. But
that doesn't really help the type-check contract problem.)
 
I would add that most scheme distributions have very limited debugging
facilities as compared to most C debuggers.  Guile has improved quite
a bit, but, it is not gdb.
 
Personally I tend to fall back on 'debug by print' paradigms with scheme.
 
-Mike Gran

Re: A bit further toward the flamewar

[Linas Vepstas]

On 13 October 2011 13:37, Mike Gran <spk121@yahoo.com> wrote:
>
>>>  Anyway this second, proof side of types, is the side that Scheme does
>>>  not have.  C has a stronger story in that regard.
>>
>> Lack of types in scheme has made me day-dream about learning
>> ocaml or haskell.  My pet peeve about scheme is that, when
>> maintaining old code, its very very hard to just "know" what type
>> some lambda is expecting.  And, to me, this makes scheme
>> sometimes very hard to read.
>>
>> very-hard-to-read == bug-prone
>>
>
> It is hard to know what types a procedure expects.  I've wondered
> why paradigms like the following weren't more popular.
>
> (define (func a b)
>   (assert-string a)
>   (assert-list b)
>    ...
>
> In the great never-ending Lisp/Scheme flamewar, I always end up
> on the "Lisp/Scheme lacks visual clues" side of the argument.  Scheme
> is just hard to read.

In the code that I work on, in (func a b), its rarely the case that a
and b are merely strings or lists; they're usually some fairly complex
structure, where e.g. 'b' is a list where car and cadr must be
strings, and caddr may or may not be another list, with certain
expectations about car, cadr, etc.

I have no clue why it never occurred to me to use the above paradigm,
I will definitely start experimenting with it.

Any clue on how to indicate that func returns type 'X' ?

I don't know if you were trying to make this point but: if one were to
code in the above paradigm, and also throw some srfi-9000 syntactic
sugar at it, one might  be able to get something that resembled
ocaml/haskell type declarations.  And, for the code that I deal with,
this might be the bees knees.

--linas

Re: A bit further toward the flamewar

[dskr]

I use procedure properties for this purpose. I assign a predicate that matches the return values as a property. Predicates are, of course, the types in Scheme.

Sent from my iPad

On Oct 13, 2011, at 5:42 PM, Linas Vepstas <linasvepstas@gmail.com> wrote:

> Any clue on how to indicate that func returns type 'X' ?

Re: A bit further toward the flamewar

[Ian Price]

Linas Vepstas <linasvepstas@gmail.com> writes:

> I have no clue why it never occurred to me to use the above paradigm,
> I will definitely start experimenting with it.
>
> Any clue on how to indicate that func returns type 'X' ?
>
> I don't know if you were trying to make this point but: if one were to
> code in the above paradigm, and also throw some srfi-9000 syntactic
> sugar at it, one might  be able to get something that resembled
> ocaml/haskell type declarations.  And, for the code that I deal with,
> this might be the bees knees.

Just because scheme doesn't have type declarations doesn't mean you
can't add them. I often write code that looks like

; partition : (A -> Boolean) Listof(A) -> Listof(A) Listof(A)
(define (partition pred list) ...)

and I also make heavy use of 'assert', and less frequently, a macro of
mine called 'assert-lambda' which looks like

(lambda ((a procedure?) (b list?)) ...)

I don't, in general, check return types, but I do try and make sure that
they obey the declaration comment. Having a built-in type/contract
syntax, like Racket has, would be nice as I could move these comments
into code, but this is better than nothing.

-- 
Ian Price

"Programming is like pinball. The reward for doing it well is
the opportunity to do it again" - from "The Wizardy Compiled"

Re: A bit further toward the flamewar

[Andy Wingo]

On Fri 14 Oct 2011 03:07, Ian Price <ianprice90@googlemail.com> writes:

> Just because scheme doesn't have type declarations doesn't mean you
> can't add them. I often write code that looks like
>
> ; partition : (A -> Boolean) Listof(A) -> Listof(A) Listof(A)
> (define (partition pred list) ...)

I can't find the source right now, but I think it was Matthias Felleisen
who gave a variant of Greenspun's tenth law, that "any sufficiently
complex Lisp program has a buggy, incomplete ML program in the
comments".

;-)

Andy
-- 
http://wingolog.org/

Re: A bit further toward the flamewar

[Linas Vepstas]

On 13 October 2011 20:07, Ian Price <ianprice90@googlemail.com> wrote:
> Linas Vepstas <linasvepstas@gmail.com> writes:
>
>> I have no clue why it never occurred to me to use the above paradigm,
>> I will definitely start experimenting with it.
>>
>> Any clue on how to indicate that func returns type 'X' ?
>>
>> I don't know if you were trying to make this point but: if one were to
>> code in the above paradigm, and also throw some srfi-9000 syntactic
>> sugar at it, one might  be able to get something that resembled
>> ocaml/haskell type declarations.  And, for the code that I deal with,
>> this might be the bees knees.
>
> Just because scheme doesn't have type declarations doesn't mean you
> can't add them. I often write code that looks like
>
> ; partition : (A -> Boolean) Listof(A) -> Listof(A) Listof(A)
> (define (partition pred list) ...)
>
> and I also make heavy use of 'assert', and less frequently, a macro of
> mine called 'assert-lambda' which looks like
>
> (lambda ((a procedure?) (b list?)) ...)
>
> I don't, in general, check return types, but I do try and make sure that
> they obey the declaration comment. Having a built-in type/contract
> syntax, like Racket has, would be nice as I could move these comments
> into code, but this is better than nothing.

Well, I see two choices:
1) Let the conversation slide, and incorporate above thoughts as 'best
practices' into my code.
2) Flame-war.

In the spirit of 2),

Andy Wingo wrote:
> I can't find the source right now, but I think it was Matthias Felleisen
> who gave a variant of Greenspun's tenth law, that "any sufficiently
> complex Lisp program has a buggy, incomplete ML program in the
> comments".

So the proposal is: (shout me down, when ready): create a new srfi,
defining an ML-like conception of types, so that scheme functions can
be annotated with types. The goal here is not so much to do
type-checking at run-time, but to allow static type checking.   That
is, one could create a "type checker tool", which one could invoke
ad-hoc, during development, to make sure that my scheme programs are
consistent with their handling of types. This is static type checking
--  as, for the most part, I am not interested in type-checking during
runtime, for two reasons: performance, and also because I want to
avoid the hard-to-debug problem where I only pass the wrong type only
once in a million.

Basically, as a debugging/development tool, everything I've read about
ML (e.g. the Jane's street commentary) is that the static
type-checking in ML is a powerful means of avoiding developer errors.
It'd be neat if I could get this feature in scheme.

BTW, as a token nod to C: please be aware that the Linux Kernel folks
have been busy creating and extending a static type-checking system
for C, which is used extensively in the linux kernel sources. The goal
there is to avoid accidentally passing user-space pointers into the
kernel (where they are invalid), and to avoid calls to __init routines
during runtime (because they no longer exist after initialization).
Note that this kind of type-checking is not possible in "ordinary" C.
I can't comment on how "well-designed" the system is, but it has been
very effective in finding zillions of bugs in the linux kernel.

--linas

Re: A bit further toward the flamewar

[Andy Wingo]

On Fri 14 Oct 2011 18:23, Linas Vepstas <linasvepstas@gmail.com> writes:

> 2) Flame-war.
>
> In the spirit of 2),

Whee!

(I generally avoid flamewars, but this one has not caught fire yet :)

> So the proposal is: (shout me down, when ready): create a new srfi,
> defining an ML-like conception of types, so that scheme functions can
> be annotated with types.

I suggest instead taking a look at Typed Racket, from the PLT folks.
They have done a lot of good thinking there.

Andy
-- 
http://wingolog.org/

Re: A bit further toward the flamewar

[Andy Wingo]

On Thu 13 Oct 2011 23:42, Linas Vepstas <linasvepstas@gmail.com> writes:

> In the code that I work on, in (func a b), its rarely the case that a
> and b are merely strings or lists; they're usually some fairly complex
> structure, where e.g. 'b' is a list where car and cadr must be
> strings, and caddr may or may not be another list, with certain
> expectations about car, cadr, etc.

In this case, I find `match' to be useful.  The structure of the pattern
matches the structure of the input data, so it is much better than
cadaddring down a list.

Andy
-- 
http://wingolog.org/

Re: A bit further toward the flamewar

[Linas Vepstas]

On 14 October 2011 03:28, Andy Wingo <wingo@pobox.com> wrote:
> On Thu 13 Oct 2011 23:42, Linas Vepstas <linasvepstas@gmail.com> writes:
>
>> In the code that I work on, in (func a b), its rarely the case that a
>> and b are merely strings or lists; they're usually some fairly complex
>> structure, where e.g. 'b' is a list where car and cadr must be
>> strings, and caddr may or may not be another list, with certain
>> expectations about car, cadr, etc.
>
> In this case, I find `match' to be useful.  The structure of the pattern
> matches the structure of the input data, so it is much better than
> cadaddring down a list.

Let me demonstrate my ignorance: what pattern-matching srfi
should I be using?  Last time I looked at 'match' in scheme, it was
defined in some decades-old white paper

Pattern Matching for Scheme
http://download.plt-scheme.org/doc/103p1/pdf/match.pdf

which didn't seem to be widely used anywhere.  Are you saying that we
have this hidden somewhere inside of guile???

--linas

Re: A bit further toward the flamewar

[Andy Wingo]

On Fri 14 Oct 2011 18:30, Linas Vepstas <linasvepstas@gmail.com> writes:

> Let me demonstrate my ignorance: what pattern-matching srfi
> should I be using?

See "Pattern Matching" in the manual.

Andy
-- 
http://wingolog.org/

Re: A bit further toward the flamewar

[Hans Aberg]

On 13 Oct 2011, at 18:30, Linas Vepstas wrote:

> On 13 October 2011 10:20, Andy Wingo <wingo@pobox.com> wrote:
>> On Thu 13 Oct 2011 16:26, ludo@gnu.org (Ludovic Courtès) writes:
>> 
>> Anyway this second, proof side of types, is the side that Scheme does
>> not have.  C has a stronger story in that regard.
> 
> Lack of types in scheme has made me day-dream about learning
> ocaml or haskell.

The Haskell Hindley-Milner type system, as implemented, prevents function name overloading except in the form of classes, which in effect steal function names. Getting around it by not loading or rewriting those classes has in practice proven to be too cumbersome.

Hans

Re: A bit further toward the flamewar

[Panicz Maciej Godek]

Could add some tiny fire drops to this flame, I'd say that
the readability and error-proneness of scheme programs
really depends on what you're doing (and on how you're
doing it)

I don't have any experience with any industrial application
of scheme and I am using it only for the purpose of fun
and cheerful hacking, and what I find really great about
it is that it really allows the top-bottom approach, so that
you can write a sentence that really resembles a sentence
of a natural language (and is therefore amazingly readable)
and then explain all the notions involved, until you reach
the level of some data representation (which could be really
chosen differently).

And this is a true joy to read.

I don't know much about  ML nor Ocaml, but I thought
the flame was supposed to be about scheme vs. C ;-)

And I think that, to some extent, C imposes on the programmer
a certain style of thinking -- that you really have to focus on the data
representation before you consider the logics of the program.
On the other hand, scheme also allows this scheme, and some
solutions for type checking indeed do pop out (like the aforementioned
racket, or bigloo, or -- not to look too far -- GOOPS and COOPS)

I think it was Peter Norvig who stated that C is a specialized language
for memory management and computer hardware stuff, and lisp is actually
a general-purpose programming language. The development of UNIX proves,
that there are some domains where C is irreplaceable, basically because
it gives you a fair abstraction over the existing computer hardware.

Lisp, on the other hand (and scheme particularly) is a fair abstraction
over the concept of programming. And still, there are cetrain things that
are best done in perl and which I would find annoying if I was supposed
to do them in scheme.

Yet Another Troll

Re: A bit further toward the flamewar

[Ludovic Courtès]

Hello!

Andy Wingo <wingo@pobox.com> skribis:

> Anyway this second, proof side of types, is the side that Scheme does
> not have.  C has a stronger story in that regard.

Right; but let’s not oversell C.  ;-)  Lisps are definitely closer to
automated theorem provers than C.  ACL2 and αleanTAP come to mind.

Ludo’.

Re: A bit further toward the flamewar

[rixed]

Your critique about C values that can be made invalid (through lack of
proper initialization or erroneous cast) are of course valid but sounds
quite rhetorical, since in practice, in my experience, this does not
cause many bugs (yet I'm sure you could site several examples of such
bugs).  What's of more practical importance to me is that when you
change a data structure somewhere you can be confident that the compiler
will spot every other places where your changes require other changes.
You have not this safety with Scheme, and this is much more problematic
; again, in my experience.  You have to run your code with all possible
inputs in order to make certain that you did not forget to propagate
your changes somewhere. This happened to me again two weeks ago when I
decided that my small guile-agentx library should use bytevectors
instead of strings to read/write from the socket. This small change had
many other small impacts but I was alone to find them, had to run the
code in many different situation to test many path before I gained
enough confidence that I didn't forgot some string operation somewhere
- yet this is a very small library!

Of course, I'm a beginner in Scheme so that might explain why my brain
lacks the necessary equipment to typecheck myself ; while my first
hello.c was written more than 20 years ago so maybe that's why I find C
quite safe in practice.

So, all in all, who knows? But I for sure would like to see type
annotations added in guile some day :-)

Re: A bit further toward the flamewar

[Ludovic Courtès]

Hi,

rixed@happyleptic.org skribis:

> What's of more practical importance to me is that when you
> change a data structure somewhere you can be confident that the compiler
> will spot every other places where your changes require other changes.
> You have not this safety with Scheme, and this is much more problematic
> ; again, in my experience.  You have to run your code with all possible
> inputs in order to make certain that you did not forget to propagate
> your changes somewhere.

Yes, you’re right.  Having the compiler type-check parts of all your
program is a win, no doubt about it.

Nevertheless, type safety can be viewed as one of the many properties of
a program one could want to prove or test.

Did you know that Coq would only compile a function when it can prove
that it terminates?  That’s another kind of compiler-supported proof one
quickly gets used to.

Thanks,
Ludo’.

Re: A bit further toward the flamewar

[Hans Aberg]

On 13 Oct 2011, at 23:14, Ludovic Courtès wrote:

> Did you know that Coq would only compile a function when it can prove
> that it terminates?  That’s another kind of compiler-supported proof one
> quickly gets used to.

Termination is a non-deducable property. They look at a intuitionistic subset of programs.

Hans

Re: A bit further toward the flamewar

[Ludovic Courtès]

Hans Aberg <haberg-1@telia.com> skribis:

> On 13 Oct 2011, at 23:14, Ludovic Courtès wrote:
>
>> Did you know that Coq would only compile a function when it can prove
>> that it terminates?  That’s another kind of compiler-supported proof one
>> quickly gets used to.
>
> Termination is a non-deducable property. They look at a intuitionistic subset of programs.

Sorry, I’m not sure what you mean.

What I had in mind is what they call “well-founded recursion” [0] and
the idea that a recursive function must have a “decreasing argument” [1].

Thanks,
Ludo’.

[0] http://coq.inria.fr/refman/Reference-Manual005.html#htoc79
[1] http://coq.inria.fr/refman/Reference-Manual003.html#Fixpoint

Re: A bit further toward the flamewar

[Hans Aberg]

On 14 Oct 2011, at 11:28, Ludovic Courtès wrote:

>>> Did you know that Coq would only compile a function when it can prove
>>> that it terminates?  That’s another kind of compiler-supported proof one
>>> quickly gets used to.
>> 
>> Termination is a non-deducable property. They look at a intuitionistic subset of programs.
> 
> Sorry, I’m not sure what you mean.

If one adds non-termination to the set of all programs, it is not possible to make an algorithm that tells exactly which programs that avoid it, though it may be possible to prove it for some of them.

> What I had in mind is what they call “well-founded recursion” [0] and
> the idea that a recursive function must have a “decreasing argument” [1].

I was looking at the normalization property*).

> [0] http://coq.inria.fr/refman/Reference-Manual005.html#htoc79
> [1] http://coq.inria.fr/refman/Reference-Manual003.html#Fixpoint

This is essentially mathematical induction. More general, one might use ordinals (I wrote some Haskell code.)

Hans


*)
http://en.wikipedia.org/wiki/Coq
http://en.wikipedia.org/wiki/Calculus_of_inductive_constructions
http://en.wikipedia.org/wiki/Calculus_of_constructions
http://en.wikipedia.org/wiki/Normalization_property_(lambda-calculus)

Re: A bit further toward the flamewar

[rixed]

> Did you know that Coq would only compile a function when it can prove
> that it terminates?  That???s another kind of compiler-supported proof one
> quickly gets used to.

It's funny how researchers are concerned by proofs that a program
terminates, while most engineers try hard everyday to design programs so
that they never terminates (unexpectedly). :)

I realize we merely don't work in the same fields.  I always write
trivial softwares that handle complex data structures and internal
states, while you probably, both as a researcher and a guile hacker, are
more used to write complex softwares manipulating in non-trivial ways
mere lists of symbols.

So I'm very interested in static type checking while, for instance,
I never fear that one of my simple for-loop may not terminate ; but I
understand that you could be very interested in Coq proving that a
complex recursive algorithm eventually terminates, while you don't care
much about the type checking.

Re: A bit further toward the flamewar

[Ludovic Courtès]

Howdy,

rixed@happyleptic.org skribis:

> but I
> understand that you could be very interested in Coq proving that a
> complex recursive algorithm eventually terminates, while you don't care
> much about the type checking.

Actually, I just meant to say that type-checking is one of the many
checks one may want the compiler to perform automatically.

Ludo’.

Re: Why is guile still so slow?

[Andy Wingo]

Hi John,

Some notes.

1. Speed is always relative.  Guile is faster than CPython or MRI.  It
is slower than V8.  Implementations can't be slow or fast; they can only
be slower than X or faster than Y.

2. Widespread Ruby usage proves that speed is not the most important
thing.  V8 proves that "slow languages" can be made fast.  Things
change; focus on expressiveness and what you want to do.

3. The benchmarks you mention are old.  Guile has improved since then.

5. Benchmark speed is but one kind of speed.  There are others:  startup
time, development time, etc.

4. Guile is slower than Ikarus because Guile compiles to bytecode, and
Ikarus to native code.  Native code will come at some point, but don't
hold your breath.

Finally, on the meta-level, you appear to be suffering from
market-induced anxiety.  If you prefer another implementation or
language, by all means, go and use it.  But if you prefer Guile, don't
worry about the others.  Problems get fixed over time with hacking.

Regards,

Andy
-- 
http://wingolog.org/

Re: Why is guile still so slow?

[John Lewis]

Thank you for the responses everybody.