Home > Archive > Functional > April 2007 > mathementical/formal foundations of computing ?
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
mathementical/formal foundations of computing ?
|
|
| news@absamail.co.za 2007-02-22, 7:07 pm |
| 2 independant issues here:
1. I'm still searching for material re. "the mathementical/formal
foundation[s] of computing" to help move programming away from an
art towards a science. Patterns seem to be a heuristic step in that
direction ?
Here's some text re. the language :joy
http://www.latrobe.edu.au/philosoph...joy/j00ovr.html
> Overview of the language JOY
> Two other functional languages are the combinatory logic of Curry and
> the FP language of Backus. They are not based on the lambda calculus,
> they eliminate abstraction completely and hence do not have to deal
> with substitution and environments. As a result these languages can be
> manipulated using simple algebraic techniques
> ........Backus acknowledges a dept to
> combinatory logic, but his aim was to produce a variable free notation
> that is amenable to simple algebraic manipulation by people. Such ease
> should produce clearer and more reliable programs. .........
> Paulson remarked that "Programming and pure mathematics are
> difficult to combine into one formal framework". Joy attempts this task.
2. the second issue is about how NOT to write tutors.
The correct way is to chain-backwards from the goal.
Ie. put the 'bottom line' first, so the reader knows if he wants
to invest the labour to 'build forward' towards the goal.
I've been reading pages of the details of 'joy', without knowing
if & when & how it will claim to allow manipulation of 'joy code'
in a formal, mathematical way.
Q - does anybody know if joy can help me reach that goal ?
I don't want to learn another language which is a hybrid of forth, lisp
& pop-11 just to repeat "hello world: 2+3=5".
The correct way to present the capabilities which I/we s is:
1. In order to simplify/formalise/be-able-to-prove-XYZ, we
need to have the 'format ABC'.
2. This is acheived by transforming .....
3. On the basis of proven rules & manipulations ...
Ie. don't start with pages of rules & manipulations, where the
reader doesn't know if the effort will take him towards his goal.
== Chris Glur.
| |
| Chris Dollin 2007-02-22, 7:07 pm |
| news@absamail.co.za wrote:
> I don't want to learn another language which is a hybrid of forth, lisp
> & pop-11 just to repeat "hello world: 2+3=5".
pop-11 is /already/ viewable as a hybrid of forth and lisp.
--
Chris "electric hedgehog" Dollin
"People are part of the design. It's dangerous to forget that." /Star Cops/
| |
| Bruce McFarling 2007-02-22, 7:07 pm |
| On Feb 22, 9:50 am, n...@absamail.co.za wrote:
> 1. I'm still searching for material re. "the mathementical/formal
> foundation[s] of computing" to help move programming away from an
> art towards a science. Patterns seem to be a heuristic step in that
> direction ?
This may be the boy scout who helped the little old lady across the
street who did not want to cross the street.
The target of moving some aspects of programming from an art (ie,
craft) to a science is not to move all of programming to a science,
but to clear clutter from the palette to provide more leverage to the
craft of design.
Its like the move from pen to typewriter to word processor ... the
goal is not to eliminate the writer from the act of writing, it is to
reduce the effort of recording and editing the written word so that
attention can be focused on the actual composition.
| |
|
| On Feb 22, 7:50 am, n...@absamail.co.za wrote:
> 2 independant issues here:
>
> 1. I'm still searching for material re. "the mathementical/formal
> foundation[s] of computing" to help move programming away from an
> art towards a science. Patterns seem to be a heuristic step in that
> direction ?
>
> Here's some text re. the language :joyhttp://www.latrobe.edu.au/philosophy/phimvt/joy/j00ovr.html
>
>
> 2. the second issue is about how NOT to write tutors.
> The correct way is to chain-backwards from the goal.
> Ie. put the 'bottom line' first, so the reader knows if he wants
> to invest the labour to 'build forward' towards the goal.
>
> I've been reading pages of the details of 'joy', without knowing
> if & when & how it will claim to allow manipulation of 'joy code'
> in a formal, mathematical way.
>
> Q - does anybody know if joy can help me reach that goal ?
>
> I don't want to learn another language which is a hybrid of forth, lisp
> & pop-11 just to repeat "hello world: 2+3=5".
>
> The correct way to present the capabilities which I/we s is:
>
> 1. In order to simplify/formalise/be-able-to-prove-XYZ, we
> need to have the 'format ABC'.
>
> 2. This is acheived by transforming .....
>
> 3. On the basis of proven rules & manipulations ...
>
> Ie. don't start with pages of rules & manipulations, where the
> reader doesn't know if the effort will take him towards his goal.
>
> == Chris Glur.
| |
| arnuld 2007-02-22, 7:07 pm |
| > 1. I'm still searching for material re. "the mathementical/formal
> foundation[s] of computing" to help move programming away from an
> art towards a science.
ever tried algorithms ?
ever tried Google with keyword: Lisp (where functions are data)
also, http://www.cs.mu.oz.au/research/mercury/
> Patterns seem to be a heuristic step in that direction ?
you mean Desgn-Patterns ?
> Here's some text re. the language :joyhttp://www.latrobe.edu.au/philosophy/phimvt/joy/j00ovr.html
>
>
> 2. the second issue is about how NOT to write tutors.
> The correct way is to chain-backwards from the goal.
> Ie. put the 'bottom line' first, so the reader knows if he wants
> to invest the labour to 'build forward' towards the goal.
>
> I've been reading pages of the details of 'joy', without knowing
> if & when & how it will claim to allow manipulation of 'joy code'
> in a formal, mathematical way.
>
> Q - does anybody know if joy can help me reach that goal ?
>
> I don't want to learn another language which is a hybrid of forth, lisp
> & pop-11 just to repeat "hello world: 2+3=5".
>
> The correct way to present the capabilities which I/we s is:
>
> 1. In order to simplify/formalise/be-able-to-prove-XYZ, we
> need to have the 'format ABC'.
>
> 2. This is acheived by transforming .....
>
> 3. On the basis of proven rules & manipulations ...
>
> Ie. don't start with pages of rules & manipulations, where the
> reader doesn't know if the effort will take him towards his goal.
>
> == Chris Glur.
i can not understand that as my a programming Newbie.
| |
| Joachim Durchholz 2007-02-22, 7:07 pm |
| news@absamail.co.za schrieb:
> 1. I'm still searching for material re. "the mathementical/formal
> foundation[s] of computing" to help move programming away from an
> art towards a science.
First, programming is a craft, not an art (though it *can* be art, just
as craft can be art).
Second, mathematics alone isn't going to help programming move along. It
won't help with getting customer requirements into something that can be
programmed (mathematics could even be an obstacle here), and it won't
help with getting bugs out of programs (which is a question of human
error, and quality testing: again, the obstacles here are more human
than technological, and mathematics isn't going to help with that).
That doesn't mean that mathematics is unimportant in programming, just
as an architect needs mathematics to do his work when calculating loads
and stability. However, it's just a tool, not an end to be pursued.
That said, "functional programming languages" are "more mathematical" in
some sense, and they do have properties that make it easier to avoid the
technical bugs, and a portion of the customer requirements bugs, too.
That's not because it's mathematics, it's because being nearer to
mathematics simplifies the semantics of these languages...
> Patterns seem to be a heuristic step in that direction ?
No. Patterns are just like tricks of the trade: helpful if you know what
you're doing, nonsensical if you don't.
> Here's some text re. the language :joy
Language rationales list what the designers had in mind.
I have observed that few if any languages actually do as the designer
intended. Most underperform; a few overperform (Lisp and PHP being the
cases where the difference is most marked). Fewer perform as expected
(Haskell, I think).
> 2. the second issue is about how NOT to write tutors.
> The correct way is to chain-backwards from the goal.
> Ie. put the 'bottom line' first, so the reader knows if he wants
> to invest the labour to 'build forward' towards the goal.
An interesting thought, though I can't tell whether that style will be
successful. It's good to determine whether a language (or other
technology) fits your needs, but it doesn't help with actually learning
it, so I fear this style won't become very popular.
Regards,
Jo
| |
| Paul Rubin 2007-02-22, 7:07 pm |
| Joachim Durchholz <jo@durchholz.org> writes:
>
> An interesting thought, though I can't tell whether that style will be
> successful. It's good to determine whether a language (or other
> technology) fits your needs, but it doesn't help with actually
> learning it, so I fear this style won't become very popular.
Reading this group makes me feel like the underwear gnomes from South
Park:
1. Abstract category theory, GADT, Curry-Howard isomorphism, etc.
2. ???
3. Software!
I've bought into it enough to be spending time banging my head against
learning Haskell, but it would help a lot if step 2 were explained
better.
| |
| Jerry Avins 2007-02-22, 7:07 pm |
| news@absamail.co.za wrote:
> 2 independant issues here:
>
> 1. I'm still searching for material re. "the mathementical/formal
> foundation[s] of computing" to help move programming away from an
> art towards a science. Patterns seem to be a heuristic step in that
That direction is a dead end. It is no more possible to create a
mathematical/formal foundation[s] of computing than it is to create one
of bridge or cathedral design. To be sure, mathematics is a useful tool
in the process, but we would have no Ponte Veccio or Chartres if it were
the foundation.
The foundation is craft. Math builds on that foundation.
Jerry
--
Engineering is the art of making what you want from things you can get.
¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯
¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯
¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯
¯¯¯¯¯¯¯¯¯¯¯
| |
| Neelakantan Krishnaswami 2007-02-22, 7:07 pm |
| In article <7x7iuarlce.fsf@ruckus.brouhaha.com>, Paul Rubin wrote:
>
> Reading this group makes me feel like the underwear gnomes from South
> Park:
>
> 1. Abstract category theory, GADT, Curry-Howard isomorphism, etc.
> 2. ???
> 3. Software!
>
> I've bought into it enough to be spending time banging my head
> against learning Haskell, but it would help a lot if step 2 were
> explained better.
Step 2 is:
2. Algebraic structures == insanely effective design patterns for libraries
--
Neel R. Krishnaswami
neelk@cs.cmu.edu
| |
| Paul E. Bennett 2007-02-22, 7:07 pm |
| Joachim Durchholz wrote:
> news@absamail.co.za schrieb:
Which gets me wondering why he hasn't done a search on Formal methods with
google to start with before worrying us here.
[color=darkred]
> First, programming is a craft, not an art (though it *can* be art, just
> as craft can be art)
I'm with you on that front. It is also a craft that requires a degree of
skill and intelligence to accomplish a satisfactory end product.
> Second, mathematics alone isn't going to help programming move along. It
> won't help with getting customer requirements into something that can be
> programmed (mathematics could even be an obstacle here), and it won't
> help with getting bugs out of programs (which is a question of human
> error, and quality testing: again, the obstacles here are more human
> than technological, and mathematics isn't going to help with that).
I have seen some places where maths (formal methods) has been a help in
extracting sense out of complex customer requirements in order to re-write
the requirements in a way that made a great deal more sense to system
developers. It is a process best left to those with a distinctly weird bent
of mathematical mind. On the other hand, there are limitations to the use
of formal methods and it is of no use at all in some situations.
> That doesn't mean that mathematics is unimportant in programming, just
> as an architect needs mathematics to do his work when calculating loads
> and stability. However, it's just a tool, not an end to be pursued.
Sometimes a highly specialised tool that needs to be wielded by experts.
> That said, "functional programming languages" are "more mathematical" in
> some sense, and they do have properties that make it easier to avoid the
> technical bugs, and a portion of the customer requirements bugs, too.
> That's not because it's mathematics, it's because being nearer to
> mathematics simplifies the semantics of these languages...
Have heard a proponent of Haskell and Gopher talk of Forth as a language
that is half way between procedural and functional and "quite nice for some
things".
--
****************************************
****************************
Paul E. Bennett ....................<email://peb@amleth.demon.co.uk>
Forth based HIDECS Consultancy .....<http://www.amleth.demon.co.uk/>
Mob: +44 (0)7811-639972
Tel: +44 (0)1235-811095
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
****************************************
****************************
| |
| Paul Rubin 2007-02-23, 4:14 am |
| Neelakantan Krishnaswami <neelk@cs.cmu.edu> writes:
> Step 2 is:
> 2. Algebraic structures == insanely effective design patterns for libraries
Interesting, but similar library functions are showing up in languages
like C++ and Python, without all that theory, or am I missing something?
It also seems to me that the mathematical hair in the Haskell stuff
that I look at comes more from mathematical logic than from algebra.
Certainly all the stuff about types, which is pretty new to me (I did
get hold of Pierce's TAPL book and have started to look at it). I
can't help wondering how much of this approach is really necessary.
| |
| Logan Shaw 2007-02-23, 4:14 am |
| news@absamail.co.za wrote:
> 2 independant issues here:
>
> 1. I'm still searching for material re. "the mathementical/formal
> foundation[s] of computing" to help move programming away from an
> art towards a science.
You'll probably not have much luck in that. Programming consists of
making computers do what people want them to. People are capable
of wanting new things that break any formalism you come up with,
over and over and over again. That is why it is partially an art.
Now, understanding how computers work and what is possible can be
a science. But computer science is not programming.
> Patterns seem to be a heuristic step in that direction ?
I read an interesting perspective on patterns the other day, which
is that patterns are standard ways of dealing with weaknesses in
computer languages. Or to describe it a different way, patterns
are all about writing down abstractions that the languages doesn't
support so that you can do them the same way and not have to
reinvent them. If the language (or library, whatever) already supported
the abstraction, you wouldn't need the pattern; you would just ask the
language to do it.
I'm not sure whether I agree with this or not, but it raises an
interesting point: once we have added some abstractions into a
language, we think of more abstractions. We codify those as part
of the language, or we codify them as part of a book on design
patterns. But either way, we are codifying them. And why is that
important? Because once we are done codifying them, we move on
to the next thing.
The point here is that there will always be a next thing. No matter
how many abstractions you think of and nail down as a science, there
will be more that can be formed.
Does anyone ever seriously suggest that we ought to turn "coming up
with new theorems in math" into a science? What about coming up
with new axioms for mathematical systems that are interesting or
useful? Does anyone suggest we should make that into a scientific
process? No, because the point is that it requires high-level
analysis. The analysis *is* the work.
- Logan
| |
| Logan Shaw 2007-02-23, 4:14 am |
| Paul Rubin wrote:
> Reading this group makes me feel like the underwear gnomes from South
> Park:
>
> 1. Abstract category theory, GADT, Curry-Howard isomorphism, etc.
> 2. ???
> 3. Software!
>
> I've bought into it enough to be spending time banging my head against
> learning Haskell, but it would help a lot if step 2 were explained
> better.
I recommend banging your head against functional programming some more.
At some point, you gain some enlightenment out of it. I've even found
myself gravitating towards writing in short fragments of functional style
in C++ (constructors wrapped around constructors wrapped around
construtors...) and Perl (map() instead of for loop, etc.).
It's not the be-all and end-all of software (because *nothing* is or
ever will be), but there is something very satisfying about it.
- Logan
| |
| Paul Rubin 2007-02-23, 4:14 am |
| Logan Shaw <lshaw-usenet@austin.rr.com> writes:
> Does anyone ever seriously suggest that we ought to turn "coming up
> with new theorems in math" into a science?
Sure, Hilbert's formalist program of the 1930's, and prior to that,
Leibniz's in the 18th century. Hilbert's program apart when they
found out about Godel's incompleteness theorem, but for a while they
were trying to do precisely what you describe. Godel himself wrote to
von Neumann in the 1950's asking basically about the complexity of
proving decidable theorems leaving aside the undecidable ones; this
foresaw the development of NP-completeness theory.
I don't understand this foundations-of-computing stuff much myself,
but foundations of math is a perfectly respectable subject that
everyone should know something about. We have a much more precise
notion of what a mathematical theorem is today, than we had 100 years
ago. And it's only been recently that we've had full-blown formal
proofs of substantial theorems. We have a traditional "proof" thats
so complicated that nobody is sure it's correct (Hales' proof of
Kepler's conjecture) so we have the (ongoing) Flyspeck project to
settle the matter once and for all. And then we have godawful
software like Windows that crashes all the time; can we use (e.g.)
constructive type theory to make programs that verifiably do what
they're supposed to? I'm a wide-eyed newbie but this stuff seems much
more promising than the insanity that goes on in most of the software
world today.
| |
| Paul Rubin 2007-02-23, 4:14 am |
| Logan Shaw <lshaw-usenet@austin.rr.com> writes:
[color=darkred]
> I recommend banging your head against functional programming some more.
> At some point, you gain some enlightenment out of it. I've even found
> myself gravitating towards writing in short fragments of functional style
> in C++ (constructors wrapped around constructors wrapped around
> construtors...) and Perl (map() instead of for loop, etc.).
I'm not having much trouble with functional part (it's familiar from
Lisp and Scheme). It's the type systems that are confusing me. I've
borrowed a 600 page book about type systems (Pierce, TAPL) which I
hope will help, but I see that it's volume 1 of a two-volume work.
Sigh.
| |
| arnuld 2007-02-23, 4:14 am |
| > On Feb 23, 12:39 pm, Logan Shaw <lshaw-use...@austin.rr.com> wrote:
> Now, understanding how computers work and what is possible can be
> a science. But computer science is not programming.
what ?
then what is programming?
and how will you define computer science?
algorithms ?
i really want to understand what you are talking about. i want to
learn.
> I read an interesting perspective on patterns the other day, which
> is that patterns are standard ways of dealing with weaknesses in
> computer languages. Or to describe it a different way, patterns
> are all about writing down abstractions that the languages doesn't
> support so that you can do them the same way and not have to
> reinvent them. If the language (or library, whatever) already supported
> the abstraction, you wouldn't need the pattern; you would just ask the
> language to do it.
>
> I'm not sure whether I agree with this or not, but it raises an
> interesting point: once we have added some abstractions into a
> language, we think of more abstractions. We codify those as part
> of the language, or we codify them as part of a book on design
> patterns. But either way, we are codifying them. And why is that
> important? Because once we are done codifying them, we move on
> to the next thing.
>
> The point here is that there will always be a next thing. No matter
> how many abstractions you think of and nail down as a science, there
> will be more that can be formed.
Logan, it reminds me of Bruce Lee. this is exactly how he developed
"jeet kuan do" after geting dissatisfied with Wing-Chun and other
expert-styles.
-- arnuld
http://arnuld.blogspot.com
| |
| Joachim Durchholz 2007-02-23, 8:06 am |
| Paul Rubin schrieb:
> I can't help wondering how much of this approach is really necessary.
I'm not sure that you understood that the term "algebraic structures"
means just those sum types (unions-of-structs in C parlance), and
possibly the associated machinery (pattern matching in particular).
Of course, "algebraic structure" has less concepts than
"union-of-structs", and "union-of-structs" doesn't capture that the
entire thing is typesafe.
Propose a less intimidating terminology if you wish :-)
Regards,
Jo
| |
| Joachim Durchholz 2007-02-23, 8:06 am |
| Paul Rubin schrieb:
> And then we have godawful software like Windows that crashes all the
> time; can we use (e.g.) constructive type theory to make programs
> that verifiably do what they're supposed to?
Insofar as you can formalize a requirement, yes.
E.g. one approach that actually made it into practice is Spark (Ada with
those parts stripped that are difficult to reason about, plus a proof
checker).
Problems with this approach are:
a) Formal requirements can be longer than the programs that implement
them, and then you end up debugging the requirements. This makes the
method unsuitable for some tasks.
b) As soon as intangibles like aesthetics or almost-intangibles like
ergonomy come into play, there's no set of formal rules that you can
check against, so such requirements are impossible to verify with a
formalism.
c) You need a way to deal with situations where the formalism says
something and reality says something different. E.g. if a file read
operation fails because the disk was disconnected, and or some random
bit in RAM flipped, or whatever; and the formal requirements didn't
consider that case. You can largely ignore the issue for application
programs, but you cannot for operating systems and safety-critical
software. However, capturing such situations in a formalism is extremely
hard; in practice, people usually make sure that the system detects such
a failure and falls back to a restricted but safe mode of operation.
(Things get *really* hairy if there is no such mode, e.g. in nuclear
plants.)
Regards,
Jo
| |
| Joachim Durchholz 2007-02-23, 8:06 am |
| arnuld schrieb:
>
>
> what ?
>
> then what is programming?
>
> and how will you define computer science?
Computer science is scientific research about programming.
The relationship between computer science and programming is similar to
that between metallurgy and mechanical engineering.
> algorithms ?
Study of the property of algorithms is CS.
Implementing them is programming.
>
> Logan, it reminds me of Bruce Lee. this is exactly how he developed
> "jeet kuan do" after geting dissatisfied with Wing-Chun and other
> expert-styles.
The personal styles developed by martial arts experts are biased towards
the specific strengths and weaknesses of the developer. It is impossible
to appreciate the advantage of a specific style unless you have spent
years practicing it, at which point your opinion will be heavily biased.
I see a parallel to learning a concrete programming language here.
Different schools of sometimes violent opposition, each founded by an
"enlightened master".
Computer science is different. New knowledge about type systems is
always an improvement. (That's because it's just knowledge, not practice.)
Regards,
Jo
| |
| Ingo Menger 2007-02-23, 8:06 am |
| On Feb 23, 9:08 am, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
> Logan Shaw <lshaw-use...@austin.rr.com> writes:
>
> I'm not having much trouble with functional part (it's familiar from
> Lisp and Scheme). It's the type systems that are confusing me.
How?
> I've
> borrowed a 600 page book about type systems (Pierce, TAPL) which I
> hope will help, but I see that it's volume 1 of a two-volume work.
> Sigh.
This is as if you bought a work about thermodynamics in order to
better understand the engine of your car, and also in order to drive
better.
This is not to say that TAPL isn't a great book.
For me, the type discipline has been a blessing in all languages that
have some form of strong typing. Unfortunately, the ALGOL descendants
require us to always write down the obvious, sometimes twice, as e.g.
in java:
List<Map<String, Integer>> foo = new
LinkedList<HashMap<String,Integer>>();
AFAIK, C# has (or will have) something called local type inference,
that would allow to drop at least part of the clutter.
But, in functional languages, it is just wonderfull, when the compiler
says something like: Look, here you use "foo bar" as a list, but in
the definition of foo, you don't compute a list. This is surely not
what you intended, ohh great master.
| |
| Tester 2007-02-23, 7:09 pm |
| On Thu, 22 Feb 2007 08:50:49 -0600, news@absamail.co.za wrote:
j
>2 independant issues here:
>
>1. I'm still searching for material re. "the mathementical/formal
>foundation[s] of computing" to help move programming away from an
>art towards a science. Patterns seem to be a heuristic step in that
>direction ?
>
Are most aspects of the formal mathematical theory of computing all
that relevant to the day-to-day process of coming up with practical
programs which will handle the data they are likely to be given in
reasonable time and space?
For example, consider:
http://en.wikipedia.org/wiki/NP-complete
How is this likely to make practical computing more of a science?
| |
| Joachim Durchholz 2007-02-23, 7:09 pm |
| Tester schrieb:
> http://en.wikipedia.org/wiki/NP-complete
>
> How is this likely to make practical computing more of a science?
NP-completeness and undecidability just delinate what a knowledgeable
programmer will simply refuse to do, on grounds that it can't be done.
(Similar to an engineer who will refuse to build a dam made of bubblegum.)
Most of the time, other issues than the limits of what can be computed
in reasonable space and time are more prevalent. Such as bridging the
gap between requirements and programs, debugging, hardening against
attacks, occasionally performance improvements, and adapting software to
changing requirements.
Regards,
Jo
| |
| J Thomas 2007-02-23, 7:09 pm |
| On Feb 23, 11:32 am, Joachim Durchholz <j...@durchholz.org> wrote:
> Tester schrieb:
>
>
>
> NP-completeness and undecidability just delinate what a knowledgeable
> programmer will simply refuse to do, on grounds that it can't be done.
No, that's a red herring. For some particular NP-complete problem you
might find that a solution for N=100 would take the current entire
world computing resources a million years to solve. But if your
customer wants a solution for N=50 and you can get your N=50 solution
in 250 milliseconds on an old PC, why refuse the job?
NP-completeness deserves at most a warning to the customer about
future upgrade problems.
> (Similar to an engineer who will refuse to build a dam made of bubblegum.)
Doesn't it depend on the job? A small dam that needs only a short
lifespan might feasibly be made of bubblegum, though some other
material might fit the needs better and/or cheaper.
| |
| Paul Rubin 2007-02-23, 7:09 pm |
| Joachim Durchholz <jo@durchholz.org> writes:
> I'm not sure that you understood that the term "algebraic structures"
> means just those sum types (unions-of-structs in C parlance), and
> possibly the associated machinery (pattern matching in particular).
I see, thanks. I thought it meant the collection of higher order
functions in libraries that are easily composible so you end up
writing programs that are sort of like commutative diagrams.
The part I'm having trouble with is the connection between
theoretical, foundational stuff and actual programming. In most other
programming language communities there's a vast disconnect between
foundations and practice, just like automobile engineering usually
doesn't concern itself with elementary particle physics.
> Of course, "algebraic structure" has less concepts than
> "union-of-structs", and "union-of-structs" doesn't capture that the
> entire thing is typesafe.
> Propose a less intimidating terminology if you wish :-)
This is pretty  , and I think it's more like C++ templates than
union-of-structs.
| |
| Paul Rubin 2007-02-23, 7:09 pm |
| "Ingo Menger" <quetzalcotl@consultant.com> writes:
> How?
It's a lot of new stuff to try to internalize. As a simple example,
I don't understand why (Maybe a) is a monad. Past that, there's
a bunch of concepts like "higher kinded polymorphism" where I don't
even know what the words mean.
I also have trouble figuring out what's wrong with a program based on
error messages from Hugs. I don't know if that's from my own
inexperience or because the error messages actually aren't very good.
However it seems like the compiler faces a difficult problem, type
inference in the presence of type classes, so it doesn't know the
initial concrete type of anything. It's as if it tries to solve some
big system of equations based on type info from 17 different places in
the program, finds there's no solution, and announces that the program
must have an error, but is not so helpful in saying where the error is.
> But, in functional languages, it is just wonderfull, when the compiler
> says something like: Look, here you use "foo bar" as a list, but in
> the definition of foo, you don't compute a list. This is surely not
> what you intended, ohh great master.
That's nice in theory but the error messages (so far) are often hard
to understand. All I can tell is that the compiler was complaining
about -something-. Maybe it's easier in ML than in Haskell, because
there aren't type classes.
| |
| Joachim Durchholz 2007-02-23, 7:09 pm |
| Paul Rubin schrieb:
> That's nice in theory but the error messages (so far) are often hard
> to understand.
That's a typical newcomer problem in Haskell.
It seems that you get used to finding the real sources of the errors,
similar to when you get a syntax error, you almost automatically look at
the line *before* the one that the error was reported in.
Regards,
Jo
| |
| Thant Tessman 2007-02-23, 7:09 pm |
| Paul Rubin wrote:
> Joachim Durchholz <jo@durchholz.org> writes:
[...]
>
> This is pretty , and I think it's more like C++ templates than
> union-of-structs.
This is the closest I've ever seen C++ come to capturing the concept.
And it still isn't quite there:
www.oonumerics.org/tmpw01/alexandrescu.pdf
-thant
| |
| Paul Rubin 2007-02-23, 7:09 pm |
| Joachim Durchholz <jo@durchholz.org> writes:
> It seems that you get used to finding the real sources of the errors,
> similar to when you get a syntax error, you almost automatically look
> at the line *before* the one that the error was reported in.
Thanks, I'll keep that in mind. For amusement purposes, here's a
syntax error that  me. I did manage to fix it by trial and
error, but I'm still not absolutely clear on the exact workings of the
rule that it broke. I'd be interested to know if you can spot the
error without trying to compile the program. In my case, even with
the error message I was not able to figure out what was wrong except
through a bunch of experiments.
main :: IO ()
main = do
putStr "Enter num1: "
n1 <- read1 "n1: "
putStr "enter operation: "
op <- getLine
n2 <- read1 "Enter num2: "
let func = case op of
"+" -> Just (+);
"-" -> Just (-);
"*" -> Just (*);
"/" -> Just (/);
"**" -> Just (**);
_ -> Nothing
case func of
Nothing -> print "unknown operator"
Just op -> print (n1 `op` n2)
main -- loop
| |
| Phil Armstrong 2007-02-23, 7:09 pm |
| Paul Rubin <http://phr.cx@nospam.invalid> wrote:
> It's a lot of new stuff to try to internalize. As a simple example,
> I don't understand why (Maybe a) is a monad. Past that, there's
> a bunch of concepts like "higher kinded polymorphism" where I don't
> even know what the words mean.
(Maybe a) happens to be a monad because it obeys the Monad laws.
> That's nice in theory but the error messages (so far) are often hard
> to understand. All I can tell is that the compiler was complaining
> about -something-. Maybe it's easier in ML than in Haskell, because
> there aren't type classes.
Sometimes it's helpful to start putting type annotations on your
functions to push the error around until it gets to the point where
you've made the actual mistake (as against the point where the
compiler finally notices that it has two irreconcilable types and
gives up, which can of course be somewhere else entirely.)
Phil
--
http://www.kantaka.co.uk/ .oOo. public key: http://www.kantaka.co.uk/gpg.txt
| |
| Paul Rubin 2007-02-23, 7:09 pm |
| Phil Armstrong <phil-news@kantaka.co.uk> writes:
> (Maybe a) happens to be a monad because it obeys the Monad laws.
Well why does it even support the >>= operator? It could be that
I'm simply about how typeclasses work, but I thought something
like that couldn't happen by accident.
| |
| Neelakantan Krishnaswami 2007-02-23, 7:09 pm |
| In article <7xzm75qug2.fsf@ruckus.brouhaha.com>, Paul Rubin wrote:
> Neelakantan Krishnaswami <neelk@cs.cmu.edu> writes:
>
> Interesting, but similar library functions are showing up in
> languages like C++ and Python, without all that theory, or am I
> missing something?
I don't think this is quite true. Many of the simpler constructions
show up, but as a general tendency the more complex ones do not. I
think this is because you don't get enough language support to use
them effectively. Either you don't get enough typechecking support
to catch stupid but hard-to-debug errors (eg, in Python), or the type
annotations you must write grow without bound (eg, Java or C++).
> It also seems to me that the mathematical hair in the Haskell stuff
> that I look at comes more from mathematical logic than from algebra.
> Certainly all the stuff about types, which is pretty new to me (I
> did get hold of Pierce's TAPL book and have started to look at it).
> I can't help wondering how much of this approach is really
> necessary.
If you're a mathematically minded programmer, you'll start noticing
all the algebraic structures that appear in your program -- for
example, you'll recognize that time intervals form a vector field,
that integers form a ring, that strings form a monoid, and so on. So
you'll start organizing your APIs to emphasize the algebraic
properties of each type, and then you'll start to hack.
At that point, you'll notice that your code is mostly transformations
from one type to another, and most of them have homomorphic structure.
At this point, the natural thing (for a mathematician) is to start
using some category theory to organize all these types and mappings
between them.
This turns out to connect very naturally to type theory, because the
typed lambda calculus has a very elegant categorical semantics. So now
your programs end up very tightly connected to the semantic, algebraic
concepts you had: your programs are the constructive witnesses to the
existential statements in the math.
It all kind of happens just by following your nose, and I think that's
really, really .
--
Neel R. Krishnaswami
neelk@cs.cmu.edu
| |
| Mark T.B. Carroll 2007-02-23, 7:09 pm |
| Paul Rubin <http://phr.cx@NOSPAM.invalid> writes:
> Phil Armstrong <phil-news@kantaka.co.uk> writes:
>
> Well why does it even support the >>= operator?
Largely because it makes some sort of sense for it to.
> It could be that I'm simply about how typeclasses work, but I
> thought something like that couldn't happen by accident.
Indeed it doesn't: somewhere in the standard libraries there'll be an
instance definition for Maybe being an instance of Monad.
Monads are often about chaining computations together in one way or
another. The Maybe monad basically says, if one part of the computation
fails (returning Nothing), don't bother with the rest of it, just return
Nothing for the whole thing.
Mark.
--
Functional programming vacancy at http://www.aetion.com/
| |
| Daniel C. Wang 2007-02-23, 10:07 pm |
| Joachim Durchholz wrote:
{stuff deleted}
> Insofar as you can formalize a requirement, yes.
>
> E.g. one approach that actually made it into practice is Spark (Ada with
> those parts stripped that are difficult to reason about, plus a proof
> checker).
BTW I've heard the Spark people give a talk, they basically were
verifying that their software implemented a particular military
encryption algorithm correctly.
The ACL2 folk have verified both hardware and software stacks implement
various other security related systems correctly.
| |
| arnuld 2007-02-24, 4:16 am |
| > On Feb 23, 3:52 pm, Joachim Durchholz <j...@durchholz.org> wrote:
> arnuld schrieb:
>
>
>
>
>
>
> Computer science is scientific research about programming.
>
> The relationship between computer science and programming is similar to
> that between metallurgy and mechanical engineering.
>
>
> Study of the property of algorithms is CS.
> Implementing them is programming.
ok
>
>
> The personal styles developed by martial arts experts are biased towards
> the specific strengths and weaknesses of the developer.
Bruce Lee's "Jeet Kuan Do" style is *no style*. you adapt your self
according to the present situation, you develop a new style every time
you use Jeet Kuan Do. Jeet Kuan Do means, how one can express himself,
totally and completel, without any restrictions imposed by all other
styles, Wing-Chun e.g.
> It is impossible
> to appreciate the advantage of a specific style unless you have spent
> years practicing it, at which point your opinion will be heavily biased.
you can't practice Jeet Kuan Do for years because, as i said, if you
spend years practicing on Bruce Lee's style, then you are just
practicing a new style everyday
> I see a parallel to learning a concrete programming language here.
> Different schools of sometimes violent opposition, each founded by an
> "enlightened master".
>
> Computer science is different. New knowledge about type systems is
> always an improvement. (That's because it's just knowledge, not practice.)
>
> Regards,
> Jo
| |
| arnuld 2007-02-24, 4:16 am |
| > On Feb 23, 3:52 pm, Joachim Durchholz <j...@durchholz.org> wrote:
> I see a parallel to learning a concrete programming language here.
> Different schools of sometimes violent opposition, each founded by an
> "enlightened master".
yes, it is. IMVHO, Martial-Arts, Hacking and Music Composition are
very-closely related, as per my experience. yu can check the article
on my BLOG on this.
--arnuld
http://arnuld.blogspot.com
| |
| arnuld 2007-02-24, 4:16 am |
| On Feb 24, 9:48 am, "arnuld" <g.arn...@gmail.com> wrote:
>
> yes, it is. IMVHO, Martial-Arts, Hacking and Music Composition are
> very-closely related, as per my experience. yu can check the article
> on my BLOG on this.
>
to be clear, what i i meant by "yes, it is". it means, next sentence
is right:
"i see a parallel to learning a concrete programming language"
| |
| Marlene Miller 2007-02-24, 4:16 am |
| "Paul Rubin" wrote:
> I'm not having much trouble with functional part (it's familiar from
> Lisp and Scheme). It's the type systems that are confusing me. I've
> borrowed a 600 page book about type systems (Pierce, TAPL) which I
> hope will help, but I see that it's volume 1 of a two-volume work.
> Sigh.
You might be interested in the lectures notes for a class Pierce taught last
fall.
http://www.cis.upenn.edu/~bcpierce/home.html
See Old Course Materials: Software Foundations, Schedule
(I downloaded the lectures and exams with solutions, because I plan to read
TAPL after EoPL and ToPL - if I live that long - and I am not sure how long
the links will stay around.)
Marlene
| |
| Paul Rubin 2007-02-24, 4:16 am |
| "Marlene Miller" <marlenemiller@worldnet.att.net> writes:
> You might be interested in the lectures notes for a class Pierce taught last
> fall.
> http://www.cis.upenn.edu/~bcpierce/home.html
Thanks, interesting. "A Gentle Introduction to Haskell" is also
looking useful. I think I looked at it when I was first getting
started and couldn't make sense of it then, but it's easier now.
| |
| Markus E Leypold 2007-02-24, 4:16 am |
|
"J Thomas" <jethomas5@gmail.com> writes:
> On Feb 23, 11:32 am, Joachim Durchholz <j...@durchholz.org> wrote:
>
> No, that's a red herring. For some particular NP-complete problem you
> might find that a solution for N=100 would take the current entire
> world computing resources a million years to solve. But if your
> customer wants a solution for N=50 and you can get your N=50 solution
> in 250 milliseconds on an old PC, why refuse the job?
>
> NP-completeness deserves at most a warning to the customer about
> future upgrade problems.
Ah - no. Some 15 years ago I had a customer who wanted a custom
database (and UI) which would be loaded with ~2000 records of
potential customers. The first thing he then did, was to load it with
all ~20000 data sets from a CD directory (kind of an industry guide).
Since the index building algorithm was all but efficient (we took some
short cuts because dur to limited memory we could not just sort in
memory), the first build of the index of the larger database took more
than 2 days.
So scaling is not only an upgrade problem: Often your customer is a
bit vague about the problem size and you should probably write scaling
behaviour in the specs.
>
> Doesn't it depend on the job? A small dam that needs only a short
> lifespan might feasibly be made of bubblegum, though some other
> material might fit the needs better and/or cheaper.
Right. But without theory you might just use bubble gum for every dam,
since you don't knoe about the principal restrictions of using bubble
gum.
My answer to the OP, BTW, would have been Jo's.
And, @tester: where do ypu read this thread? I don't want to continue
cross posting.
Regards -- Markus
| |
| Ingo Menger 2007-02-24, 8:07 am |
| On 23 Feb., 20:31, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
> "Ingo Menger" <quetzalc...@consultant.com> writes:
>
> That's nice in theory but the error messages (so far) are often hard
> to understand. All I can tell is that the compiler was complaining
> about -something-. Maybe it's easier in ML than in Haskell, because
> there aren't type classes.
Not really. It's - unfortunatley - a property of the basic type
inference algorithm. AFAIK, there is some research going on to make
things better in this respect. Your notion of a set of equations that
can't be solved is not so far off the mark.
It helps sometimes to keep in mind that type inference has a left to
right bias (although not necessarily a top to bottom one), so, for
example, in
foo xs = head xs && xs
the compiler will most probably infer xs :: [Bool] (from the
definition of head and the appearance of (head xs) as first argument
of &&) and then it will bitterly complain that it can't unify Bool and
[Bool]. But note that if it'd do it the other way around, assuming
first that xs must be Bool, the result would be no better. In any
case, the compiler arrives at some conclusion about the type a certain
variable should have, and then it will stick to that, even if all
other uses clearly suggest another type. Often, this will be
counterintuitive to the human mind (which has it's own notion about
this matter).
Note that this example is quite simple, it is perhaps not a good idea
to propose, that the compiler should print out a detailed log about
what assumptions it has made, and how they were justified. A single
error message could easily become 1000 lines and more this way.
As others have pointed out, whenever you have problems with the type
system, you should explicitely annotate your definitions. Not only
will the error messages get more understandable, but the discipline of
thinking every moment about the question: "Well, what will the type of
this expression, this function, this variable be?" will most probably
prevent you from making type errors in the first place.
Last but not least: No matter how bad the messages from the type
inference algorithm are, they are certainly more informative than
Segmentation fault, core dumped
which is what you get when you run programs containing type errors
written in languages that allow you to confuse a boolean and a list of
booleans.
| |
| Chris Uppal 2007-02-24, 7:03 pm |
| Paul Rubin wrote:
> I also have trouble figuring out what's wrong with a program based on
> error messages from Hugs. I don't know if that's from my own
> inexperience or because the error messages actually aren't very good.
It would be nice if there was some sort of switch to tell the system "I
know it's wrong, but I want to run it anyway", perhaps implemented as
some simple meta-interpreter. Beginers could then /watch/ it go wrong
in the debugger (I assume there's a halfway decent debugger available?)
which is usually enlightening.
For all I know, the feature may already be there.
-- chris
| |
| Arthur J. O'Dwyer 2007-02-24, 7:03 pm |
|
On Sat, 24 Feb 2007, Chris Uppal wrote in comp.programming:
> Paul Rubin wrote:
>
> It would be nice if there was some sort of switch to tell the system "I
> know it's wrong, but I want to run it anyway", perhaps implemented as
> some simple meta-interpreter. Beginers could then /watch/ it go wrong
> in the debugger (I assume there's a halfway decent debugger available?)
> which is usually enlightening.
I believe this thread is discussing languages which are high-level
enough that "run it anyway" is a meaningless request. If the program
is malformed, you /can't/ "run it anyway"; there's no legal program
present to run!
Some interpreted languages (Turbo Pascal 3.0, Perl) will let you
start running a malformed program, bailing only when they get to the
unrecoverable error. However, those languages are far closer to the
machine than ML or Haskell, and don't do lots of inferences about
type, so they can afford to "ignore" large parts of the program at
first. With type inference, you need to figure out all the types in
advance, whether they're on executable codepaths or not.
And with a compiled language, the compiler /must/ understand everything
in the program, because it has to translate it to machine code. There's
no way for the compiler to "ignore" parts of the program it doesn't
understand; everything must be assigned a meaning.
HTH,
-Arthur
| |
|
| In message <1172155799.675959@vasbyt.isdsl.net>
news@absamail.co.za wrote:
> 2 independant issues here:
>
> 1. I'm still searching for material re. "the mathementical/formal
> foundation[s] of computing" to help move programming away from an
> art towards a science. Patterns seem to be a heuristic step in that
> direction ?
Have you read Edsger Dijkstra's "A discipline of programming"
or David Gries' "The science of programming"?
Regards,
Arjan
| |
| Paul Rubin 2007-02-24, 7:03 pm |
| Arjan <arjan@example.com> writes:
> Have you read Edsger Dijkstra's "A discipline of programming"
> or David Gries' "The science of programming"?
Those sound hopelessly out of date. I looked at Dijkstra's book
a long time ago but I think current approaches are much different.
Someone on #haskell recommend this a while back:
http://www-2.cs.cmu.edu/~rwh/plbook/
It looks excellent and I hope to read it someday.
| |
|
|
| Ben Pfaff 2007-02-24, 7:03 pm |
| "Arthur J. O'Dwyer" <ajonospam@andrew.cmu.edu> writes:
> Some interpreted languages (Turbo Pascal 3.0, Perl) will let you
> start running a malformed program, bailing only when they get to the
> unrecoverable error.
I used Turbo Pascal 3.0 back in, um, perhaps 1988 or so, and I
don't remember it working that way. It compiled the whole
program, then ran it. Is there some newer product also called
Turbo Pascal 3.0 that works differently?
--
"In the PARTIES partition there is a small section called the BEER.
Prior to turning control over to the PARTIES partition,
the BIOS must measure the BEER area into PCR[5]."
--TCPA PC Specific Implementation Specification
| |
| Benjamin Franksen 2007-02-24, 7:03 pm |
| Joachim Durchholz wrote:
> Paul Rubin wrote:
>
> I'm not sure that you understood that the term "algebraic structures"
> means just those sum types (unions-of-structs in C parlance), and
> possibly the associated machinery (pattern matching in particular).
>
> Of course, "algebraic structure" has less concepts than
> "union-of-structs", and "union-of-structs" doesn't capture that the
> entire thing is typesafe.
> Propose a less intimidating terminology if you wish :-)
I think you misunderstood 'algebraic structure', especially as an 'insanely
effective design pattern for libraries'. The term here refers to the set of
algebraic laws that are satisfied by the operations exported from the
library. In most cases the interface to such a library /must/ make the
exported data types abstract so that the laws can be guaranteed to hold.
The so called 'algebraic data types' you are refering to are merely the
basic building blocks, one could say they are '0-th order' algebraic
structures, that is, the laws that apply to them are the ones guaranteed by
the language alone.
The following paper was a real eye-opener for me. It explains how the right
algebraic structure leads to a simpler, yet more effective interface. It
also explains how to use such laws internally to tweak performance while
maintaining correctness.
homepages.inf.ed.ac.uk/ wadler/papers/prettier/prettier.pdf
Cheers
Ben
| |
| Randy Howard 2007-02-24, 7:03 pm |
| On Sat, 24 Feb 2007 14:23:20 -0600, Ben Pfaff wrote
(in article <87hctbz4nb.fsf@blp.benpfaff.org> ):
> "Arthur J. O'Dwyer" <ajonospam@andrew.cmu.edu> writes:
>
>
> I used Turbo Pascal 3.0 back in, um, perhaps 1988 or so,
I used it earlier than that, probably 3 or 4 years at least.
> and I don't remember it working that way.
Neither do I.
> It compiled the whole program, then ran it.
Right, no interpreter at all. No idea what he's talking about.
--
Randy Howard (2reply remove FOOBAR)
"The power of accurate observation is called cynicism by those
who have not got it." - George Bernard Shaw
| |
| Benjamin Franksen 2007-02-24, 7:03 pm |
| Paul Rubin wrote:
> For amusement purposes, here's a
> syntax error that me. _I did manage to fix it by trial and
> error, but I'm still not absolutely clear on the exact workings of the
> rule that it broke. _I'd be interested to know if you can spot the
> error without trying to compile the program. _In my case, even with
> the error message I was not able to figure out what was wrong except
> through a bunch of experiments.
>
> main :: IO ()
> main = do
> putStr "Enter num1: "
> n1 <- read1 "n1: "
> putStr "enter operation: "
> op <- getLine
> n2 <- read1 "Enter num2: "
> let func = case op of
> "+" -> Just (+);
> "-" -> Just (-);
> "*" -> Just (*);
> "/" -> Just (/);
> "**" -> Just (**);
> _ -> Nothing
>
> case func of
> Nothing -> print "unknown operator"
> Just op -> print (n1 `op` n2)
>
> main -- loop
I suppose it's something to do either with the indentation of the (first)
case branches or with the semicolons separating them (or both). The
semicolons are not necessary (since you are using layout anyway) and may
interfere with the 'let'. I'd leave them out. And the case branches ("+" ->
Just (+) etc...) should be indented at least one space further than the
start of the let item (starting with "func = case op of").
Haskell's layout rule really has its subtleties, especially in connection
with do-notation. There are some pitfalls that almost all beginners fall
into.
Cheers
Ben
| |
| Benjamin Franksen 2007-02-24, 7:03 pm |
| Phil Armstrong wrote:
> Paul Rubin <http://phr.cx@nospam.invalid> wrote:
>
> (Maybe a) happens to be a monad because it obeys the Monad laws.
More precisely, (Maybe a) /can be viewed as/ a monad by giving suitable
definitions of (>>=) and (return). Here, 'suitable' is of course meant to
entail that the monad laws are obeyed, but to be useful the monad should be
non-trivial, too.
Cheers
Ben
| |
| Paul Rubin 2007-02-24, 7:03 pm |
| Benjamin Franksen <benjamin.franksen@bessy.de> writes:
> I suppose it's something to do either with the indentation of the (first)
> case branches or with the semicolons separating them (or both).
Oh woops, I put in the semicolons while trying to debug the problem
and then I forgot to take them out. And yes, the problem was that the
case branches were not indented far enough. It amazed me. Coming
from Python, I was used to significant indentation, but Haskell's
indentation rules are more complex and seem to make less sense, and
theyaren't described in the tutorial I looked at.
In Python, if you indent a line further to the right than the previous
line, the lexical scanner calls that an "indent" and if you indent it
further to the left than the previous line, the scanner calls it a
"dedent". Python's "indent" and "dedent" are equivalent to begin/end
or left and right curly braces in other languages. But the amount of
additional indentation is not significant. Only the direction matters.
| |
| Joachim Durchholz 2007-02-24, 7:03 pm |
| Arthur J. O'Dwyer schrieb:
> With type inference, you need to figure out all the types in
> advance, whether they're on executable codepaths or not.
Sorry, that's plain wrong.
You can always assign an Error type to those names where type inference
didn't give a meaningful result, and run the code anyway. Just make sure
you have run-time checks in place when assigning to or from that name,
that's all you need to do to get a perfectly running program (which may
terminate with a type error, of course, but hey! - that's what was
requested).
> And with a compiled language, the compiler /must/ understand
> everything in the program, because it has to translate it to machine
> code.
That's even more wrong. You can do type checks with machine code just fine.
There's one thing you need to do: have the type information available at
runtime. If you leave that out, then the run-time system will have
trouble checking types (unsurprisingly).
I'm not sure how much of an impact on run-time system design that has.
It would probably be part of making the run-time data structures
printable (and without that "just running the code" doesn't make much
sense, you want to see the code in action), so it's probably no
additional overhead anyway.
Regards,
Jo
| |
| J Thomas 2007-02-25, 4:06 am |
| On Feb 23, 12:13 pm, Markus E Leypold
<development-2006-8ecbb5cc8aREMOVET...@ANDTHATm-e-leypold.de> wrote:
> "J Thomas" <jethom...@gmail.com> writes:
[color=darkred]
>
>
>
> Ah - no. Some 15 years ago I had a customer who wanted a custom
> database (and UI) which would be loaded with ~2000 records of
> potential customers. The first thing he then did, was to load it with
> all ~20000 data sets from a CD directory (kind of an industry guide).
> Since the index building algorithm was all but efficient (we took some
> short cuts because dur to limited memory we could not just sort in
> memory), the first build of the index of the larger database took more
> than 2 days.
>
> So scaling is not only an upgrade problem: Often your customer is a
> bit vague about the problem size and you should probably write scaling
> behaviour in the specs.
Yes, but at this point I believe that NP-complete is a red herring.
What the customer cares about is at what N the resources become an
issue, and at what N the solution becomes impractical.
As I understand it, to prove a problem is NP-complete or prove it
isn't, will not in either case answer those questions. To know that
scaling issues will at some point make the solution completely
impractical doesn't at all say whether it's impractical for the
customer's uses. And vice versa, it can scale gently and be too
unwieldy even at the scale the customer needs now.
So it looks to me like finding out whether it's NP-complete is solving
the wrong problem. What you need to know is something else. Some of
the details you use to decide NP-completely might be used for that
other question, though.
>
>
> Right. But without theory you might just use bubble gum for every dam,
> since you don't knoe about the principal restrictions of using bubble
> gum.
If you don't understand your materials you can expect problems. On the
other hand, civil engineering has traditionally operated with a very
large component of precedent. If a theoretician decides that a
particular procedure is unsafe, but it has been in widespread use
without incident, he's likely to generate lots of comments about
proofs that bumblebees can't fly. On the other hand if a design is
constructed with traditional safety margins much reduced because
theory says they're not needed, it's likely to get a lot of interest
while the engineers wait for it to fall down.
Theory is a useful supplement to practice. When you operate outside
your area of expertise it's all you have. And this is probably why
people are generally so hesitant to do significant projects outside
their areas of expertise.
| |
| J Thomas 2007-02-25, 4:06 am |
| On Feb 24, 4:38 pm, Benjamin Franksen <benjamin.frank...@bessy.de>
wrote:
> Paul Rubin wrote:
[color=darkred]
> I suppose it's something to do either with the indentation of the (first)
> case branches or with the semicolons separating them (or both). The
> semicolons are not necessary (since you are using layout anyway) and may
> interfere with the 'let'. I'd leave them out. And the case branches ("+" ->
> Just (+) etc...) should be indented at least one space further than the
> start of the let item (starting with "func = case op of").
>
> Haskell's layout rule really has its subtleties, especially in connection
> with do-notation. There are some pitfalls that almost all beginners fall
> into.
This is why I say it's important for Forth to become more intuitive
for beginners. Each little trap that beginners predictably fall into
is a barrier, something that lengthens the learning curve.
Of course it's hard to expect the experts to change their habits for
beginners, when we have so many more experts than beginners. But
stil....
| |
| Bjorn Reese 2007-02-25, 8:03 am |
| J Thomas wrote:
> proofs that bumblebees can't fly. On the other hand if a design is
> constructed with traditional safety margins much reduced because
> theory says they're not needed, it's likely to get a lot of interest
> while the engineers wait for it to fall down.
That is not the reason why structures fall down. Initially new
structural designs are built with a large safety margin. Subsequently
this safety margin is not reduced dramatically because of theory, but
is rather gradually lowered little by little for practical reasons
(cost, aesthetics, etc.) as people gain confidence in the design.
Eventually the safety margin is gone and the structure falls down.
See Henry Petroski's "Design Paradigms" for a thorough explanation
of this phenomenon.
--
mail1dotstofanetdotdk
| |
| Joachim Durchholz 2007-02-25, 8:03 am |
| J Thomas schrieb:
> On Feb 23, 11:32 am, Joachim Durchholz <j...@durchholz.org> wrote:
>
> No, that's a red herring.
Isn't :-)
Seriously, you're right that NP-complete algorithms are occasionally
useful. Even undecidable algorithms are used (some varieties of
dependent type systems do that).
However, NP-complete and undecidable algorithms drastically reduce your
design space, so the first reaction of a programmer asked to do such a
thing will be a search for alternatives.
I.e. CS defines bounds. You can overstep them, but you pay steep price.
Regards,
Jo
| |
| Chris Smith 2007-02-25, 7:05 pm |
| <Paul Rubin <http://phr.cx@NOSPAM.invalid>> wrote:
> And then we have godawful
> software like Windows that crashes all the time; can we use (e.g.)
> constructive type theory to make programs that verifiably do what
> they're supposed to?
No. People claim that they do this, but all they really prove is that
one extrapolation of the requirement into a formal language (the
program) is equivalent to another (the input to the validator, which is
often confusingly called the "specification" or something like that, in
order to distract you from the fact that it can be every bit as likely
to contain bugs as the program). Sometimes, the fact that both
techniques, which are traditionally somewhat radically different from
each other, agree can be useful information. It probablistically
supports the proposition that the program is correct. Any claim beyond
this -- that such a method actually proves that the program contains no
bugs or does "what it's supposed to do", for example -- is misleading
and exaggerated.
At a lower level, there are many commonly used proof systems that prove
the absence of specific program behaviors. They are called type
systems, and a good number of programming languages have them built in.
--
Chris Smith
| |
| Chris Uppal 2007-02-25, 7:05 pm |
| Arthur J. O'Dwyer wrote:
[me:]
[color=darkred]
> I believe this thread is discussing languages which are high-level
> enough that "run it anyway" is a meaningless request. If the program
> is malformed, you can't "run it anyway"; there's no legal program
> present to run!
I don't think that's true at all.
Functional languages (real ones, I mean, not LISP) all have trivial
variations on lambda calculus as their runtime semantics (the
NON-trivial variation is in evaluation order, which is vitally
important, but irrelevant here). It is simple to create an "untyped"
implementation of that concept. For instance the earliest functional
programming langage implementation that I, personally, know of
(remember that I don't count LISP) was Turner's SASL -- an untyped,
lazy, pure functional programming language (for his PhD in 1979).
His SASL interpreter was done in C, which meant he had to implement GC,
etc (3.5 K lines of code in total). But these days nobody would follow
that path -- they'd probably write it /in/ Haskell, and the thing would
be trivial.
-- chris
| |
| Chris Smith 2007-02-25, 10:04 pm |
| Chris Uppal <chris.uppal@metagnostic.REMOVE-THIS.org> wrote:
> Functional languages (real ones, I mean, not LISP)
> For instance the earliest functional
> programming langage implementation that I, personally, know of
> (remember that I don't count LISP)
I'm curious why you don't count LISP as a functional language. I can't
stand LISP myself, but I don't see how you'd call it non-functional.
The mutation features are not much different from ML's mutation features
except that they aren't so clearly delineated so that mutation can
pollute programs. Other than that, the only significant difference I
see between LISP and the pure lambda calculus is that function
parameters are lists rather than being curried.
Is it one of those things, or something else?
--
Chris Smith
| |
| Ingo Menger 2007-02-26, 4:12 am |
| On Feb 24, 11:16 pm, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
>Coming
> from Python, I was used to significant indentation, but Haskell's
> indentation rules are more complex and seem to make less sense, and
> theyaren't described in the tutorial I looked at.
They *are* described, however, in the Haskell report. (in the
appendix)
| |
| Chris Uppal 2007-02-26, 8:06 am |
| Chris Smith wrote:
[me:]
....[color=darkred]
> I'm curious why you don't count LISP as a functional language. I
> can't stand LISP myself, but I don't see how you'd call it
> non-functional.
That Lisp has an important functional aspect is beyond dispute. But
for me (and, as far as I know, for most people outside the US[*]) Lisp
is not a member of that category of languages known as Functional
Programming Languages.
([*] At least that's how it was when I last used a functional
programming language in anger -- years ago.)
Why ? A matter of history, a matter of emphasis.
History: it never has been -- Lisp has always been in a category by
itself, functional, programming is a separate, albeit related,
category. <shrug/>
Emphasis: Lisp is to a large degree about lists. Remove lists from
Lisp and you are left with nothing. Functional Programming languages
are about higher order functions, remove lists from them and you are
left with an FP language with reduced expressiveness. Applicative
evaluation order. Currying. Pattern matching. They all add up to a
style and feel which is common to all functional languages, and which
is not shared by Lisp. (I know there are exceptions to all the above
-- ML has the "wrong" evaluation order, for instance -- it's a "family
resemblence" thing, not a list of formal criteria).
OTOH, Lisp has a feel and a collection of features of its own, which is
not shared by functional programming languages.
I see no benefit in conflating the two.
-- chris
| |
| Stefan Ram 2007-02-26, 8:06 am |
| "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org> writes:
>Remove lists from Lisp and you are left with nothing.
(Try to post this on comp.lang.lisp, and see what happens.)
~
A functional language /enables/ functional programming,
which means:
- functions are values and at the same time can be
applied (to an argument)
- it has function literals for a wide class of functions
- functions can be returned from functions
- evaluation of arguments can be suppressed somewhat,
so as to implement »if« or »cond« as a function
- it has a garbage collector
- it has a constructor for some kind of container
(like a list)
A /pure/ functional language /enforces/ functional programming.
- no inbuilt notion of state or statements or an
execution sequence in time, only a notation for
values being specified in terms of other values.
| |
| Rainer Joswig 2007-02-26, 8:06 am |
| In article <xn0f2x2j980wlzp000@news.gradwell.net>,
"Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org> wrote:
> Chris Smith wrote:
>
> [me:]
> ...
>
> That Lisp has an important functional aspect is beyond dispute. But
> for me (and, as far as I know, for most people outside the US[*]) Lisp
> is not a member of that category of languages known as Functional
> Programming Languages.
>
> ([*] At least that's how it was when I last used a functional
> programming language in anger -- years ago.)
>
> Why ? A matter of history, a matter of emphasis.
>
> History: it never has been -- Lisp has always been in a category by
> itself, functional, programming is a separate, albeit related,
> category. <shrug/>
>
> Emphasis: Lisp is to a large degree about lists.
I'd say you are stuck even before 1958.
Lisp is a family of programming languages.
LISP (all caps) is typically used to denote some ancient dialect of Lisp
btw.
In the family of Lisp typical dialects are Scheme and Common Lisp.
Both are not pure FPLs. Both support a functional programming
style. Scheme a bit more than Common Lisp. But Common Lisp also
carries the functional programming style over to object-oriented
programming (which is not provided in Scheme by default).
In Common Lisp, functions are objects, methods
are objects, there are meta-classes for those and so on.
A higher-order functional programming style is quite
common (!) in Common Lisp - even with CLOS. More so in Scheme.
True is that Scheme and Common Lisp are quite different from Haskell,
SML and other some other FPLs.
> Remove lists from
> Lisp and you are left with nothing. Functional Programming languages
> are about higher order functions,
I use higher-order functions in Lisp all day. Thank you. It is
hard to write any Lisp code ignoring higher-order functions.
> remove lists from them and you are
> left with an FP language with reduced expressiveness. Applicative
> evaluation order. Currying. Pattern matching.
Pattern matching has nothing to do with FP. (like it might be
that some cars have automatic transmission for convenience,
but a car is perfectly a car with manual transmission).
> They all add up to a
> style and feel which is common to all functional languages, and which
> is not shared by Lisp.
Programming in Haskell is quite different from programming in SML.
Laziness, Monads, Type Classes, Syntax (significant whitespace), etc.
Erlang is different again. J? Mercury? Oz? Clean?
> (I know there are exceptions to all the above
> -- ML has the "wrong" evaluation order, for instance -- it's a "family
> resemblence" thing, not a list of formal criteria).
>
> OTOH, Lisp has a feel and a collection of features of its own, which is
> not shared by functional programming languages.
>
> I see no benefit in conflating the two.
FP is so vague as OOP is nowadays. It is almost useless.
Inclusion or not inclusion is mostly political.
>
> -- chris
| |
| Rainer Joswig 2007-02-26, 7:08 pm |
| In article <Lisp-20070226142541@ram.dialup.fu-berlin.de>,
ram@zedat.fu-berlin.de (Stefan Ram) wrote:
> "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org> writes:
>
> (Try to post this on comp.lang.lisp, and see what happens.)
>
> ~
>
> A functional language /enables/ functional programming,
> which means:
>
> - functions are values and at the same time can be
> applied (to an argument)
>
> - it has function literals for a wide class of functions
>
> - functions can be returned from functions
>
> - evaluation of arguments can be suppressed somewhat,
> so as to implement »if« or »cond« as a function
>
> - it has a garbage collector
>
> - it has a constructor for some kind of container
> (like a list)
>
> A /pure/ functional language /enforces/ functional programming.
>
> - no inbuilt notion of state or statements or an
> execution sequence in time, only a notation for
> values being specified in terms of other values.
Which makes Haskell 'pure'. But not SML. Which I would say
is a much more fundamental difference than, say, having
pattern matching or not.
Probably I'm not telling anything new. ;-) But maybe for C.U..?
| |
| Matthias Blume 2007-02-26, 10:07 pm |
|
Rainer Joswig <joswig@lisp.de> writes:
> FP is so vague as OOP is nowadays. It is almost useless.
> Inclusion or not inclusion is mostly political.
A better term -- one I heard first from Andrew Appel (although I am
not sure where it originated) -- is "value-oriented programming",
which hits the nail on the head much better.
Whether a language is functional is (to me) a matter of degree:
Haskell is certainly functional (unless you program in the IO monad,
in which case it is still functional, but more so only in name, and
less so in spirit).
ML is a bit less functional yet, since you are forced to program in
the IO monad all the time. Still, most of its data structures are
pure, and there is a significant and useful subset of the language
where programmers, compilers, and program analysis tools can safely
rely on freedom from side effects.
Scheme is even less functional, although it is still quite close to
the ML. However, there are significantly fewer "pure" constructs.
Almost anything involving structured data has side effects. (CONS in
Scheme has a side effect, and even LAMBDA does, for crying out loud!)
Common Lisp and other Lisp 2s is still further removed, as they give
up on the notion of functions being "just ordinary data" by making a
distinction between the rules of evaluation in operator position and
other positions.
That's my take on it, anyway.
> Pattern matching has nothing to do with FP. (like it might be
> that some cars have automatic transmission for convenience,
> but a car is perfectly a car with manual transmission).
To me, as the elimination form for sums, pattern matching is an
important aspect of /typed/ functional programming.
Matthias
| |
| Rainer Joswig 2007-02-27, 4:16 am |
| In article <m2hct82rza.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:
> Rainer Joswig <joswig@lisp.de> writes:
>
>
> A better term -- one I heard first from Andrew Appel (although I am
> not sure where it originated) -- is "value-oriented programming",
> which hits the nail on the head much better.
A Lisp programmer knows the value of everything, but the cost of
nothing. -- Alan Perlis
> Whether a language is functional is (to me) a matter of degree:
> Haskell is certainly functional (unless you program in the IO monad,
> in which case it is still functional, but more so only in name, and
> less so in spirit).
The not-side-effect-free outside world makes a lot problems. ;-)
> ML is a bit less functional yet, since you are forced to program in
> the IO monad all the time. Still, most of its data structures are
> pure, and there is a significant and useful subset of the language
> where programmers, compilers, and program analysis tools can safely
> rely on freedom from side effects.
How practical is it in 'reality'?
Say, you don't (re)use hash-tables and arrays in 'typical' ML
programs?
> Scheme is even less functional, although it is still quite close to
> the ML. However, there are significantly fewer "pure" constructs.
> Almost anything involving structured data has side effects. (CONS in
> Scheme has a side effect, and even LAMBDA does, for crying out loud!)
What is the LAMBDA or CONS side effect?
> Common Lisp and other Lisp 2s is still further removed, as they give
> up on the notion of functions being "just ordinary data" by making a
> distinction between the rules of evaluation in operator position and
> other positions.
For my practical programming purposes, this is mostly a
complication, but not a limitation.
>
> That's my take on it, anyway.
>
>
> To me, as the elimination form for sums, pattern matching is an
> important aspect of /typed/ functional programming.
If you drive all time a car with automatic transmission, you
start to think that it is necessary to have it.
If you remove or add pattern matching, it does not make a
programming language more or less 'functional', IMHO.
>
> Matthias
| |
| Markus E Leypold 2007-02-27, 7:08 pm |
|
"Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org> writes:
> Arthur J. O'Dwyer wrote:
>
> [me:]
>
>
> I don't think that's true at all.
>
> Functional languages (real ones, I mean, not LISP) all have trivial
> variations on lambda calculus as their runtime semantics (the
> NON-trivial variation is in evaluation order, which is vitally
> important, but irrelevant here). It is simple to create an "untyped"
> implementation of that concept. For instance the earliest functional
> programming langage implementation that I, personally, know of
> (remember that I don't count LISP) was Turner's SASL -- an untyped,
> lazy, pure functional programming language (for his PhD in 1979).
>
> His SASL interpreter was done in C, which meant he had to implement GC,
> etc (3.5 K lines of code in total). But these days nobody would follow
> that path -- they'd probably write it /in/ Haskell, and the thing would
> be trivial.
>
> -- chris
And how does that relate to
"If the program is malformed, you can't "run it anyway"; there's no
legal program present to run!"
?
Regards -- Markus
| |
| Markus E Leypold 2007-02-27, 7:08 pm |
|
"J Thomas" <jethomas5@gmail.com> writes:
> On Feb 23, 12:13 pm, Markus E Leypold
> <development-2006-8ecbb5cc8aREMOVET...@ANDTHATm-e-leypold.de> wrote:
>
>
> Yes, but at this point I believe that NP-complete is a red herring.
> What the customer cares about is at what N the resources become an
> issue, and at what N the solution becomes impractical.
The OPs problem was "what the **** is all that theory good for". Well:
You won't be able to discuss "upgrade problems" or "scaling" or even
see that there is a problem (and will stay here) if you don't know
about NP-completeness etc.
>
> As I understand it, to prove a problem is NP-complete or prove it
> isn't, will not in either case answer those questions. To know that
> scaling issues will at some point make the solution completely
> impractical doesn't at all say whether it's impractical for the
> customer's uses. And vice versa, it can scale gently and be too
> unwieldy even at the scale the customer needs now.
>
> So it looks to me like finding out whether it's NP-complete is solving
> the wrong problem. What you need to know is something else. Some of
? Whoever said that?
> the details you use to decide NP-completely might be used for that
> other question, though.
>
> If you don't understand your materials you can expect problems. On the
Same applies to CS and algorithms and their complexity.
> other hand, civil engineering has traditionally operated with a very
> large component of precedent. If a theoretician decides that a
> particular procedure is unsafe, but it has been in widespread use
> without incident, he's likely to generate lots of comments about
> proofs that bumblebees can't fly. On the other hand if a design is
> constructed with traditional safety margins much reduced because
> theory says they're not needed, it's likely to get a lot of interest
> while the engineers wait for it to fall down.
> Theory is a useful supplement to practice. When you operate outside
Supplement? It's actually the _fundament_ of practice. If not, in
chemistry we'd still be searching how to make gold,
because "it might just work this time".
> your area of expertise it's all you have. And this is probably why
> people are generally so hesitant to do significant projects outside
> their areas of expertise.
Regards -- Markus
| |
| Markus E Leypold 2007-02-27, 7:08 pm |
|
"J Thomas" <jethomas5@gmail.com> writes:
> On Feb 24, 4:38 pm, Benjamin Franksen <benjamin.frank...@bessy.de>
> wrote:
>
>
>
> This is why I say it's important for Forth to become more intuitive
^^^^^
I completely agree with that. You have my support,
Regards -- Markus
| |
| Chris Smith 2007-02-27, 7:08 pm |
| > "Chris Uppal" <chris.uppal@metagnostic.REMOVE-THIS.org> writes:
Markus E Leypold wrote:[color=darkred]
> And how does that relate to
>
> "If the program is malformed, you can't "run it anyway"; there's no
> legal program present to run!"
>
> ?
Simple. The error messages from Hugs are almost certainly type errors.
In that case, they are complaining that something can go wrong, but the
program still has well-defined semantics. If one has trouble
identifying the meaning of the type error, one could just run the
program and try to watch something go wrong, and thereby identify the
meaning of the error.
That is assuming we're talking about type errors; but in practice, we
almost always are. Syntax errors are comparatively rare (except for
beginners when they have to do with Haskell's bizarre indentation rules)
and easy to fix. I think you can assume Chris's comment was intended
for type errors only.
--
Chris Smith
| |
| Jerry Avins 2007-02-27, 7:08 pm |
| Markus E Leypold wrote:
> "J Thomas" <jethomas5@gmail.com> writes:
...
>
> Supplement? It's actually the _fundament_ of practice. If not, in
> chemistry we'd still be searching how to make gold,
> because "it might just work this time".
Theory developed to explain practice. Practice came first. I recall a
well written eleventh-century treatise titled something like "How to
Build a Thirty-Foot Bridge with Twelve-Foot Timbers". (Wood was becoming
scarce in England around then.) No theory, but instructions I could
follow. The heuristics were confined to footings and piers.
Jerry
--
Engineering is the art of making what you want from things you can get.
¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯
¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯
¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯
¯¯¯¯¯¯¯¯¯¯¯
| |
| Markus E Leypold 2007-02-27, 7:08 pm |
|
Chris Smith <cdsmith@twu.net> writes:
>
> Markus E Leypold wrote:
>
> Simple. The error messages from Hugs are almost certainly type errors.
> In that case, they are complaining that something can go wrong, but the
> program still has well-defined semantics.
No, I don't think so. The set of all well typed language constructs is
contains the set of all programs with a well defined semantics. The
language definitions of Haskell and ML languages I know of are thus,
that there is no such thing as a "badly typed program". "Well typed"
is a requirement for "being a program". If it doesn't type, there is
only some text that could be parsed into tokens (in adheres to the
lexis of the language), could perhaps even be used to construct a
sysntax tree (it adheres to the syntax of the language) but since it
couldn't be typed it's not a program. The semantic is only defined on
(well typed) programs.
BTW it is exactly your kind of thinking -- that "well typed",
"compiled", "can be run", "has well defined semantics" are disjoint
concepts -- that make C such a mess (at least for people that haven't
yet developed reflexes to stay well clear of areas of doubtful
reputation).
> If one has trouble identifying the meaning of the type error, one
> could just run the program and try to watch something go wrong, and
> thereby identify the meaning of the error.
Hardly. Doesn't sound like a good idea. Constructing a test case to
find the "error" would be tantamount to understanding the cause for
the type error in the beginning. No need to run the non-program then.
> That is assuming we're talking about type errors; but in practice, we
> almost always are.
> Syntax errors are comparatively rare (except for
> beginners when they have to do with Haskell's bizarre indentation rules)
> and easy to fix. I think you can assume Chris's comment was intended
> for type errors only.
I know. I still think it a really bad idea. Esp. from a sociological
point of view: We know how warnings from the C-compiler are usually
treated by people who want to get their stuff done before the dead
line: --no-warn-all-errors (...).
Regards -- Markus
| |
| Chris Uppal 2007-02-27, 7:08 pm |
| Chris Smith wrote:
> That is assuming we're talking about type errors; but in practice, we
> almost always are. Syntax errors are c | | |