Paul Rubin <no.em...@nospam.invalid> writes:
>an...@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>> Concerning being worth, I have far fewer type errors in Forth than in
>> Haskell.
>Do you mean type errors that the compiler didn't notice?
No, I mean that there are far fewer type errors in my Forth code than
type error messages for my Haskell code. Of course in Forth neither
the compiler nor the run-time system usually notices a type error, but
that's not what I claimed.
>When I wrote my first nontrivial Forth program, I several
>times said + when I meant F+, and of course the runtime happily added
>the wrong two stack items, causing later crashes that I then had to
>debug.
That's a type error, yes.
>Haskell's type system makes it feasible to write maintainable code in a
>quite abstract style involving higher-order functions, parametrized data
>types, and so on. This can also be done in Forth or Scheme but it gets
>confusing rather quickly.
I would have thought that it's the bread and butter of programming in
Scheme. Concerning parameterized data types, they are a solution for
a problem that you only have if you try to perform static type
checking.
> Having a computer keep track of the types
>takes cognitive burden off of the programmer,
I doubt that very much, because the programmer cannot write correct
programs if he does not keep track of the types himself.
> and makes refactoring
>easier (just fix the resulting type errors until the compiler stops
>complaining, and you probably have working code).
Paul Rubin <no.em...@nospam.invalid> writes:
>Doug Hoffman <glide...@gmail.com> writes:
>> If you are writing short, factored words, and testing each word before
>> continuing then that "+ instead of F+" should have become immediately
>> apparent and so no problem at all to notice and fix. No type checker
>> needed if you follow the recommended Forth way of writing a program.
>As I remember, it wasn't so immediately apparent what the problem was,
>since the failure didn't occur til a little ways after the + happened.
>And the symptom was that the program crashed without much clue about
>what had happened. Of course fancy debugging tools would have made it
>easier to trace and fix the problem, and it's not inherent in Forth that
>the implementation I used didn't happen to have them.
In my experience such a basic error as writing a + where there should
be an F+ shows up really quick, but maybe I avoid writing code where
it would not show up quickly.
Concerning fancy tools, I use the ~~ tracer (a more convenient variant
of what C programmers call printf debugging), and Gforth has
backtraces to let you know where an error happened. Some people like
a stepping debugger, but in my experience it's a good recipe for
wasting time. A back-stepping debugger with reverse watchpoints, now
that would be useful; apparently newer versions of gdb have that, but
I have not found the need for that yet.
>Anyway, if a type-checked language lets me write a page full of code and
>fix the compile-time errors to usually get working program, while the
>typeless counterpart makes me stop what I'm doing after basically every
>single line to check for problems the type checker would have caught
>automatically, I'd say the type checker has made itself worthwhile.
Why would I stop after every line? I typically write code until I
think it's time to test and debug, and then I start to test and debug.
While testing and debugging, it helps to have short words that can be
called individually.
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).
> 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).
> 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
...
Bernd Paysan <bernd.pay...@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:
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:
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:
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.
an...@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>>Do you mean type errors that the compiler didn't notice?
> No, I mean that there are far fewer type errors in my Forth code than
> type error messages for my Haskell code.
That could be a matter of differing programming styles between the two
languages. Like in Forth, if you have a value denoting an optional
string parameter, you might encode it as a null pointer if the string is
not present; or maybe you'd pass it as a struct with some kind of flag
indicating presence or absence. If there is some sort of error in
passing this around, it's not a type error, it's just a runtime bug. In
Haskell, you'd use a type of Maybe String, and then there are
potentially type errors that in Forth would just be bugs.
Then again it could be a matter of what you're used to.
>>quite abstract style involving higher-order functions...
> I would have thought that it's the bread and butter of programming in
> Scheme.
I think it's even more so in Haskell. Like the way one usually handles
iteration with map or fold instead of with recursion. I haven't seen
that much Scheme code written by experts though.
> I doubt that very much, because the programmer cannot write correct
> programs if he does not keep track of the types himself.
Yes of course you have to think about the types, but (compared to a
typeless language) you can let up a little on vigilance towards them and
devote your attention to other aspects of the program, since the
typechecker will catch the errors automatically. It's just like
interactively trying things in Forth except it's at compile time. You
can write some code that looks reasonable, then throw it at the
typechecker to see what happens, instead of agonizing over it checking
all the type assignments by hand.
Also, types can get very complicated, like in that red-black tree
example, where types track everything that happens to a complex data
structure through a complicated function. The corresponding situation
in Forth might be to treat stack effects as types, so some internal word
in the program may be operating on a stack dozens of levels deep, with a
hypothetical type checker keeping track of the whole stack contents so
it could (maybe only sometimes) statically detect overflow. A human
normally wouldn't track that carefully.
>> Anyway, if a type-checked language lets me write a page full of code and
>> fix the compile-time errors to usually get working program, while the
>> typeless counterpart makes me stop what I'm doing after basically every
>> single line to check for problems the type checker would have caught
>> automatically, I'd say the type checker has made itself worthwhile.
> Unit-testing every definition pays off handsomely in saved debugging
> time by catching all kinds of bugs, not just type errors.
> And my experience is similar to Anton's, in that I make very few type
> errors. This may be because I'm accustomed to matching the right
> operators to the right data type, whereas folks who are used to
> languages that do type inference are less conscious of it. But the
> majority of errors (not only for me but for programmers I work with) are
> logic/algorithm errors, and they're readily detected by unit testing
> each definition. Takes seconds, can save hours!
Writing a whole page of code at a time just has the wrong feel to doing the job right. Concentrate on the correctness of one function at a time, review the intent (as expressed in the glossary text you wrote to specify what was to happen) and test each word as you complete it (ensuring it meets the specification of the glossary). On this basis I built the techniques for certification of Forth code to ensure compliance with specification. No real hunting required for the hidden bugs as you should expunge them as you go to ensure they are not introduced in the first place. Of course, you need to really concentrate on getting the specification right first.
-- ********************************************************************
Paul E. Bennett...............<email://Paul_E.Benn...@topmail.co.uk>
Forth based HIDECS Consultancy
Mob: +44 (0)7811-639972
Tel: +44 (0)1235-510979
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
********************************************************************
> >> Anyway, if a type-checked language lets me write a page full of code and
> >> fix the compile-time errors to usually get working program, while the
> >> typeless counterpart makes me stop what I'm doing after basically every
> >> single line to check for problems the type checker would have caught
> >> automatically, I'd say the type checker has made itself worthwhile.
> > Unit-testing every definition pays off handsomely in saved debugging
> > time by catching all kinds of bugs, not just type errors.
> > And my experience is similar to Anton's, in that I make very few type
> > errors. This may be because I'm accustomed to matching the right
> > operators to the right data type, whereas folks who are used to
> > languages that do type inference are less conscious of it. But the
> > majority of errors (not only for me but for programmers I work with) are
> > logic/algorithm errors, and they're readily detected by unit testing
> > each definition. Takes seconds, can save hours!
> Writing a whole page of code at a time just has the wrong feel to doing the
> job right. Concentrate on the correctness of one function at a time, review
> the intent (as expressed in the glossary text you wrote to specify what was
> to happen) and test each word as you complete it (ensuring it meets the
> specification of the glossary). On this basis I built the techniques for
> certification of Forth code to ensure compliance with specification. No real
> hunting required for the hidden bugs as you should expunge them as you go to
> ensure they are not introduced in the first place. Of course, you need to
> really concentrate on getting the specification right first.
> --
> ********************************************************************
> Paul E. Bennett...............<email://Paul_E.Benn...@topmail.co.uk>
> Forth based HIDECS Consultancy
> Mob: +44 (0)7811-639972
> Tel: +44 (0)1235-510979
> Going Forth Safely ..... EBA.www.electric-boat-association.org.uk..
> ********************************************************************- Hide quoted text -
> - Show quoted text -
Agreed. And you also have to accept that you can't get your
documentation 100% perfect up-front. It's just a fact of life that
you'll discover something during the physical implementation that may
require you to add a new function (perhaps to handle an unanticipated
exception, for example) that will require you to re-vist and update
your documentation.
It's not Necessarily a design failure. It's just reality!
We spend weeks working on up-front software documentation. Working in
the mission-critical oil and gas business, it's just a normal part of
the design process. We're pretty good at it (we can design to SIL-1 on
our in-house designed and manufactured controllers) but we still come
across issues that we failed to anticipate, despite numerous peer
reviews and design reviews! They're never show-stoppers, but there's
always a gotcha lurking in there somewhere!
>> Writing a whole page of code at a time just has the wrong feel to doing
>> the job right. Concentrate on the correctness of one function at a time,
>> review the intent (as expressed in the glossary text you wrote to specify
>> what was to happen) and test each word as you complete it (ensuring it
>> meets the specification of the glossary). On this basis I built the
>> techniques for certification of Forth code to ensure compliance with
>> specification. No real hunting required for the hidden bugs as you should
>> expunge them as you go to ensure they are not introduced in the first
>> place. Of course, you need to really concentrate on getting the
>> specification right first.
> Agreed. And you also have to accept that you can't get your
> documentation 100% perfect up-front. It's just a fact of life that
> you'll discover something during the physical implementation that may
> require you to add a new function (perhaps to handle an unanticipated
> exception, for example) that will require you to re-vist and update
> your documentation.
This is so true too. I estimate that you will probably visit each part of the system 3 times during development (especially working on critical systems).
> It's not Necessarily a design failure. It's just reality!
> We spend weeks working on up-front software documentation. Working in
> the mission-critical oil and gas business, it's just a normal part of
> the design process.
Do you have a good grasp of the total concept at that time or is the specification still a collection of "I would like" type items? I have seen many organisations that do the up-front documentation on half baked design specs that still have lots of un-answered questions. The trick is usually to be a lot clearer about the full explicit requirements that will mean mission success early enough, even if all the fine details haven't yet emerged. This may take a number of review sessions that truly walk the problem space before the design really begins.
> We're pretty good at it (we can design to SIL-1 on
> our in-house designed and manufactured controllers) but we still come
> across issues that we failed to anticipate, despite numerous peer
> reviews and design reviews! They're never show-stoppers, but there's
> always a gotcha lurking in there somewhere!
There is no reason why you shouldn't deal with SIL-3 or SIL-4 requirements if you are able to improve your early design and development processes. Eliminate the systematic bugs before they get into the system design and you save a lot of time, effort and money in the later stages.
-- ********************************************************************
Paul E. Bennett...............<email://Paul_E.Benn...@topmail.co.uk>
Forth based HIDECS Consultancy
Mob: +44 (0)7811-639972
Tel: +44 (0)1235-510979
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
********************************************************************
> Doug Hoffman <glide...@gmail.com> writes:
>> If you are ... testing each word [ or unit , added 8/27 dbh ] before
>> continuing then that "+ instead of F+" should have become immediately
>> apparent...
> As I remember, it wasn't so immediately apparent what the problem was,
> since the failure didn't occur til a little ways after the + happened.
> And the symptom was that the program crashed without much clue about
> what had happened.
Interesting and surprising to hear that.
> Anyway, if a type-checked language lets me write a page full of code and
> fix the compile-time errors to usually get working program, while the
> typeless counterpart makes me stop what I'm doing after basically every
> single line to check for problems
No. Stopping after every line isn't exactly necessary. Depends on the length of your words and what you would consider a coherent/testable unit (may be several words as a group).
> the type checker would have caught
> automatically, I'd say the type checker has made itself worthwhile.
You might want to try StrongForth. Though it doesn't seem to have gained much traction.
Doug Hoffman <glide...@gmail.com> writes:
>> And the symptom was that the program crashed without much clue about
>> what had happened.
> Interesting and surprising to hear that.
Well, the issue probably would have been obvious to a more experienced
Forth user--I remember staring at the code for a while and seeing
nothing wrong, and having to go to some effort to debug the crash, and
as mentioned it took a couple of repeats for the lesson to sink in.
> No. Stopping after every line isn't exactly necessary. Depends on
> the length of your words and what you would consider a
> coherent/testable unit (may be several words as a group).
Most of my words are one line. Testing several as a group does seem to
make more sense.
> You might want to try StrongForth. Though it doesn't seem to have
> gained much traction.
Yeah, if I were doing anything serious with Forth I suppose I'd consider
it. For just fooling around as I'm doing, regular Forth's lack of
safety probably builds character ;-).
Paul Rubin <no.em...@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!" );
}
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:
> 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/
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
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/
>>> 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. 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. 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. I've programmed that way in Forth a little bit, but have been
> advised against it.
I meant to comment on this last week, but got distracted.
I don't like "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" but my reasons have nothing to do with data types or type checking, pro or con. It's just not a natural style for Forth. Most of the time, words are to be called, not treated as data. To be sure, there are times when explicit use of an xt is appropriate (with CATCH, with DEFERs, and in indexable tables of function pointers, mainly), but those are very specific application needs. The examples of that sort of thing I've seen posted here all strike me as wildly unreadable and unnecessarily obscure, and usually quite inefficient.
Cheers,
Elizabeth
-- ==================================================
Elizabeth D. Rather (US & Canada) 800-55-FORTH
FORTH Inc. +1 310.999.6784
5959 West Century Blvd. Suite 700
Los Angeles, CA 90045
http://www.forth.com
"Forth-based products and Services for real-time
applications since 1973."
==================================================
Andrew Haley <andre...@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:
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.
Paul Rubin <no.em...@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.
Bernd Paysan <bernd.pay...@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:
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. ;-).
an...@mips.complang.tuwien.ac.at (Anton Ertl) writes:
> In my experience such a basic error as writing a + where there should
> be an F+ shows up really quick, but maybe I avoid writing code where
> it would not show up quickly.
I think it took a while for me to debug because I hadn't yet gotten used
to hitting that kind of error.
> Some people like a stepping debugger, but in my experience it's a good
> recipe for wasting time. A back-stepping debugger with reverse
> watchpoints, now that would be useful
I find single stepping to be very helpful. I haven't tried a
back-stepping debugger but I can remember having wanted such a thing.
> Why would I stop after every line?
Other people on this newsgroup have been advising me to test each word
before writing the next one. Most of my words are 1 line. Yeah in
practice I tend to write several words before testing. It's certainly
seems true that testing in very small units helps quickly narrow what
part of the code is probably going wrong. Better diagnostics make that
narrowing less important, so I can code and test larger units, speeding
up development.
Bernd Paysan <bernd.pay...@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
> 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.
Paul Rubin <no.em...@nospam.invalid> wrote:
> Andrew Haley <andre...@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
Andrew Haley <andre...@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!"
Paul Rubin <no.em...@nospam.invalid> wrote:
> Andrew Haley <andre...@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".
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/
Doug Hoffman wrote: <503b9703$0$292$14726...@news.sunsite.dk>
> On 8/25/12 6:09 PM, Paul Rubin wrote:
>> the type checker would have caught
>> automatically, I'd say the type checker has made itself worthwhile.
> You might want to try StrongForth. Though it doesn't seem to have > gained much traction.
My impression of StrongForth is that it's an experimental/toy system,
not one intended for serious use. When Stephan came out with
StrongForth.f and I tried it, I quickly gave up because it choked on
several pieces of perfectly valid code which it simply didn't have the
type signatures to handle.
I had the impression that it would be relatively trivial to "finish" it
so that it was much more comfortable to use, but figured it was a really
bad sign that the author didn't care enough to do it in the first
place... And the code wasn't particularly well organized or readable to
my eye.
I still think it would be really cool to take the concept and produce a
clean, extensible static type checking library. I think you could do a
lot of neat things with it without it being too obtrusive.
Everything has it's place. I think systems are built in layers.
1) Machine code.
2) Assembly.
3) C, as the insecure cast acceptable, [] memory sequential indexing, and real control over byte ordering with a malloc. I would say forth can fit here.
4) A type abstraction language, with security proofs and restrictions on what can and can not be allocated or indexed into. Java fits here, although I would by choice have null removed and require a static null item declarator. Haskill could also fit here, even with it's higher order functions.
5) A weak typed all cast auto attempt script language, with underlying hidden types to ensure continual REPL or incremental operation without restart. Maybe even a reverse switch, and an execution buffer.
6) A strong functional interjection language, where available modules (auto profile space time optimized) are suggested to replace "intent code". The logic engine could even supply useful names for the possible behaviour which are detected at various "diagnosed effect entry points".
7) The far future..... where coders are metal and bank managers have no status.
