Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.forth > #15078 > unrolled thread
| Started by | visualforth@rocketmail.com |
|---|---|
| First post | 2012-08-21 21:43 -0700 |
| Last post | 2012-08-22 07:37 -0700 |
| Articles | 20 on this page of 163 — 19 participants |
Back to article view | Back to comp.lang.forth
Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-21 21:43 -0700
Re: Comparative Productivity of Programming Languages "A. K." <akk@nospam.org> - 2012-08-22 07:07 +0200
Re: Comparative Productivity of Programming Languages Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-22 03:35 -0500
Re: Comparative Productivity of Programming Languages John Passaniti <john.passaniti@gmail.com> - 2012-08-22 14:06 -0700
Function Points (was: Comparative Productivity of Programming Languages) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-23 14:50 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-23 11:43 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-25 14:13 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 10:12 -0700
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-25 15:39 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 15:09 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 12:34 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 16:43 -0700
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-25 18:05 -0700
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-25 20:34 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-26 03:24 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 22:44 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 21:19 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 00:36 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 21:50 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 01:08 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-26 23:20 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 19:33 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-27 13:34 -0500
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-27 22:38 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 02:45 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 18:14 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 18:24 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:22 +0000
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 03:07 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-28 08:18 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 12:15 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-28 23:05 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-29 03:55 -0500
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-27 22:28 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 20:26 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-28 23:17 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 01:13 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 02:23 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 02:59 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 22:18 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 20:44 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-31 01:29 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-31 09:33 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 02:58 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 19:39 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:10 +0000
Re: Function Points gavino_himself <visploveslisp@gmail.com> - 2012-08-30 20:08 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-30 17:47 -1000
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-27 13:43 -1000
Re: Function Points "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> - 2012-08-27 12:14 +0100
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-08-27 05:12 -0700
Re: Function Points "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> - 2012-08-27 15:52 +0100
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-26 13:09 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 20:52 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:08 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-30 10:43 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-30 08:25 -1000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 22:42 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 01:23 -0400
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-31 03:08 -0500
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 18:56 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 02:35 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-31 23:52 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:27 +0000
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:18 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 17:45 +0200
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 16:14 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 19:13 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-09-02 03:19 -0500
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:18 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:04 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 04:02 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 17:40 +0200
Re: Function Points jim@rainbarrel.com - 2012-09-02 10:32 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 20:49 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:33 -0400
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 17:03 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 09:02 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:35 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 13:42 -1000
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:54 -0700
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-09-03 00:29 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:30 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 21:21 -1000
Re: Function Points jim@rainbarrel.com - 2012-09-03 10:37 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-04 07:14 +0000
Re: Function Points Coos Haak <chforth@hccnet.nl> - 2012-09-03 21:12 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 17:32 -0400
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 17:51 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-03 22:37 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-04 04:25 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-04 07:35 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-05 02:13 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-04 20:18 -1000
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-05 10:56 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-05 16:11 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-05 14:07 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:27 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 00:52 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-02 16:28 -0700
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:48 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 20:21 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 14:45 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:12 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 21:26 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:06 -0400
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-08-31 03:29 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-31 10:35 +0000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 18:49 -0400
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:49 +0000
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-01 08:36 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:11 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 01:58 +0200
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 17:54 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:19 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:05 +0200
Re: Function Points Coos Haak <chforth@hccnet.nl> - 2012-08-31 23:10 +0200
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-31 15:50 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-01 10:31 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 21:52 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:36 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-01 14:36 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:30 +0200
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 23:15 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-02 15:02 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 01:50 +0200
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:57 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-03 23:11 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-04 14:30 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-04 10:14 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-04 22:10 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 00:19 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-06 17:48 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 12:01 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-06 22:02 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 14:19 -0700
Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-07 11:30 +0000
Re: Heap (was: Function Points) Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-07 18:12 +0200
Re: Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-07 16:48 +0000
Re: Heap (was: Function Points) Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-07 21:34 +0200
Re: Heap Gerry Jackson <gerry@jackson9000.fsnet.co.uk> - 2012-09-07 22:04 +0100
Re: Heap anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-08 11:52 +0000
Re: Heap Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-08 22:48 +0200
Re: Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-08 12:11 +0000
priority queue (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-03 11:46 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 15:03 +0200
Re: Function Points mhx@iae.nl (Marcel Hendrix) - 2012-09-03 22:36 +0200
Re: Function Points mhx@iae.nl (Marcel Hendrix) - 2012-09-06 20:27 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-09-02 04:00 -0500
Re: Function Points visualforth@rocketmail.com - 2012-09-03 10:40 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 20:26 +0200
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-27 11:49 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 09:16 -0700
Re: Function Points Josh Grams <josh@qualdan.com> - 2012-08-28 22:46 +0000
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-28 16:06 -0700
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-28 20:50 -0400
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-26 12:59 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 22:24 -0700
Re: Function Points (was: Comparative Productivity of Programming Languages) John Passaniti <john.passaniti@gmail.com> - 2012-08-23 15:02 -0700
Re: Function Points (was: Comparative Productivity of Programming Languages) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-25 14:57 +0000
Re: Comparative Productivity of Programming Languages "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-22 08:07 -0400
Re: Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-22 08:12 -0700
Re: Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-22 07:37 -0700
Page 2 of 9 — ← Prev page 1 [2] 3 4 5 6 7 8 9 Next page →
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-26 23:20 +0200 |
| Subject | Re: Function Points |
| Message-ID | <1454970.h5ifmF2e1c@sunwukong.fritz.box> |
| In reply to | #15166 |
Paul Rubin wrote:
> Are you talking about compiling programs of similar size, on similar
> hardware, with compilers that do similar levels of optimization? It's
> certainly plausible that given more CPU power, fancy compilers will
> use it to do more optimization and automation, rather than just doing
> the same stuff as before and finishing sooner.
No, I'm comparing a bloated Java+C++ project to a non-bloated Forth
project. But even when I compare two non-bloated projects, GCC is
hellish slow.
> Maybe you should try TCC (tinycc.org) for development builds.
> It's around 10x faster than GCC, though the output code is nowhere
> near as optimized.
Unfortunately, TCC is also lacking features. And using a different
compiler for debug builds than for production builds is a bad idea - if
you run into bugs of the production build compiler, what do you do then?
The usual Forth approach to coding is making small incremental changes,
because then you don't have to search long for the reasons why it
doesn't work - it's very likely the small change you just did now.
>> That also guides to my most-used debugging method: Inserting ~~ in
>> suspicious places.
>
> This still takes a lot of runs of the program and possible creation of
> new test cases, which can be pretty tedious.
Well, it does not feel "a lot" if you can do these runs pretty quickly.
>>> IMHO Haskell's type system makes it practical to program in a style
>>> that while not impossible, would be much harder to manage in
>>> Forth....
>> I'm not sure why you claim it is error-prone and to be avoided....
>> Forth is a programming language which tells you to avoid unnecessary
>> abstractions.
>
> Right, the reason it tells you to avoid unnecessary abstractions is
> that using abstraction in Forth is error-prone.
No, that's not the case. You should avoid unnecessary abstractions
since they don't pay off. You can use necessary abstractions, and are
encouraged to do so.
> I wasn't thinking really
> of postpone and create/does, but more of a style where you pass around
> execution tokens a lot, and those xt's may take other xt's as
> arguments
> to invoke over generic data structures, and so on.
After I added quotations to my system, I started doing that regularly.
Not exactly as in Haskell, but MINOS, using an OOP system, does that
sort of stuff. Juggling around many things on the stack is bad Forth
code, so pass xts around that take another xts quite likely will result
in many parameters on the stack. Don't do that.
The OOP system I use in MINOS handles that: You pack the several xts
into one class, and use that. No need for several xts flying around,
the class framework wrap them up into one entity, which is much easier
to pass around.
> In Haskell, it's
> natural to program that way, and the code still feels solid. In
> Scheme or Python you can write basically the same code, but with no
> type system watching over you, it feels like walking on a tightrope
> without a safety net.
Don't fear the program crash! As I said, in a strong typed language, I
feel like in a straightjacket. I wouldn't walk a tightrope in such a
language, regardless of safety net or not.
> I've programmed that way in Forth a little bit, but have been
> advised against it.
>
>> No type system prevents programs from going wrong.
>
> Well, I'd say a well-typed program, including something like Lisp with
> runtime type-checking, can at least have well-defined semantics, while
> an untyped (e.g. Forth or C) program can go completely into the weeds
> if there is a type error (such as a subscript overflow).
A subscript overflow is not exactly a type error.
>> It applies a number of low-hanging fruit checks,
>
> Haskell typechecking can be quite powerful. I like this example:
> https://gist.github.com/2659812
>
> Explanation: Red-black trees are binary trees with the following
> invariants:
> 1. Each internal node is colored either red or black.
> All leaves are black and the root is black.
> 2. All children of red nodes must be black. Black nodes can
> have children of either or both colors.
> 3. All paths from the root to the leaf contain the
> same number of black nodes.
>
> This means the tree is approximately balanced: any path from the root
> to a leaf contains n black nodes, and between 0 and n red nodes, so
> the
> worst case search depth is no more than 2x the best case. You can't
> get
> a completely lopsided tree. To insert or delete a node, you have to
> do somewhat complicated juggling operations ("tree rotations") to
> preserve the invariants, and it's easy to make mistakes coding these
> operations. The C++ implementation that I looked at has assert
> statements that check at runtime that the code didn't hit some weird
> edge case that messed the
> invariants up. Even after extensive testing, the assert statements
> are still there in the program.
>
> It turns out to be pretty straightforward to express those invariants
> as
> a Haskell datatype (seen in the url above). Any value belonging to
> the
> type must be a properly balanced tree. That means that the juggling
> code cannot possibly mess up the invariants. Any attempt to make an
> unbalanced tree will cause a type-checking error, and the program
> won't
> compile.
That's exactly what I don't like. This is a rather complicated thing,
and I'm sure neither of us will write a perfect program first time. As
I try to write incremental programs, my first approach to a r/b tree
would be a general tree program, and let the tree be as unbalanced as I
like. If this works, I would start adding balancing rotation
operations, one after the other (you know, there are several cases you
have to think about). Each of them is tested, but of course, the tree
will still be lopsided.
Maybe you can do that in Haskell, too, by just trying with the full
blown type, and doing the test runs with a reduced type information,
which doesn't care about balancing.
> It would be pointless to have assert statements in the
> executable since the compiler has statically verified that the
> asserted
> conditions hold. I would not call this low-hanging fruit. It's a
> sophisticated condition being checked, that's a source of bugs in
> other real-world implementations, and the compiler verifies it to
> higher confidence than even quite a lot of unit tests could give.
>
> As an even more extreme example, Coq's type system is even stronger
> than Haskell's: it can express any mathematical proposition, so it has
> to be Turing complete, meaning it can't do inference and you have to
> manually
> supply type derivations (which is tedious). But it can encode (for
> example) the semantics of assembly code fragments (Hoare triples) as
> types. So if you have a compiler optimization pass that is annotated
> to take one fragment and returns another fragment of the same type,
> the Coq typechecker is able to verify that the input and output have
> the same semantics and the optimization pass has not introduced any
> semantic
> bugs. I think I mentioned before, a sizable part of a C compiler has
> been written that way (CompCert). This is not low hanging fruit at
> all. It is probably the future, especially as better automation
> becomes available for developing this sort of code.
Calling this still a "type system" is a misnomer. Yes, this is no low-
hanging fruit, but as you said, it is also tedious to use. And if
that's useful during development depends on the error message. Let's
say I have a code transformation pattern
BEGIN code WHILE REPEAT -> BEGIN code UNTIL
to skip the empty part between WHILE and REPEAT, the transformation is
wrong, because the flag for WHILE means the opposit as for UNTIL. If
the code system tells me just "your transformation is wrong", then I
have no clue why, and can only guess. If I unit-test this thing, I'd
give it a simple task and look at the results, and since the results are
runable programs, I'll see why the two are different.
>> while at the same time putting a straitjacket onto the programmer.
>> At least that's how I feel when I program in a language with a strong
>> type system. The compiler tells me "no, you can't do this", and "no,
>> you can't do that".
>
> I never felt terribly straitjacketed programming in C, but I also felt
> that the type system wasn't helping me that much.
C has no really strong type system. A type mismatch usually results in
a warning, it doesn't even fail to compile. I'm not that much
complaining about C, C's type system is more a simple operator
overloading system than anything else.
> I was comfortable
> programming with lots of void*'s, and programming in Lisp with runtime
> types. Trying Haskell was really eye-opening for me. I'm a long way
> from being a Haskell expert but I find it tremendously interesting and
> different (whether that means "better" is of course a separate
> matter).
Yes, of course. It is quit different.
>>> http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/
>> Performance is not a problem? Come on. I'm constantly seeing
>> software which is slow as molasses,
>
> He's talking about compiled code with runtime type checks, vs.
> compiled code that has been statically checked but otherwise does the
> same stuff,
> e.g. Lisp vs ML. If the compiler is any good, the performance
> difference is usually a small constant factor, maybe just a few
> percent. The large, order-of-magnitude slowdowns you're seeing in the
> examples you mention are due to architectural issues in the slow
> programs.
Yes. Usually several architectural issues stacked on each others, like
using a complicated delegate-style OOP program (nobody really wants to
solve the problem, so it gets delegated over and over again) on top of a
slow Java VM with a bad JIT - if there is a JIT at all.
>> What I think would be worth to do for analytic compilers which track
>> that information anyways: Have a stack effect checker.
>
> Yes, that would have caught my + vs. F+ bugs. StrongForth does
> that sort of checking as you're probably aware.
It does a bit more, and there's even a version which runs on top of
Gforth.
>> Warnings when it doesn't match, please, it should compile, because
>> running it (with inserted ~~) will identify the problem quickly.
>
> GHC now has a command-line option that lets it produce executable code
> even if the program has type errors. You then get a runtime error
> only
> if the program tries to actually evaluate an ill-typed expression.
Nice. This allows you to check what actually happens.
> This turns out to be handy during development even though the compiler
> has
> already told you where the errors are. It's sometimes useful to be
> able test the successfully compiling parts of your program right away,
> postponing dealing with the unsuccessful parts til later.
Given that fact, I'm less opposed than before. How useful is GHCi (the
interactive command line)?
>> Forth's interactivity and abstraction avoidance is what makes it
>> strong. Interactivity is more than just a command line promt, it
>> also
>> means that you can recompile quickly. "Blink", not "lunch".
>
> I sometimes like to imagine what it must have been like to program in
> Forth or Lisp in the glory days of those languages. I'd be interested
> in seeing a demo sometime (maybe on video) of someone hacking on Forth
> code that does something complicated, using good interactive Forth
> tools.
We Forthers really try hard to not do something complicated ;-). When I
implemented bigForth' fast dictionary search, I explored several
options, hashing and AVL trees. AVL trees were more complicated, and
they lost to hashing in every metric: Time to write, execution
performance, memory usage, and bugs to fix during development.
In many cases you have an option which is simple, fast, and correct.
Don't try to use the other option.
> When I started using Python, I found myself thinking "this is
> what the old-time Maclisp hackers must have felt like". Haskell is
> different, completely different, a vision as powerful as Lisp but
> unlike
> anything that had been used for programming before. That in some
> sense outweighs any difficulties involved in trying to actually use
> it. ;-)
I'm still wondering how useful that would be for me. The main
challanges in the programs I write are the outside world, not the inner
logic of the program. E.g. take my net2o flow control, which took me
quite some time to develop. The code for it is rather simple, and it
always was rather simple, didn't crash or anything. That's not the
challange. The challange is to fill a network with packets just fast
enough, so they don't pile up in buffers, but yet leave no unused
bandwidth under real world conditions, which means things like Wifi with
rapidly changing quality, competing with multiple TCP/IP, BitTorrent or
net2o itself. This was a serious issue which I underestimated, given
how bold other people were about their results (like LEDBAT). I thought
I could just copy that, but it turned out to be not good enough.
A type system won't help at all here. The type system will catch the
low hanging fruits like f+ vs. + or similar. I don't have problems with
those, these are "declinations", and something the human brain can
handle quite well (the grammar engine).
--
Bernd Paysan
"If you want it done right, you have to do it yourself"
http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-26 19:33 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xtxvpkqrt.fsf@ruckus.brouhaha.com> |
| In reply to | #15182 |
Bernd Paysan <bernd.paysan@gmx.de> writes:
> No, I'm comparing a bloated Java+C++ project to a non-bloated Forth
> project. But even when I compare two non-bloated projects, GCC is
> hellish slow.
Oh ok, yeah, but I'd even say these days that GCC is bloated.
> Unfortunately, TCC is also lacking features. And using a different
> compiler for debug builds than for production builds is a bad idea - if
> you run into bugs of the production build compiler, what do you do then?
I'd think you have to test your production builds very thoroughly in any
case. TCC might be useful for rapid development and initial testing.
I think if I did anything serious with C these days, I'd also want to
test it with KCC, a very slow interpreter designed to make sure that if
your program attempts undefined behavior (which is ridiculously easy in
C), it will crash with an error message, rather than doing something
unpredictable and going on its way. Some info:
http://blog.regehr.org/archives/523
That guy's blog has lots of other good stuff too, that all makes me want
to stay far away from C.
>> This still takes a lot of runs of the program
> Well, it does not feel "a lot" if you can do these runs pretty quickly.
Yeah, that isn't always completely feasible though.
>> style where you pass around execution tokens a lot, and those xt's
>> may take other xt's as arguments ...
> After I added quotations to my system, I started doing that regularly.
I have to wonder how much debugging headache that created. Was it
a problem?
> A subscript overflow is not exactly a type error.
I think subscript overflow is considered a type error in the type system
literature, because if p is a pointer to type Foo, then p+i also has
type pointer to Foo, but if i is out of range then p+i may actually
point to something other than an Foo.
>> Red-black trees are binary trees...
> That's exactly what I don't like. This is a rather complicated thing,
> and I'm sure neither of us will write a perfect program first time.
But the idea is that with the right language features, we -can- get
these programs perfect the first time, if we mean the first time we try
to actually run the program. Of course it may take a lot of tries to
get the compiler to stop flagging errors, before we can run the program
that first time.
>> a sizable part of a C compiler has been written that way (CompCert).
> Calling this still a "type system" is a misnomer.
But it really is a type system! It's the Haskell type system on enough
steroids that it can no longer do automatic inference and needs a lot of
manual help, but it's a type system in the purest sense. It's fantastic
and wonderful from a mathematical standpoint even if it's useless in
practice. The theory behind it (constructive type theory) was developed
by a philosophical logician (Per Martin-Löf) in the 1970's, propagated
from there through mathematical logic and into CS theory, and has just
started appearing in actual programming languages in the last decade or
so, so it's still bleeding edge. I haven't used it yet (so I probably
still have some misconceptions) but I've been reading about it, and one
of my goals is to build up some skill with it pretty soon. Right now
only a few nerds care about it, but I think it's going to become
pervasive and important as the technology matures. There are some
online books:
1. http://www.cis.upenn.edu/~bcpierce/sf/
2. http://adam.chlipala.net/cpdt/
3. http://www.paultaylor.eu/stable/Proofs+Types.html
The first is pretty readable and I've been looking at it, the second
goes into perhaps more depth, and the third is pure theory and I don't
understand it, but I mention it for completeness.
> If the code system tells me just "your transformation is wrong", then
> I have no clue why, and can only guess.
I think in practice it's not that hard to figure out where the error is
when the compiler complains. There are some interactive tools (an IDE
and some Emacs modes) that let you navigate the types from the inside
outward or some such. I saw a demo of one of them and the guy could
operate it pretty fast, but I don't know how to use it myself for now.
> Yes. Usually several architectural issues stacked on each others, like
> using a complicated delegate-style OOP program
The functional programming crowd seems pretty opposed to OOP, e.g.:
http://existentialtype.wordpress.com/2011/03/15/teaching-fp-to-freshmen/
"Object-oriented programming is eliminated entirely from the introductory
curriculum, because it is both anti-modular and anti-parallel by its
very nature, and hence unsuitable for a modern CS curriculum."
That's from a CMU professor about their new intro programming course,
which uses ML. The guy is one of ML's designers and he doesn't like
Haskell either, so hmm... ;-)
>> test the successfully compiling parts of your program right away,
>> postponing dealing with the unsuccessful parts til later.
> Given that fact, I'm less opposed than before. How useful is GHCi (the
> interactive command line)?
It's pretty useful, especially the more recent versions that remove some
annoying restrictions of the older ones. It's still an interpreter
that's maybe 10x slower than running compiled code. There's an Emacs
mode that lets you write Haskell code in one window and run GHCi in
another window and quickly send Emacs buffers to GHCi, sort of like
gforth.el. I think one tends to develop in a less intensely interactive
manner than in Forth though, in part because more time is spent writing
out static descriptions in the form of types.
>> Haskell is different, completely different...
> I'm still wondering how useful that would be for me. The main
> challanges in the programs I write are the outside world...
Hmm, I'd say the issues you're dealing with area in an area that has
historically been rather hard to control with Haskell. Recently there
have been a bunch of attacks on the problem (called enumeratees,
conduits, etc.) that are improving the situation, but are still in a
state of rapid change and require building up a significant skill level
before they can be used at all. So as an immediate practical tool for
those purposes, Haskell might not be ready yet. You might look at
Erlang.
That said, I've put a lot of effort into studying Haskell and its
surrounding infrastructure (e.g. I've learned a fair amount of logic) in
the past few years, and I think it's been worth it from a mental clarity
point of view, even if I don't end up using it directly for practical
programming. It's the same sort of benefit that one gets from
practicing some assembly coding, except from the opposite direction:
assembler is too low-level for most everyday use, and Haskell may be too
high-level, but knowing either brings increased clarity to the practical
stuff in the middle. Similar things have long been said about Lisp.
> The challange is to fill a network with packets just fast enough, so
> they don't pile up in buffers, but yet leave no unused bandwidth under
> real world conditions, which means things like Wifi with rapidly
> changing quality, competing with multiple TCP/IP, BitTorrent or net2o
> itself.
But this sounds like a computational problem, tracking the capacity
and contents of all those channels, and periodically deciding what
to do next. Haskell may be fine for that.
> A type system won't help at all here. The type system will catch the
> low hanging fruits like f+ vs. + or similar.
Really, I think that underestimates how expressive and useful a serious
type system is. Here is a cool paper:
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.104.5859&rep=rep1&type=pdf
The author read a Google publication about its parallel MapReduce
framework, which gave an overview in which some details were unclear.
And by describing the understandable parts as Haskell types, he was able
to use the Haskell typechecker to figure out stuff that wasn't clear in
the Google paper.
Anecdote: the best programmer I know (the initial author of GCC and
Emacs--you know who I mean) likes to tell about when he first put
automatic parenthesis balancing into Emacs, so that when you type a
right-paren, the cursor momentarily bounces back to the matching
left-paren. He said that before he implemented that feature, he didn't
have too bad a time writing properly nested Lisp code manually, but
after using the new automatic balancing for a few days, he lost the
ability to do it by hand. And his conclusion was that this purely
mechanical skill had been tying up a significant amount of his
brainpower that he could now use for more productive purposes.
It's the same way IMHO with programming language features. The more
they do for you automatically, the more your own ability is freed up to
do stuff that can't be automated.
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2012-08-27 13:34 -0500 |
| Subject | Re: Function Points |
| Message-ID | <boCdnWK73KpVIKbNnZ2dnUVZ8kednZ2d@supernews.com> |
| In reply to | #15183 |
Paul Rubin <no.email@nospam.invalid> wrote:
> The functional programming crowd seems pretty opposed to OOP, e.g.:
> http://existentialtype.wordpress.com/2011/03/15/teaching-fp-to-freshmen/
> "Object-oriented programming is eliminated entirely from the
> introductory curriculum, because it is both anti-modular and
> anti-parallel by its very nature, and hence unsuitable for a
> modern CS curriculum."
>
> That's from a CMU professor about their new intro programming course,
> which uses ML. The guy is one of ML's designers and he doesn't like
> Haskell either, so hmm... ;-)
As far as I can tell from that article and the following discussion,
its justification is mostly in terms of formal methods: formal methods
haven't made much progress with OO, so OO must be bad. (Yes, I'm
oversimplifying.) And the claims that functional programming is more
parallel than OO are a bit much. How do threads in Concurrent Haskell
communicate? Through shared state, just as threads in imperative and
object-oriented languages do. I don't know of another way do do it.
Of course, you can functions like map and reduce on top of threads,
but you don't need functional languages for that.
One thing I agree with: Java isn't a great language for introductory
programming courses, not because it is object-oriented (that's good)
but because it requires some boilerplate. Compare
class HelloWorld {
static public void main( String args[] ) {
System.out.println( "Hello, World!" );
}
}
and Python
print "Hello, World!"
not to mention
.( Hello, World!)
No contest!
Andrew.
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-27 22:38 +0200 |
| Subject | Re: Function Points |
| Message-ID | <2058205.mNSn2Xapql@sunwukong.fritz.box> |
| In reply to | #15198 |
Andrew Haley wrote:
> One thing I agree with: Java isn't a great language for introductory
> programming courses, not because it is object-oriented (that's good)
> but because it requires some boilerplate. Compare
>
> class HelloWorld {
> static public void main( String args[] ) {
> System.out.println( "Hello, World!" );
> }
> }
>
> and Python
>
> print "Hello, World!"
>
> not to mention
>
> .( Hello, World!)
>
> No contest!
Java is a bit inconsistent there in that you don't need to import
java.lang.system to do that. I would have expected so, but apparently,
System is accessible even without a boiler plate.
--
Bernd Paysan
"If you want it done right, you have to do it yourself"
http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2012-08-28 02:45 -0500 |
| Subject | Re: Function Points |
| Message-ID | <-6-dnU_Gt7KJ6qHNnZ2dnUVZ8hCdnZ2d@supernews.com> |
| In reply to | #15203 |
Bernd Paysan <bernd.paysan@gmx.de> wrote:
> Andrew Haley wrote:
>> One thing I agree with: Java isn't a great language for introductory
>> programming courses, not because it is object-oriented (that's good)
>> but because it requires some boilerplate. Compare
>>
>> class HelloWorld {
>> static public void main( String args[] ) {
>> System.out.println( "Hello, World!" );
>> }
>> }
>>
>> and Python
>>
>> print "Hello, World!"
>>
>> not to mention
>>
>> .( Hello, World!)
>>
>> No contest!
>
> Java is a bit inconsistent there in that you don't need to import
> java.lang.system to do that. I would have expected so, but apparently,
> System is accessible even without a boiler plate.
You don't have to import java.lang.anything. That seems reasonable
enough.
Andrew.
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-27 18:14 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xd32bx1fj.fsf@ruckus.brouhaha.com> |
| In reply to | #15198 |
Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
>> The functional programming crowd seems pretty opposed to OOP, e.g.:
>> http://existentialtype.wordpress.com/2011/03/15/teaching-fp-to-freshmen/
> As far as I can tell from that article and the following discussion,
> its justification is mostly in terms of formal methods...
I hear similar things from other FP folks, and it may be partly
tribalism, but additional objections are 1) subtype polymorphism is
messy compared with Haskell's bounded polymorphism; 2) inheritance
making the program flow confusing; 3) the usual gripes about mutable
state, especially mutable state spread all over the place.
> And the claims that functional programming is more parallel than OO
> are a bit much. How do threads in Concurrent Haskell communicate?
> Through shared state,
Ah, but one does not need Concurrent Haskell to get parallel execution.
Haskellers distinguish between concurrency (multiple threads of
execution to deal with non-deterministic, asynchronous inputs from the
outside world) and parallelism (using multiple CPU cores simultaneously
to do a deterministic computation faster). Concurrent threads will
usually communicate through MVars (or STM), and yeah, these are mutable
cells, but typically there'd be a very small number of them per thread
for communications purposes, and the stuff happening within a thread
wouldn't involve mutation the way OO programs usually have objects
changing state everywhere.
Haskell parallelism doesn't require any visible mutation or threads at
all, e.g. the "par" combinator: x `par` y advises the compiler that it
can likely get some speedup by computing x and y in parallel, but the
result is exactly the same as if they were done sequentially. The
programmer doesn't have to deal with any interthread communication,
state, locks, etc. at all. See:
http://donsbot.wordpress.com/2007/11/29/use-those-extra-cores
for how it works. There are similarly things like parMap which is like
map but runs in parallel in CPU threads, and some stuff in progress that
can spin out parallel vector operations to a GPU, again with almost no
fuss to the programmer, no visible shared state, etc.
> and Python
> print "Hello, World!"
Unfortunately this breaks in Python 3 :-(
> not to mention
> .( Hello, World!)
Hmm,
: hw .( Hello, World!) ; Hello, World! ok
hw ok
;-)
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-27 18:24 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7x8vczx0zn.fsf@ruckus.brouhaha.com> |
| In reply to | #15211 |
Paul Rubin <no.email@nospam.invalid> writes: >> its justification is mostly in terms of formal methods... > I hear similar things from other FP folks Self-followup: 1) Clarification, by "similar" I just mean anti-OO sentiment in general, not related to formal methods. 2) Also meant to add: one of the arguments for fancy static type systems (stated explicitly in Pierce's book "Types and programming languages") is that the types amount to lightweight formal methods, that can be used without much fuss in everyday programming. They are no longer huge, tedious, special purpose machinery used only for ultra-critical high-budget applications like spacecraft. The red-black tree example I gave earlier (GADT's verify the red-black tree invariants) is illustrative of this.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2012-08-30 14:22 +0000 |
| Subject | Re: Function Points |
| Message-ID | <2012Aug30.162206@mips.complang.tuwien.ac.at> |
| In reply to | #15212 |
Paul Rubin <no.email@nospam.invalid> writes:
>2) Also meant to add: one of the arguments for fancy static type systems
>(stated explicitly in Pierce's book "Types and programming languages")
>is that the types amount to lightweight formal methods, that can be used
>without much fuss in everyday programming. They are no longer huge,
>tedious, special purpose machinery used only for ultra-critical
>high-budget applications like spacecraft. The red-black tree example I
>gave earlier (GADT's verify the red-black tree invariants) is
>illustrative of this.
Not at all. I have never implemented a balanced tree, and I guess
most other programmers have not, either, or only as an exercise. For
every potential use I have encountered there has been a less complex
and usually more efficient data structure (usually a hash table).
So, the example illustrates that Haskell's type system may help me
with a problem that I have never encountered. Not very convincing as
far as real-world usage is concerned. The example gets categorized as
"cool, but useless".
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2012: http://www.euroforth.org/ef12/
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2012-08-28 03:07 -0500 |
| Subject | Re: Function Points |
| Message-ID | <ZP2dnVxfr6yk4aHNnZ2dnUVZ8iWdnZ2d@supernews.com> |
| In reply to | #15211 |
Paul Rubin <no.email@nospam.invalid> wrote: > Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >>> The functional programming crowd seems pretty opposed to OOP, e.g.: >>> http://existentialtype.wordpress.com/2011/03/15/teaching-fp-to-freshmen/ >> As far as I can tell from that article and the following discussion, >> its justification is mostly in terms of formal methods... > > I hear similar things from other FP folks, and it may be partly > tribalism, but additional objections are 1) subtype polymorphism is > messy compared with Haskell's bounded polymorphism; 2) inheritance > making the program flow confusing; 3) the usual gripes about mutable > state, especially mutable state spread all over the place. > >> And the claims that functional programming is more parallel than OO >> are a bit much. How do threads in Concurrent Haskell communicate? >> Through shared state, > > Ah, but one does not need Concurrent Haskell to get parallel > execution. No, of course not: you can put the parallelism into a library if you have an embarassingly parallel problem. But that's true of many languages. > Haskell parallelism doesn't require any visible mutation or threads > at all, e.g. the "par" combinator: x `par` y advises the compiler > that it can likely get some speedup by computing x and y in > parallel, but the result is exactly the same as if they were done > sequentially. The programmer doesn't have to deal with any > interthread communication, state, locks, etc. at all. Well, yes. Just like fork/join in Cilk plus. I think that the parallel advantages of functional programming may have been oversold. Sure, there are theoretical advantages, but do they actually result in greater use of parallelism in practical applications? >> not to mention >> .( Hello, World!) > > Hmm, > > : hw .( Hello, World!) ; Hello, World! ok > hw ok > > ;-) Huh!? That's just a bug. Andrew.
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-28 08:18 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xk3wjujt3.fsf@ruckus.brouhaha.com> |
| In reply to | #15219 |
Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
> No, of course not: you can put the parallelism into a library if you
> have an embarassingly parallel problem. But that's true of many
> languages.
I think GHC's parallelization capabilities go beyond "embarassingly
parallel" (computations that are obviously independent). For example,
memoization in an imperative language usually works by updating some
kind of table to stored memoized values, and if you want to do this in
parallel you face the usual hassles of locks or maybe STM. In Haskell,
memoization is done with lazy evaluation and the GHC implemention of
this is already thread-safe, so you can memoize in a parallel program
without adding headaches.
> Well, yes. Just like fork/join in Cilk plus.
It looks like you have to be very careful in Cilk to make sure that the
parallel computations don't interfere with each other. Functional
purity in Haskell makes it easy to statically guarantee this. It
wouldn't surprise me if Cilk applications end up using functional-style
data structures instead of traditional imperative ones in places,
because of this non-interference.
> I think that the parallel advantages of functional programming may
> have been oversold. Sure, there are theoretical advantages, but do
> they actually result in greater use of parallelism in practical
> applications?
The notion from 20 years ago that FPL compilers were going to
parallelize stuff automatically (with no programmer advice or
annotations) seems to have failed, so I suppose it was oversold in that
sense. The overhead of dispatching calculations to multiple cores
outweighs the parallel speedup if the calculations are small, which the
compiler can't tell. Adding a few annotations at good parallization
opportunities gets around this problem, and is safe and easy compared to
imperative approaches. So it seems to me that there is more low-hanging
fruit available. I think it's not in widespread use yet mostly because
it is still pretty new.
>> : hw .( Hello, World!) ; Hello, World! ok
>> hw ok
>> ;-)
>
> Huh!? That's just a bug.
It looks like .( does what it's supposed to. It just surprised me and
it wasn't the equivalent of Python's print statement. I expected
something more like
." Hello, World!"
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2012-08-28 12:15 -0500 |
| Subject | Re: Function Points |
| Message-ID | <KICdna57R5BSYaHNnZ2dnUVZ8jGdnZ2d@supernews.com> |
| In reply to | #15220 |
Paul Rubin <no.email@nospam.invalid> wrote: > Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >> No, of course not: you can put the parallelism into a library if you >> have an embarassingly parallel problem. But that's true of many >> languages. > > I think GHC's parallelization capabilities go beyond "embarassingly > parallel" (computations that are obviously independent). For > example, memoization in an imperative language usually works by > updating some kind of table to stored memoized values, and if you > want to do this in parallel you face the usual hassles of locks or > maybe STM. In Haskell, memoization is done with lazy evaluation and > the GHC implemention of this is already thread-safe, so you can > memoize in a parallel program without adding headaches. Well, yes, so you use STM for memoization. Where, exactly, is the problem? I must be missing something. >> Well, yes. Just like fork/join in Cilk plus. > > It looks like you have to be very careful in Cilk to make sure that > the parallel computations don't interfere with each other. I wouldn't have thought so: fork/join is for computations that can be partitioned in some way. Of course, the partitioning has to be correct. > Functional purity in Haskell makes it easy to statically guarantee > this. It wouldn't surprise me if Cilk applications end up using > functional-style data structures instead of traditional imperative > ones in places, because of this non-interference. To the extent that functional-style data structures make sense, yes, of course. I presume "functional-style" means write-once or some kind of copy on write, which is well established. >> I think that the parallel advantages of functional programming may >> have been oversold. Sure, there are theoretical advantages, but do >> they actually result in greater use of parallelism in practical >> applications? > > The notion from 20 years ago that FPL compilers were going to > parallelize stuff automatically (with no programmer advice or > annotations) seems to have failed, so I suppose it was oversold in > that sense. The overhead of dispatching calculations to multiple > cores outweighs the parallel speedup if the calculations are small, > which the compiler can't tell. Adding a few annotations at good > parallization opportunities gets around this problem, and is safe > and easy compared to imperative approaches. But no easier than fork/join apart from the claim that "you have to be very careful" of which I am not totally convinced. AFAIK functional languages have no advantages over imperative languages in the area of concurrency except the aforementioned checking. Of course proponents of bondage and discipline languages will argue that everything is much easier because we're protected from ourselves. > So it seems to me that there is more low-hanging fruit available. I > think it's not in widespread use yet mostly because it is still > pretty new. Perhaps. I've been massively impressed by the speed at which GCC is adopting fork/join and transactions, and I suspect that it will have alot more impact on real-world concurrency. >>> : hw .( Hello, World!) ; Hello, World! ok >>> hw ok >>> ;-) >> >> Huh!? That's just a bug. > > It looks like .( does what it's supposed to. Well, yes: the bug is in your program. > It just surprised me and it wasn't the equivalent of Python's print > statement. Not exactly, no. These are just "Hello, World" programs in various languages. All they have to do is print "Hello, World". Andrew.
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-28 23:05 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7x4nnmw7vj.fsf@ruckus.brouhaha.com> |
| In reply to | #15222 |
Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >>In Haskell, memoization is done with lazy evaluatio > Well, yes, so you use STM for memoization. Where, exactly, is the > problem? I must be missing something. Hmm, maybe you're right; I'm not sure. There is a potentially bad performance bottleneck with STM if there's a big memoization table that you're updating a lot of parts of simultaneously from different threads. GHC's approach relies on the immutability of values in Haskell, so two threads might update the same cell with no locks, but it's with the same value so it's ok. I guess you could also write imperative code that way though, so I'll have to ask the #haskell folks if there's more to it than that. I know there has to be some special hair in GHC's garbage collector for it, but maybe it's less of a big deal than I thought. > I wouldn't have thought so: [Cilk] fork/join is for computations that > can be partitioned in some way. Of course, the partitioning has to be > correct. By comparison, Haskell's "par" annotations can be inserted anywhere in a program with no effect on the computed result. If you choose un-judiciously where to put them, you might get a slowdown instead of a speedup, but you won't introduce weird bugs. There is a cool tool "ThreadScope" that shows how much parallelism actually results, so you can tune it. I think Cilk might have something similar, though. > To the extent that functional-style data structures make sense, yes, > of course. I presume "functional-style" means write-once or some kind > of copy on write, which is well established. Yes, a classic example is using AVL or red-black trees instead of hash tables for associative maps. The idea is you can "copy" an AVL tree while adding or deleting a value in O(log n) operations, with the new tree sharing most of the old tree's structure. There's a good book "Purely Functional Data Structures" by Chris Okasaki with more examples. > AFAIK functional languages have no advantages over imperative > languages in the area of concurrency except the aforementioned > checking. Of course functional languages are implemented with imperative machinery under the hood, so with enough effort you can always write imperative code that does the same stuff as functional code. FPL's just make writing parallel code safer and more convenient, which actually does matter quite a lot of the time. Did you ever look at Tim Sweeney's slides about future programming languages? I think I've posted the url before: http://www.st.cs.uni-sb.de/edu/seminare/2005/advanced-fp/docs/sweeny.pdf It was one of the things that got me interested in Haskell. > Of course proponents of bondage and discipline languages will argue > that everything is much easier because we're protected from ourselves. Rather than "B&D" I prefer to think of it as "let the compiler figure this out so I don't have to". It's just like if I have an unbalanced parenthesis in a C program, I'm better off having it flagged at compile time than causing a runtime crash. > Perhaps. I've been massively impressed by the speed at which GCC is > adopting fork/join and transactions, and I suspect that it will have > alot more impact on real-world concurrency. Maybe so. It takes a lot more work (or at least a lot more SLOC) to do something in C than in Haskell, but it could be that the applications where parallelism has the most impact (like supercomputing, or MapReduce running across whole data centers) are also the ones that justify the higher development budgets that it takes to use C. My hope from Haskell (maybe not realistic) is to get programmer productivity comparable to Python with performance comparable to Java and reliability superior to both. Low-hassle, safe parallelism from simple constructs is a big win in that context. In the most performance critical applications, C and C++ will probably continue to dominate. I do think it's awesome that Cilk is now part of GCC, which I only just found out. >> It looks like .( does what it's supposed to. > Well, yes: the bug is in your program. Yeah, I hadn't seen .( before, so I tried it and got a surprise. No big deal.
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2012-08-29 03:55 -0500 |
| Subject | Re: Function Points |
| Message-ID | <ypednXF7cq14RaDNnZ2dnUVZ7vednZ2d@supernews.com> |
| In reply to | #15234 |
Paul Rubin <no.email@nospam.invalid> wrote: > Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >>>In Haskell, memoization is done with lazy evaluatio >> Well, yes, so you use STM for memoization. Where, exactly, is the >> problem? I must be missing something. > > Hmm, maybe you're right; I'm not sure. There is a potentially bad > performance bottleneck with STM if there's a big memoization table > that you're updating a lot of parts of simultaneously from different > threads. I don't think so. STM can be as fine-grained as you like, and if it's sufficiently fine-grained you're not going to get any peformance bottleneck. If multiple threads are trying to update the same value, the transaction manager will back some of them off and allow others to proceed. It is true that STM has substantial overhead on current computer architectures, but IMO that problem is temporary: new hardware has the support we need. > GHC's approach relies on the immutability of values in Haskell, so > two threads might update the same cell with no locks, but it's with > the same value so it's ok. I guess you could also write imperative > code that way though, so I'll have to ask the #haskell folks if > there's more to it than that. If it's just a matter of updating one pointer or maybe a pair of them, then yes you can do it. But of course everything that Haskell does is imperative under the table, you just have to dig deep enough. :-) >> AFAIK functional languages have no advantages over imperative >> languages in the area of concurrency except the aforementioned >> checking. > > Of course functional languages are implemented with imperative machinery > under the hood, so with enough effort you can always write imperative > code that does the same stuff as functional code. FPL's just make > writing parallel code safer and more convenient, which actually does > matter quite a lot of the time. Well, that's the claim. AFAICS it's the same claim that the functional people make for everything else. I guess I should learn Haskell, but I only have one life. > Did you ever look at Tim Sweeney's slides about future programming > languages? I think I've posted the url before: > > http://www.st.cs.uni-sb.de/edu/seminare/2005/advanced-fp/docs/sweeny.pdf Yes, I've seen it before, thanks. There's a lot to like about it. I understand why referential transaparency helps, but as soon as you've got interprocess communication referential transaparency goes out of the window. I *am* convinced that transactions are a huge breakthrough: that's beyond doubt IMO. One thing we can say for certain is that a particular style is very helpful with concurrent programming. This style involves immutable objects and secure mechanisms such as transactions where state must be shared. [Aside: as far as I can tell, transactional memory solves completely the famous "Inheritance Anomaly" whereby inheritance makes it difficult to subclass without breaking synchronization. Despite the fact that hundreds of papers and some theses have been written about this problem, few people seem to have noticed. Perhaps I'm missing something.] Andrew. Satoshi Matsuoka, Akinori Yonezawa: Analysis of Inheritance Anomaly in Object-Oriented Concurrent Programming Languages, in G. Agha, A. Yonezawa, P. Wegner, eds., Research Directions in Concurrent Object-Oriented Programming, MIT Press, 1993.
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-27 22:28 +0200 |
| Subject | Re: Function Points |
| Message-ID | <1541485.dRTfZbgPJF@sunwukong.fritz.box> |
| In reply to | #15183 |
Paul Rubin wrote: > Oh ok, yeah, but I'd even say these days that GCC is bloated. I mean it is hellish slow to compile a non-bloated project. GCC+bloated project=lunch. Actually, I compiled Android from source over night, because I don't have the same sort of computing power as Google ;-). This feels like programming was 40 years ago on mainframes - at the time where Forth was invented. >>> style where you pass around execution tokens a lot, and those xt's >>> may take other xt's as arguments ... >> After I added quotations to my system, I started doing that >> regularly. > > I have to wonder how much debugging headache that created. Was it > a problem? No. The quotations are short, and you can only test them in context, so you just run the thing in context, it's no problem that the quotation has no name and can't be called directly on the command line. It does not make that much sense as stand-alone program. A quotation should be short, and use tested factors (which then have names). You debug quotations with ~~ statements inserted at interesting places if necessary (most quotations are right first time, because they should deliberately be simple). >> A subscript overflow is not exactly a type error. > > I think subscript overflow is considered a type error in the type > system literature, because if p is a pointer to type Foo, then p+i > also has type pointer to Foo, but if i is out of range then p+i may > actually point to something other than an Foo. I'd rather say an array with index [0..n] has a subtype of int as index, but that is an algebraic constraint. You had this example with the type system that allowed a lot of algebraic constraints, but I would not call that a type system anymore. It's more a formal verification system, following the same sort of algebra you use for type systems. The self- advertizing of Coq also says it's a formal proof management system. >>> Red-black trees are binary trees... >> That's exactly what I don't like. This is a rather complicated >> thing, and I'm sure neither of us will write a perfect program first >> time. > > But the idea is that with the right language features, we -can- get > these programs perfect the first time, if we mean the first time we > try to actually run the program. Indeed. But it's the attitude of "running the code is to be done as late as possible". You should not do that, at least not in Forth. You should start writing a program, and when you get to the point where you actually can try something (which is early), you should let it run. It is rewarding to get something done, even if it is little, and a process that is rewarding the programmier is improving productivity and makes it more fun to write programs. Humans are motivated by positive feedback, so fun is important. It's frustrating to only see error messages from the compiler. When I'd be writing an r/b tree program, the first step would be to insert nodes and print the tree. Hey, great, I can insert nodes and print a tree. It's not balanced, but I can now add tree rotation operations. And print the rotated tree. It's a hands-on experience. The program does something in all stages of development, though it is not perfect at the first run. > Of course it may take a lot of tries to > get the compiler to stop flagging errors, before we can run the > program that first time. Yes, but that's not "right first time". A program is "right first time" if - after internal debugging - it gets out error-free to the customer. What happens in between the first keystroke and the release to customer is entirely yours. This sort of "getting the program to finally compile" is frustrating for me, and what I observed from other people is that after it finally compiles, they are happy when it sort-of-runs, and are not interested in more debugging. > Right now > only a few nerds care about it, but I think it's going to become > pervasive and important as the technology matures. There are some > online books: > > 1. http://www.cis.upenn.edu/~bcpierce/sf/ > 2. http://adam.chlipala.net/cpdt/ > 3. http://www.paultaylor.eu/stable/Proofs+Types.html > > The first is pretty readable and I've been looking at it, the second > goes into perhaps more depth, and the third is pure theory and I don't > understand it, but I mention it for completeness. Thanks for the links. >> Yes. Usually several architectural issues stacked on each others, >> like using a complicated delegate-style OOP program > > The functional programming crowd seems pretty opposed to OOP, e.g.: > http://existentialtype.wordpress.com/2011/03/15/teaching-fp-to- freshmen/ > "Object-oriented programming is eliminated entirely from the > introductory curriculum, because it is both anti-modular and > anti-parallel by its very nature, and hence unsuitable for a > modern CS curriculum." > > That's from a CMU professor about their new intro programming course, > which uses ML. The guy is one of ML's designers and he doesn't like > Haskell either, so hmm... ;-) Maybe a bit biased ;-). >> Given that fact, I'm less opposed than before. How useful is GHCi >> (the interactive command line)? > > It's pretty useful, especially the more recent versions that remove > some > annoying restrictions of the older ones. It's still an interpreter > that's maybe 10x slower than running compiled code. There's an Emacs > mode that lets you write Haskell code in one window and run GHCi in > another window and quickly send Emacs buffers to GHCi, sort of like > gforth.el. Nice. The fact that it still doesn't have an incremental compiler is a bit lame ;-). >> The challange is to fill a network with packets just fast enough, so >> they don't pile up in buffers, but yet leave no unused bandwidth >> under real world conditions, which means things like Wifi with >> rapidly changing quality, competing with multiple TCP/IP, BitTorrent >> or net2o itself. > > But this sounds like a computational problem, tracking the capacity > and contents of all those channels, and periodically deciding what > to do next. Haskell may be fine for that. The problem is: The buffers won't tell you. At least not as long as they are IP routers, not net2o switches - and even those won't tell you the whole story, because telling means network traffic. The network should be used for the actual data, management (including flow control) should be minimized in bandwidth. The resulting program I have is fairly trivial, and it should be possible to implement it in whatever programming language you like, given you have a precise real-time clock and access to a socket interface. > Anecdote: the best programmer I know (the initial author of GCC and > Emacs--you know who I mean) likes to tell about when he first put > automatic parenthesis balancing into Emacs, so that when you type a > right-paren, the cursor momentarily bounces back to the matching > left-paren. He said that before he implemented that feature, he > didn't have too bad a time writing properly nested Lisp code manually, > but after using the new automatic balancing for a few days, he lost > the > ability to do it by hand. And his conclusion was that this purely > mechanical skill had been tying up a significant amount of his > brainpower that he could now use for more productive purposes. Hehe. Yes, that's a defect of Lisp, which makes it hard to use. Some derivatives used ] to close all brackets, which is somewhat helpful. > It's the same way IMHO with programming language features. The more > they do for you automatically, the more your own ability is freed up > to do stuff that can't be automated. As Forther, I like to automate things, but especially those things that helps me to reduce typing. That's why we extend the compiler. On the other hand, Forth does not automate the stack, which is something pretty basic, and almost every other language automates the stack. We don't, and we have a reason for not doing so. It clearly does consume brainpower by not doing so, but it encourages factoring, which is worth the price. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-27 20:26 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xk3wjn1cu.fsf@ruckus.brouhaha.com> |
| In reply to | #15202 |
Bernd Paysan <bernd.paysan@gmx.de> writes:
> I mean it is hellish slow to compile a non-bloated project. GCC+bloated
> project=lunch.
Maybe C++ is partly to blame, because of header bloat, template bloat,
etc. Here is an interesting rant about how fast Turbo Pascal was,
attributing the speed (compared with C++) in part to language
differences:
http://prog21.dadgum.com/47.html
Ocaml's compiler is supposed to also be fast, though I haven't used it.
> You had this example with the type system that allowed a lot of
> algebraic constraints, but I would not call that a type system
> anymore. It's more a formal verification system, following the same
> sort of algebra you use for type systems. The self- advertizing of
> Coq also says it's a formal proof management system.
Well, people can call things whatever they want, but it's quite standard
terminology in the PLT community that these things are type systems; and
there is an amazing correspondence (the Curry-Howard correspondence)
between type systems and proof systems: types represent propositions and
programs represent proofs.
As an extreme example (this is handwaving, but I think has at least some
resemblance to reality): say you've got a type X representing planar
maps (as in "map of Europe"), and a type Y representing those maps with
an assignment of one of 4 colors to each country, such that countries
sharing borders have different colors. The famous 4-color map theorem
says (in one way to phrase it) that there exists a function F, whose
input type is X and whose output type is Y, i.e. given any map this
function will produce a 4-coloring for the map.
What this means is if you can actually code a function with such a type
signature and get it through the Coq type checker, then Coq has verified
that you have exhibited the asked-for function F, i.e. you have proved
the 4-color theorem, just by getting F to type-check, without having to
actually run it. The actual Coq proof of the 4-color theorem[1] is very
complicated, but I think it basically amounts to writing a function with
a certain signature and getting it to type-check.
> Humans are motivated by positive feedback, so fun is important. It's
> frustrating to only see error messages from the compiler.
But the error messages are feedback too (hey, a new motto, "GHC, the
compiler where fixing type errors is fun!!"). Anyway, of course one
does develop incrementally in practice. Get one thing to work (and
typecheck), get the next thing to work, etc.
> Yes, but that's not "right first time". A program is "right first time"
> if - after internal debugging - it gets out error-free to the customer.
There's another aspect: how do you convince the customer (or anyone
else) of the absence of errors? Of course you can fail to find test
cases that give wrong results, but that doesn't substitute for a
deductive process saying that no failure cases exist. Say there's a
spot in the code that will obviously crash if x=0, but that's ok, you've
got some sound but non-trivial reasoning showing that x>0 whenever that
spot is reached. Maybe you have to explain this reasoning in code
review, and perhaps you write a longish comment explaining it. Someone
else perhaps carefully reads the comment, checking all the claims in the
comment against the code to make sure they are valid.
Now the customer asks for a new feature, that you implement with a code
change. What happened to the validity of that comment? It has to be
checked again, burning somebody's time (maybe yours) every time the code
changes, and that ignores the possibility of making a mistake the 37th
time you check the comment.
That's what I think is one of the interesting visions is of Haskell (not
currently achieved in practice, but something to aim for). In
traditional programming, you reason in your head to figure out the
computation process, implement the process as code, but the reasoning is
at best written down as a comment. This is the "semantic gap" between
"what the programmer knows and what the language allows to be
stated".[2] In an idealized typed FP, the reasoning is written down as
part of the code, so the compiler can check it every time you recompile.
I believe from other people's reports and from (limited) personal
experience that Haskell is superior to Python in the following common
situation:
1) write and debug compplicated program. Deliver to customer.
2) Project is finished, so go work on other things.
3) 1 year later, customer asks for a new feature, and you have by now
forgotten most of how the program works. You have to patch it
without introducing bugs.
I can't compare it with Forth (not enough experience) but I have to
wonder if the situation is comparable. Automatic tests help, but they
aren't a silver bullet.
> I observed from other people is that after it finally compiles, they
> are happy when it sort-of-runs, and are not interested in more debugging.
That's a situation one might see with beginning programmers using Java
or something like that, but it's much different with experienced
programmers and Haskell-like languages.
> Nice. The fact that it still doesn't have an incremental compiler is a
> bit lame ;-).
Usually your program is in reasonable-sized, separately compiled
modules, so when hacking with ghci you're only recompiling the module
that you're actively working on. At least on a modern pc, this is fast
enough in practice.
> The problem is: The buffers won't tell you. At least not as long as
> they are IP routers, not net2o switches - and even those won't tell you
> the whole story, because telling means network traffic.
I guess I still don't understand this: you mean you want to model the
travel of packets in flight, so you can dynamically adjust things to
prevent congestion even in places outside your network that you can't
observe directly? That sounds cool but difficult.
Well, there is a joke FAQ built into the Haskell IRC bot, where no
matter what you ask, the bot replies "The answer is: yes! Haskell can
do that." This sounds like one of those types of problems. ;-).
[1] http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf
[2] https://personal.cis.strath.ac.uk/patricia.johann/popl08.pdf
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-28 23:17 +0200 |
| Subject | Re: Function Points |
| Message-ID | <33657766.8ZRYGjOceB@sunwukong.fritz.box> |
| In reply to | #15214 |
Paul Rubin wrote: > Well, people can call things whatever they want, but it's quite > standard terminology in the PLT community that these things are type > systems; and there is an amazing correspondence (the Curry-Howard > correspondence) between type systems and proof systems: types > represent propositions and programs represent proofs. I don't think of types as such. A data type is a particular representation of your data. You can have bytes, words, floats, addresses, and combinations/tuples of those like strings (which starts at an address, has a length, and a bunch of bytes/characters froming the string). > The actual Coq proof of the 4-color theorem[1] is > very complicated, but I think it basically amounts to writing a > function with a certain signature and getting it to type-check. Coq's proof system is similar to other formal proof systems (the ones formalized in the late 20th of the previous century). >> Humans are motivated by positive feedback, so fun is important. It's >> frustrating to only see error messages from the compiler. > > But the error messages are feedback too (hey, a new motto, "GHC, the > compiler where fixing type errors is fun!!"). Anyway, of course one > does develop incrementally in practice. Get one thing to work (and > typecheck), get the next thing to work, etc. No, an error message is a negative feedback, it tells you "you did something wrong". >> Yes, but that's not "right first time". A program is "right first >> time" if - after internal debugging - it gets out error-free to the >> customer. > > There's another aspect: how do you convince the customer (or anyone > else) of the absence of errors? Of course you can fail to find test > cases that give wrong results, but that doesn't substitute for a > deductive process saying that no failure cases exist. I once had a customer who told me that he didn't believe the Shannon Theorem. Well, I said, you can prove that it is correct. But that didn't bother him much. Note also that Knuth once wrote "Beware: I have proved this program currect, but didn't test it". The deducing process is alway an equivalence check: The program and the specified conditions are (after transformation) equivalent. The specification of the conditions is just as bug-prone as the program itself (or even more), so proving equivalence does not prove absense of bugs. Almost 20 years ago, I had attended to a CS course which had as topic "complex systems", and was really about using theoreme provers to aid program development. Not as nice as Coq, but similar in spirit. The language to specify conditions was more cumbersome to use and more error-prone as to actually write the program and test it. > Say there's a > spot in the code that will obviously crash if x=0, but that's ok, > you've got some sound but non-trivial reasoning showing that x>0 > whenever that > spot is reached. Maybe you have to explain this reasoning in code > review, and perhaps you write a longish comment explaining it. > Someone else perhaps carefully reads the comment, checking all the > claims in the comment against the code to make sure they are valid. You shouldn't have non-trivial reasonings for that. Trivial reasonings are ok, e.g. x is a pointer, and you don't pass null pointers around, only allocated objects. > Now the customer asks for a new feature, that you implement with a > code > change. What happened to the validity of that comment? It has to be > checked again, burning somebody's time (maybe yours) every time the > code changes, and that ignores the possibility of making a mistake the > 37th time you check the comment. > > That's what I think is one of the interesting visions is of Haskell > (not > currently achieved in practice, but something to aim for). In > traditional programming, you reason in your head to figure out the > computation process, implement the process as code, but the reasoning > is > at best written down as a comment. This is the "semantic gap" between > "what the programmer knows and what the language allows to be > stated".[2] In an idealized typed FP, the reasoning is written down as > part of the code, so the compiler can check it every time you > recompile. This is where I think it becomes silly. If you can write your reasoning down in a formalized language, you should be able to get a working program from that (e.g. using the methods Prolog uses). I also don't think there is a semantic gap between programmer knowledge and program, there usually is a semantic gap between what the programmer thinks is sufficient to describe the problem, and what is actually needed to implement it. The difference between idea and realization. > I believe from other people's reports and from (limited) personal > experience that Haskell is superior to Python in the following common > situation: > > 1) write and debug compplicated program. Deliver to customer. > 2) Project is finished, so go work on other things. > 3) 1 year later, customer asks for a new feature, and you have by > now > forgotten most of how the program works. You have to patch it > without introducing bugs. If you have forgotten how most of your program works, adding a new feature is futile. Well, at least in Forth, because there, you have created a sort-of domain specific language, in which you will have to write your new feature, as well. If you forgot how that works, you won't be able to. On the other hand, well organized programs don't fall apart when you change things. The last really old project I've resurrected was an eleven year old battery monitor simulator, and the request was to change the waveform viewer to one I had done a year before, because the newer one looked nicer (it was for a demo at Apple, and they have designers, not engineers ;-). So I ripped the old waveform viewer out, put the new one in, and with a small amount of testing, the program worked. The key of success for this is to create components which are loosely coupled, and not a tightly coupled mess which you can't untangle a year later. I don't think it's a matter of programming language, you can write bad programs in every language. Though, some programs make it easier for bad programmers to be learned, and I'd say, Haskell is really driving bad programmers to Python and PHP. > I can't compare it with Forth (not enough experience) but I have to > wonder if the situation is comparable. Automatic tests help, but they > aren't a silver bullet. But automated proofs are no silver bullet, either. Essentially, there is no silver bullet. > That's a situation one might see with beginning programmers using Java > or something like that, but it's much different with experienced > programmers and Haskell-like languages. But then, you have a self-selected group of better programmers. Brooks found that in his small test group, bad vs. good was by a factor of 20 apart. Having a self-selected group of good programmers is just awesome. It's way more important than the programming language (though, of course, good programmers select their own tools). >> Nice. The fact that it still doesn't have an incremental compiler is >> a bit lame ;-). > > Usually your program is in reasonable-sized, separately compiled > modules, so when hacking with ghci you're only recompiling the module > that you're actively working on. At least on a modern pc, this is > fast enough in practice. In Forth, you don't have to think about which part of the program you are working at, it's fast enough to recompile the whole program, even if the program is pretty large. >> The problem is: The buffers won't tell you. At least not as long as >> they are IP routers, not net2o switches - and even those won't tell >> you the whole story, because telling means network traffic. > > I guess I still don't understand this: you mean you want to model the > travel of packets in flight, so you can dynamically adjust things to > prevent congestion even in places outside your network that you can't > observe directly? That sounds cool but difficult. Yes, but that's the requirement for an Internet protocol. The key to success of course is to take the observable part of the data, and use that. The observable part is the time when each packet arrives at the destination, and that timing information is then used to do some relatively simple calculations about what actuall packet rate is achievable. > Well, there is a joke FAQ built into the Haskell IRC bot, where no > matter what you ask, the bot replies "The answer is: yes! Haskell can > do that." This sounds like one of those types of problems. ;-). Well, it's not about being able to do that, the code to do this congestion control is actually rather trivial. What I said is that having some typechecking in this quite trivial code isn't helpful. The tough part is finding some quite trivial code which does avoid congestions, and to do that, you need to look at what your program actually does. This is trivial stuff, either: you just print out the observed values, pass them to gnuplot, and view the plot. Haskell would probably give me some headaches with the low-level code, where I just need to get nanoseconds from the OS timer, and pack bytes together into a packet to be send at the given time through a network socket, but it should have no problem to compute the sending rate. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-29 01:13 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xzk5euncv.fsf@ruckus.brouhaha.com> |
| In reply to | #15226 |
Bernd Paysan <bernd.paysan@gmx.de> writes:
> I don't think of types as such. A data type is a particular
> representation of your data.
The way I used the term is consistent with the academic literature on
the subject, though I can accept that academic literature isn't
necessarily the whole story.
> You can have bytes, words, floats, addresses, and combinations/tuples
> of those like strings (which starts at an address, has a length, and a
> bunch of bytes/characters froming the string).
If you add discriminated unions (sum types) and parametrized types (like
List<T> in C++), you get approximately the ML type system. Haskell adds
additional hair but is along the same lines. Coq adds types
parametrized by runtime values, so Day<month> could mean "integer in the
range 1..31" if the month is January, but "integer in the range 1..28"
for month=February. That means you have to supply static manual proofs
about what the runtime values can be, in order for Coq type-check at
compile time. It turns out that with this system, Coq types can express
basically any property that can be written down in math.
> Coq's proof system is similar to other formal proof systems (the ones
> formalized in the late 20th of the previous century).
You mean 1995-2000? Yeah I suppose so (Agda, Epigram, Cayenne, etc.)
They're different from older systems in that they are proof assistants
and programming languages at the same time.
>> But the error messages are feedback too (hey, a new motto, "GHC, the
>> compiler where fixing type errors is fun!!").
> No, an error message is a negative feedback, it tells you "you did
> something wrong".
I mean really, some people are really into it. There's a Haskell blog
whose title is "The power of types compels you":
The types. At first, they helped me to write programs, then it turned
into an obsession. Compulsive need to turn every possible programming
error into statically checked type error, consumed my soul. Soon, it
was impossible for me to code anymore - inability to express the
proper solution in types and constant strive for perfection rendered
me unable to accept inferior solutions.
Would I stop myself, three years ago, from writing the first fold? Of
course not, I choose to believe what I was programmed to believe.
OK, enough of that, it probably wasn't funny anyway.
(http://paczesiowa.blogspot.com/2010_01_01_archive.html)
I think the further levels of Haskell type hackery are like the hairy
end of C++ template metaprogramming, i.e. not really sane, but people
like to see if it can be done. It seems to make more sense to use a
fundamentally more powerful system like Coq, at the cost of having to do
more of the derivations manually. But, right now this stuff is still
beyond my depth.
> The specification of the conditions is just as bug-prone as the
> program itself (or even more), so proving equivalence does not prove
> absense of bugs.
I think that's more true in the hardware control or human interaction
world, than in the purely computational world. It's far easier to
state Fermat's Last Theorem (the specification) than it is to prove it
(the program).
>> you've got some sound but non-trivial reasoning showing that x>0
> You shouldn't have non-trivial reasonings for that. Trivial reasonings
> are ok, e.g. x is a pointer, and you don't pass null pointers around,
> only allocated objects.
Every nontrivial algorithm uses nontrivial reasoning, or else the
algorithm would itself be trivial. Do you mean we should only use
trivial algorithms?
>
> This is where I think it becomes silly. If you can write your reasoning
> down in a formalized language, you should be able to get a working
> program from that (e.g. using the methods Prolog uses).
That's a far, far harder problem, that nobody has much clue about right
now. It amounts to automated theorem proving. Prolog simply uses
exponential search with some unreliable heuristics, so on non-trivial
problems it just won't finish in a practical amount of time. By
comparison, machine-checking the correctness of a human-created proof is
much better understood by now.
> I also don't think there is a semantic gap between programmer
> knowledge and program,
If the programmer can explain or document worthwhile facts about
the program that aren't formally part of the code, then that knowledge
is part of the semantic gap.
> If you have forgotten how most of your program works, adding a new
> feature is futile.
Of course programmers are required all the time to add new features to
unfamiliar legacy code. If you wrote the code yourself and forgot
most of the details, you're still a few steps ahead of someone who has
never seen the code before.
> The key of success for this is to create components which are loosely
> coupled, and not a tightly coupled mess which you can't untangle a year
> later. I don't think it's a matter of programming language, you can
> write bad programs in every language.
Generally it takes an iterative process to write the code and
concurrently clarify one's thoughts. It's great to be able to make some
additional iterative cleanup passes after the code is working, but
schedule and budget pressure don't always permit this. One has
to be a bit tactical in deciding when and what to refactor.
> Though, some programs make it easier for bad programmers to be
> learned, and I'd say, Haskell is really driving bad programmers to
> Python and PHP.
I'm not sure what you mean by this. PHP certainly has a lot of crap
code written by low-skill programmers, while getting past Haskell's
early learning curve takes quite a lot of effort. Haskell programmers
tend to be extremely skillful, which is one of the things that attracts
me to the Haskell community. (Forth is the same way, which is part of
why I still hang around here). I don't know of anyone switching from
Haskell to Python or PHP; it's always the other direction.
>> Automatic tests help, but they aren't a silver bullet.
> But automated proofs are no silver bullet, either. Essentially, there
> is no silver bullet.
This guy claims there is something like Moore's law for programmer
productivity: http://people.cs.umass.edu/~yannis/law.html
Why would this be? Languages would seem to have something to do with
it.
Types are no silver bullet, but they're a useful tool that IME do some
of the same work that test automation does. In that situation I
described (I recently had to add some new features to an old Python
program) I was able to add the new code quickly, but made some errors
that added some debugging time. It wasn't a huge amount, but it was
enough to be a nuisance, and types would have caught the problem
instantly.
>> That's a situation one might see with beginning programmers using Java
> But then, you have a self-selected group of better programmers.
No really, I just can't imagine someone writing a nerd blog about the
Java type system like the Haskell one I gave above (and there are quite
a few more like it). Haskellers aren't just self-selected good
programmers, they're self-selected for being into types! So yes, they
enjoy fixing type errors and writing their code so that impermissible
operations will result in type errors. There's an old article on
the subject:
http://www.lucacardelli.name/Papers/TypefulProg.pdf
it includes dynamic types as being typeful, as opposed to something like
Forth which is untyped.
> [Forth is] fast enough to recompile the whole program, even if the
> program is pretty large.
Yeah, GHC isn't anywhere near that fast. Separate compilation works
well enough though.
> Haskell would probably give me some headaches with the low-level code,
> where I just need to get nanoseconds from the OS timer, and pack bytes
> together into a packet to be send at the given time through a network
> socket, but it should have no problem to compute the sending rate.
Just reading the system timer and writing bytes at a given time is no
problem. If you need consistent sub-millisecond accuracy, random GC
delays might get in the way of that, but you could queue the packets
through a separate real-time process.
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-29 02:23 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7x7gsi2gsb.fsf@ruckus.brouhaha.com> |
| In reply to | #15236 |
Paul Rubin <no.email@nospam.invalid> writes: > If you add discriminated unions (sum types) and parametrized types (like > List<T> in C++), you get approximately the ML type system. Oops, silly me, I forgot to add function types. If X and Y are types, then X -> Y is a type, denoting functions from X to Y. Of course C also has types like that.
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-30 02:59 +0200 |
| Subject | Re: Function Points |
| Message-ID | <79196555.sLtJZzQ0cY@sunwukong.fritz.box> |
| In reply to | #15240 |
Paul Rubin wrote: > Paul Rubin <no.email@nospam.invalid> writes: >> If you add discriminated unions (sum types) and parametrized types >> (like List<T> in C++), you get approximately the ML type system. > > Oops, silly me, I forgot to add function types. If X and Y are types, > then X -> Y is a type, denoting functions from X to Y. Of course C > also has types like that. Or Forth. When we say, that Forth is untyped, we mean Forth is not typechecked. It's not actually untyped. We write the function type as "essential" comment into the functions we write, and name it "stack effect". -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-29 22:18 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xmx1ddkjh.fsf@ruckus.brouhaha.com> |
| In reply to | #15256 |
Bernd Paysan <bernd.paysan@gmx.de> writes: >>If X and Y are types, then X -> Y is a type, denoting functions from X >>to Y. Of course C also has types like that. > > Or Forth. When we say, that Forth is untyped, we mean Forth is not > typechecked. It's not actually untyped. We write the function type as > "essential" comment into the functions we write, and name it "stack > effect". It's untyped in the sense that the compiler doesn't know about the types: they are solely in the mind of the programmer and in the comment, i.e. part of the "semantic gap" mentioned earlier. FWIW, Forth's "types" aren't that precise about functions, e.g.: : triple ( n -- n ) 3 * ; : do-twice ( n xt -- n ) swap over execute swap execute ; : times-9 ( n -- n ) ['] triple do-twice ; In Haskell, we'd give do-twice a type like Integer -> (Integer -> Integer) -> Integer i.e. something like ( n ( n -- n ) -- n ) in pseudo-Forth notation.
[toc] | [prev] | [next] | [standalone]
Page 2 of 9 — ← Prev page 1 [2] 3 4 5 6 7 8 9 Next page →
Back to top | Article view | comp.lang.forth
csiph-web