Sorry for spamming but now when I'm reading a lot about static typing
and the *benefits* I really found this comic amusing
http://blog.rvburke.com/2006/10/10/static-typing/
bobi
On 1 Dec, 09:29, Slobodan Blazeski <·················@gmail.com>
wrote:
> Sorry for spamming but now when I'm reading a lot about static typing
> and the *benefits* I really found this comic amusinghttp://blog.rvburke.com/2006/10/10/static-typing/
>
> bobi
That's very funny. I love Larson's cartoons.
The reason university teachers prefer to teach FP from statically
typed languages is that it forces students to think about the nature
of the data structures they're working with. So its a good discipline
for learners.
More experienced programmers often skip it if they find it gets in the
way.
But if you'e going to do anything safety critical, nuclear reactors,
space probes, sensitive DBs, I think you really do need to have it.
Mark
> But if you'e going to do anything safety critical, nuclear reactors,
> space probes, sensitive DBs, I think you really do need to have it.
>
> Mark
Why?
On 1 Dec, 12:40, ··················@gmail.com wrote:
> > But if you'e going to do anything safety critical, nuclear reactors,
> > space probes, sensitive DBs, I think you really do need to have it.
>
> > Mark
>
> Why?
Well, because the consequence of error is so serious - either because
of litigation, loss of life or money - that you have to do everything
you can to minimise the chances of it happening.
Static typing has a lot to contribute to that goal. To give an
example, suppose you're working on a project as part of a team and
you're given the task of implementing a stack to receive and store
messages from a source. Two offices down, another guy is working on
the same program. Both programs work fine until they're conjoined
and then pow it fails. It turns out that you used lists for your
stack and he's used closures.
In this situation what you need to do is to agree with the team in
advance, what data structures you're using (either abstract or
concretely). Also, to stop a lot of hand-waving and 'I thought you
meant ... You didn't? Darn!' exchanges you need to formally desribe
those structures. And if, in addition, you can use this formal
description in such a way as to get the computer to guarantee that
you've all used the same data structures, then you've eliminated a
source of error. And thats exactly what type checking does.
Mark
. .
On Dec 1, 3:20 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> On 1 Dec, 12:40, ··················@gmail.com wrote:
>
> > > But if you'e going to do anything safety critical, nuclear reactors,
> > > space probes, sensitive DBs, I think you really do need to have it.
>
> > > Mark
>
> > Why?
>
> Well, because the consequence of error is so serious - either because
> of litigation, loss of life or money - that you have to do everything
> you can to minimise the chances of it happening.
>
> Static typing has a lot to contribute to that goal. To give an
> example, suppose you're working on a project as part of a team and
> you're given the task of implementing a stack to receive and store
> messages from a source. Two offices down, another guy is working on
> the same program. Both programs work fine until they're conjoined
> and then pow it fails. It turns out that you used lists for your
> stack and he's used closures.
You're example is naive and doesn't hold any water. If they are
working on different modules of a SAME program they will build
incrementally with each one checking the day to day changes in the
repository.I really don't remember a company that doesn't use source
control in the last 6 years. And if the company as at least a little
good they will have automatic testing and a QA team. So there is no
way for me change my code drastically unless the changes are only of
internal nature. Static type could help very little, as it happened
to me to have perfectly valid types and WRONG behavior.
>
> In this situation what you need to do is to agree with the team in
> advance, what data structures you're using (either abstract or
> concretely). Also, to stop a lot of hand-waving and 'I thought you
> meant ... You didn't? Darn!' exchanges you need to formally desribe
> those structures. And if, in addition, you can use this formal
> description in such a way as to get the computer to guarantee that
> you've all used the same data structures, then you've eliminated a
> source of error. And thats exactly what type checking does.
>
> Mark
>
> . .
Mark Tarver wrote:
> On 1 Dec, 12:40, ··················@gmail.com wrote:
>
>>>But if you'e going to do anything safety critical, nuclear reactors,
>>>space probes, sensitive DBs, I think you really do need to have it.
>>
>>>Mark
>>
>>Why?
>
>
> Well, because the consequence of error is so serious - either because
> of litigation, loss of life or money - that you have to do everything
> you can to minimise the chances of it happening.
>
> Static typing has a lot to contribute to that goal.
PWUAAAAHHAHAHAHHAHA!!!!!!!! Over on c.l.javascript I just figured out
that the consensus hatred there of frameworks* has to do mostly with
failure of frameworks to pass JSLint and in general a C++/Java OCD
bias... static typing strikes back!
My tone over there has been more to ascertain that I have understood
them correctly in which case FOR THE LOVE OF GOD LET'S NOT REVISIT THIS!!!!!
:)
But as long as we are, I gotta tell you, if I ever have the misfortune
(?) to end up with the responsibility for some "must not fail" code I
suspect (and this is admitted guesswork) that the QA qould be as big a
project as the project itself, with all sorts of clever stuff done on
the QA side to head off all sorts of program failures and I think about
1% of the challenge will be finding places where "hi mom" was passed as
a float.
kenny
* I do not disagree except for qooxdoo, but for other reasons. k
On Dec 1, 9:20 am, Mark Tarver <··········@ukonline.co.uk> wrote:
> On 1 Dec, 12:40, ··················@gmail.com wrote:
>
> > > But if you'e going to do anything safety critical, nuclear reactors,
> > > space probes, sensitive DBs, I think you really do need to have it.
>
> > > Mark
>
> > Why?
>
> Well, because the consequence of error is so serious - either because
> of litigation, loss of life or money - that you have to do everything
> you can to minimise the chances of it happening.
>
> Static typing has a lot to contribute to that goal. To give an
> example, suppose you're working on a project as part of a team and
> you're given the task of implementing a stack to receive and store
> messages from a source. Two offices down, another guy is working on
> the same program. Both programs work fine until they're conjoined
> and then pow it fails. It turns out that you used lists for your
> stack and he's used closures.
>
> In this situation what you need to do is to agree with the team in
> advance, what data structures you're using (either abstract or
> concretely). Also, to stop a lot of hand-waving and 'I thought you
> meant ... You didn't? Darn!' exchanges you need to formally desribe
> those structures. And if, in addition, you can use this formal
> description in such a way as to get the computer to guarantee that
> you've all used the same data structures, then you've eliminated a
> source of error. And that's exactly what type checking does.
>
> Mark
>
> . .
It just strikes me as a strange idea, because I work on 'safety
critical' software in lisp.
Some of it is a judicious use of macros/function that automatically
convert 'incorrect' types.
(Get-foo-from-anything, which takes a string or object, or array
index, being a favorite example).
Is it an assumption that because a language is dynamically typed it
does not have the facilities to properly managed typed data?
And if you really harness the power of macro-writing-macros, you can
even further reduce the 'boilerplate' involved there.
··················@gmail.com wrote:
> It just strikes me as a strange idea, because I work on 'safety
> critical' software in lisp.
No wonder you're anonymous.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
On Dec 3, 11:44 am, Jon Harrop <····@ffconsultancy.com> wrote:
> ··················@gmail.com wrote:
> > It just strikes me as a strange idea, because I work on 'safety
> > critical' software in lisp.
>
> No wonder you're anonymous.
>
> --
> Dr Jon D Harrop, tool
Actually its so I can call you a tool.
On Mon, 01 Dec 2008 06:20:46 -0800, Mark Tarver wrote:
> On 1 Dec, 12:40, ··················@gmail.com wrote:
>> > But if you'e going to do anything safety critical, nuclear reactors,
>> > space probes, sensitive DBs, I think you really do need to have it.
>>
>> > Mark
>>
>> Why?
>
> Well, because the consequence of error is so serious - either because of
> litigation, loss of life or money - that you have to do everything you
> can to minimise the chances of it happening.
>
> Static typing has a lot to contribute to that goal. To give an example,
> suppose you're working on a project as part of a team and you're given
> the task of implementing a stack to receive and store messages from a
> source. Two offices down, another guy is working on the same program.
> Both programs work fine until they're conjoined and then pow it fails.
> It turns out that you used lists for your stack and he's used closures.
>
> In this situation what you need to do is to agree with the team in
> advance, what data structures you're using (either abstract or
> concretely). Also, to stop a lot of hand-waving and 'I thought you
> meant ... You didn't? Darn!' exchanges you need to formally desribe
> those structures. And if, in addition, you can use this formal
> description in such a way as to get the computer to guarantee that
> you've all used the same data structures, then you've eliminated a
> source of error. And thats exactly what type checking does.
You ignore the costs of static type checking. It is not cost that is
best measured in money, but in the time and attention of the programmer
that has to be diverted to writing boilerplate code. Since attention is
a finite resource, and is critical too in discovering deeper, conceptual
mistakes, I am not convinced that static typing leads to a net gain.
Static typing is often touted as a panacea, but its proponents forget
that there are relatively simple type statements that cannot be checked
in practice. For example, you can meaningfully talk about increasing
double -> double univariate functions, but no compiler I know of will be
able to check that for you.
If you have critical code, the only thing that helps is a lot of
imaginative testing and auditing. Also, a nice condition handling system
(Lisp! Lisp! :-)) used with paranoid fallbacks. Compared to that, the
importance of static typing is just noise.
Tamas
> You ignore the costs of static type checking. It is not cost that is
> best measured in money, but in the time and attention of the programmer
> that has to be diverted to writing boilerplate code.
Datatype definitions do use up a certain amount of space and this
space tends to be fairly constant and grows only slowly with an
increasingly bigger program. Hence if you see only small examples in
books, the datatype definitions seem to take up a large percentage of
the code. Actually for large programs the amount of this
'boilerplate' (is it boilerplate to formally define your data
structures?) is percentagewise quite small.
> Since attention is
> a finite resource, and is critical too in discovering deeper, conceptual
> mistakes, I am not convinced that static typing leads to a net gain.
>
> Static typing is often touted as a panacea, but its proponents forget
> that there are relatively simple type statements that cannot be checked
> in practice.
Actually I think that we've barely begun to tap the resources of type
theory. I think people are operating with the equation.
type theory = what ML and Haskell understand
Its a lot more interesting than that.
For example, you can meaningfully talk about increasing
> double -> double univariate functions, but no compiler I know of will be
> able to check that for you.
>
> If you have critical code, the only thing that helps is a lot of
> imaginative testing and auditing. Also, a nice condition handling system
> (Lisp! Lisp! :-)) used with paranoid fallbacks. Compared to that, the
> importance of static typing is just noise.
>
> Tamas- Hide quoted text -
>
> - Show quoted text -
Yes; great stuff. Testing, by all means do it. Type checking is to
software as wearing a seat belt is to driving. It does not absolve you
from the responsibility of being a safe driver.
Lisp? Its a great language, but I'm not convinced its the automatic
choice for safety critical work; vide my comments above.
Mark
On Mon, 01 Dec 2008 08:00:56 -0800, Mark Tarver wrote:
> bigger program. Hence if you see only small examples in books, the
> datatype definitions seem to take up a large percentage of the code.
> Actually for large programs the amount of this 'boilerplate' (is it
> boilerplate to formally define your data structures?) is percentagewise
> quite small.
For me, "boilerplate code" also means code that is meant to work around
the constraints of static typing.
> Actually I think that we've barely begun to tap the resources of type
> theory. I think people are operating with the equation.
>
> type theory = what ML and Haskell understand
>
> Its a lot more interesting than that.
Maybe. I think we disagree because when we are talking about static
typing, I am considering practical languages here and now, and you are
thinking about some glorious future development. I have to admit that I
don't have the expertise to speculate about what is going to happen in
this area, and I see where you are pushing the boundaries quite actively.
Qi (esp. QiII) seems like a very nice language, and I wish you success
with it. If you can eliminate the obnoxious aspects of static typing, it
may be very successful. But that has to happen before I find languages
with static typing attractive.
> Yes; great stuff. Testing, by all means do it. Type checking is to
> software as wearing a seat belt is to driving. It does not absolve you
> from the responsibility of being a safe driver.
I don't think this is a good metaphor. Safety belts are a very good
trade-off of minor inconvenience vs large safety benefits. In the kind
of programs I write, static typing is a huge PITA with insignificant
benefits, especially when compared to what is already caught by smart
Lisp compilers (which do a lot of type inference and other checks).
> Lisp? Its a great language, but I'm not convinced its the automatic
> choice for safety critical work; vide my comments above.
It would be my automatic choice for writing a DSL for safety-critical
work.
Tamas
Tamas K Papp wrote:
> On Mon, 01 Dec 2008 08:00:56 -0800, Mark Tarver wrote:
>> bigger program. Hence if you see only small examples in books, the
>> datatype definitions seem to take up a large percentage of the code.
>> Actually for large programs the amount of this 'boilerplate' (is it
>> boilerplate to formally define your data structures?) is percentagewise
>> quite small.
>
> For me, "boilerplate code" also means code that is meant to work around
> the constraints of static typing.
Can you give any actual examples?
>> Actually I think that we've barely begun to tap the resources of type
>> theory. I think people are operating with the equation.
>>
>> type theory = what ML and Haskell understand
>>
>> Its a lot more interesting than that.
>
> Maybe. I think we disagree because when we are talking about static
> typing, I am considering practical languages here and now, and you are
> thinking about some glorious future development.
ML is well over 30 years old.
> I have to admit that I don't have the expertise... [Lisp] would be my
> automatic choice for writing a DSL for safety-critical work.
Because you are unaware of the alternatives.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Tamas K Papp wrote:
> You ignore the costs of static type checking. It is not cost that is
> best measured in money, but in the time and attention of the programmer
> that has to be diverted to writing boilerplate code.
What boilerplate?
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
In article
<····································@j35g2000yqh.googlegroups.com>,
Mark Tarver <··········@ukonline.co.uk> wrote:
> On 1 Dec, 12:40, ··················@gmail.com wrote:
> > > But if you'e going to do anything safety critical, nuclear reactors,
> > > space probes, sensitive DBs, I think you really do need to have it.
> >
> > > Mark
> >
> > Why?
>
> Well, because the consequence of error is so serious - either because
> of litigation, loss of life or money - that you have to do everything
> you can to minimise the chances of it happening.
>
> Static typing has a lot to contribute to that goal. To give an
> example, suppose you're working on a project as part of a team and
> you're given the task of implementing a stack to receive and store
> messages from a source. Two offices down, another guy is working on
> the same program. Both programs
Both programs? The same program?
> work fine until they're conjoined
> and then pow it fails. It turns out that you used lists for your
> stack and he's used closures.
Not sure if you have ever worked in a team. The same happens
with teams using statically typed software. That's
why teams have integration machines that check out code from
the central code repository and run tests. It's called
'continuous integration'. Same problem. Two guys develop
something over the day using their own environment
and then they check there code in. Either the software
then will not build, it will not compile, it will not link,
it will not start, it will not run any tests, etc. Somewhere
it WILL crash. That's why teams have a rule that after a check in
of code in a repository, a build has to be tried and
the tests have to be run - before the guy goes home.
The typical response then is 'it runs on my machine'.
But the goal is that it runs on the build and test machines
and on the other developers machines too. It's all
the same whether you develop software in Java, C, Lisp
or anything else. The compiler finds something on the
build machine, what the developer's local compiler did not find.
Etc.... You will also find out that the only situation
where 'two guys are working on the same part of a module' makes sense is
when they do 'pair programming' and sit together.
Otherwise usually there is a contract between the provider
of the module and the user. What in CLOS for example
is called a 'protocol'.
>
> In this situation what you need to do is to agree with the team in
> advance, what data structures you're using (either abstract or
> concretely). Also, to stop a lot of hand-waving and 'I thought you
> meant ... You didn't? Darn!' exchanges you need to formally desribe
> those structures. And if, in addition, you can use this formal
> description in such a way as to get the computer to guarantee that
> you've all used the same data structures, then you've eliminated a
> source of error. And thats exactly what type checking does.
>
> Mark
>
> . .
--
http://lispm.dyndns.org/
On 1 Dec, 14:36, Rainer Joswig <······@lisp.de> wrote:
> In article
> <····································@j35g2000yqh.googlegroups.com>,
> Mark Tarver <··········@ukonline.co.uk> wrote:
>
>
>
>
>
> > On 1 Dec, 12:40, ··················@gmail.com wrote:
> > > > But if you'e going to do anything safety critical, nuclear reactors,
> > > > space probes, sensitive DBs, I think you really do need to have it.
>
> > > > Mark
>
> > > Why?
>
> > Well, because the consequence of error is so serious - either because
> > of litigation, loss of life or money - that you have to do everything
> > you can to minimise the chances of it happening.
>
> > Static typing has a lot to contribute to that goal. To give an
> > example, suppose you're working on a project as part of a team and
> > you're given the task of implementing a stack to receive and store
> > messages from a source. Two offices down, another guy is working on
> > the same program. Both programs
>
> Both programs? The same program?
>
> > work fine until they're conjoined
> > and then pow it fails. It turns out that you used lists for your
> > stack and he's used closures.
>
> Not sure if you have ever worked in a team. The same happens
> with teams using statically typed software. That's
> why teams have integration machines that check out code from
> the central code repository and run tests. It's called
> 'continuous integration'. Same problem. Two guys develop
> something over the day using their own environment
> and then they check there code in. Either the software
> then will not build, it will not compile, it will not link,
> it will not start, it will not run any tests, etc. Somewhere
> it WILL crash. That's why teams have a rule that after a check in
> of code in a repository, a build has to be tried and
> the tests have to be run - before the guy goes home.
> The typical response then is 'it runs on my machine'.
> But the goal is that it runs on the build and test machines
> and on the other developers machines too. It's all
> the same whether you develop software in Java, C, Lisp
> or anything else. The compiler finds something on the
> build machine, what the developer's local compiler did not find.
> Etc.... You will also find out that the only situation
> where 'two guys are working on the same part of a module' makes sense is
> when they do 'pair programming' and sit together.
> Otherwise usually there is a contract between the provider
> of the module and the user. What in CLOS for example
> is called a 'protocol'.
>
>
>
> > In this situation what you need to do is to agree with the team in
> > advance, what data structures you're using (either abstract or
> > concretely). Also, to stop a lot of hand-waving and 'I thought you
> > meant ... You didn't? Darn!' exchanges you need to formally desribe
> > those structures. And if, in addition, you can use this formal
> > description in such a way as to get the computer to guarantee that
> > you've all used the same data structures, then you've eliminated a
> > source of error. And thats exactly what type checking does.
>
> > Mark
>
> > . .
>
> --http://lispm.dyndns.org/- Hide quoted text -
>
> - Show quoted text -
Different programs. I was thinking of a situation where a number of
programmers are working on one large system which shares the same data
between them.
Of course testing is fine, it should be done and it is complementary
to formal verification. But testing can only show the program is
faulty, not that it is correct. Unless you have some formal proof
that your tests are somehow exhaustive, there will be a margin of
uncertainty. Static typing gives you the assurance that within a
certain class - errors will not occur.
My example was simplified for the purpose of a short post. The point
is that having a formal description of your system which is shared
between workers and computably enforcable by the machine, increases
the security of the project. Any project which aims to provide safety
critical software should provide this guarantee.
Mark
On Dec 1, 3:59 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> On 1 Dec, 14:36, Rainer Joswig <······@lisp.de> wrote:
>
>
>
> > In article
> > <····································@j35g2000yqh.googlegroups.com>,
> > Mark Tarver <··········@ukonline.co.uk> wrote:
>
> > > On 1 Dec, 12:40, ··················@gmail.com wrote:
> > > > > But if you'e going to do anything safety critical, nuclear reactors,
> > > > > space probes, sensitive DBs, I think you really do need to have it.
>
> > > > > Mark
>
> > > > Why?
>
> > > Well, because the consequence of error is so serious - either because
> > > of litigation, loss of life or money - that you have to do everything
> > > you can to minimise the chances of it happening.
>
> > > Static typing has a lot to contribute to that goal. To give an
> > > example, suppose you're working on a project as part of a team and
> > > you're given the task of implementing a stack to receive and store
> > > messages from a source. Two offices down, another guy is working on
> > > the same program. Both programs
>
> > Both programs? The same program?
>
> > > work fine until they're conjoined
> > > and then pow it fails. It turns out that you used lists for your
> > > stack and he's used closures.
>
> > Not sure if you have ever worked in a team. The same happens
> > with teams using statically typed software. That's
> > why teams have integration machines that check out code from
> > the central code repository and run tests. It's called
> > 'continuous integration'. Same problem. Two guys develop
> > something over the day using their own environment
> > and then they check there code in. Either the software
> > then will not build, it will not compile, it will not link,
> > it will not start, it will not run any tests, etc. Somewhere
> > it WILL crash. That's why teams have a rule that after a check in
> > of code in a repository, a build has to be tried and
> > the tests have to be run - before the guy goes home.
> > The typical response then is 'it runs on my machine'.
> > But the goal is that it runs on the build and test machines
> > and on the other developers machines too. It's all
> > the same whether you develop software in Java, C, Lisp
> > or anything else. The compiler finds something on the
> > build machine, what the developer's local compiler did not find.
> > Etc.... You will also find out that the only situation
> > where 'two guys are working on the same part of a module' makes sense is
> > when they do 'pair programming' and sit together.
> > Otherwise usually there is a contract between the provider
> > of the module and the user. What in CLOS for example
> > is called a 'protocol'.
>
> > > In this situation what you need to do is to agree with the team in
> > > advance, what data structures you're using (either abstract or
> > > concretely). Also, to stop a lot of hand-waving and 'I thought you
> > > meant ... You didn't? Darn!' exchanges you need to formally desribe
> > > those structures. And if, in addition, you can use this formal
> > > description in such a way as to get the computer to guarantee that
> > > you've all used the same data structures, then you've eliminated a
> > > source of error. And thats exactly what type checking does.
>
> > > Mark
>
> > > . .
>
> > --http://lispm.dyndns.org/-Hide quoted text -
>
> > - Show quoted text -
>
> Different programs. I was thinking of a situation where a number of
> programmers are working on one large system which shares the same data
> between them.
>
> Of course testing is fine, it should be done and it is complementary
> to formal verification. But testing can only show the program is
> faulty, not that it is correct. Unless you have some formal proof
> that your tests are somehow exhaustive, there will be a margin of
> uncertainty. Static typing gives you the assurance that within a
> certain class - errors will not occur.
It simply will not mean that the software is correct. It just means
that some class of errors might not occur (given the uncertainty
of a non-formally proofed complex type checker that will have bugs,
uncertain infrastructure, uncertain machinery, uncertain interfaces,
etc.).
Both c = a + b and c = a * b will type check just fine. Only one
of them is correct in my program. Which is it? Will the compiler
tell me?
>
> My example was simplified for the purpose of a short post. The point
> is that having a formal description of your system which is shared
> between workers and computably enforcable by the machine, increases
> the security of the project. Any project which aims to provide safety
> critical software should provide this guarantee.
>
> Mark
On 1 Dec, 15:35, ·······@corporate-world.lisp.de" <······@corporate-
world.lisp.de> wrote:
> On Dec 1, 3:59 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
>
>
>
>
>
> > On 1 Dec, 14:36, Rainer Joswig <······@lisp.de> wrote:
>
> > > In article
> > > <····································@j35g2000yqh.googlegroups.com>,
> > > Mark Tarver <··········@ukonline.co.uk> wrote:
>
> > > > On 1 Dec, 12:40, ··················@gmail.com wrote:
> > > > > > But if you'e going to do anything safety critical, nuclear reactors,
> > > > > > space probes, sensitive DBs, I think you really do need to have it.
>
> > > > > > Mark
>
> > > > > Why?
>
> > > > Well, because the consequence of error is so serious - either because
> > > > of litigation, loss of life or money - that you have to do everything
> > > > you can to minimise the chances of it happening.
>
> > > > Static typing has a lot to contribute to that goal. To give an
> > > > example, suppose you're working on a project as part of a team and
> > > > you're given the task of implementing a stack to receive and store
> > > > messages from a source. Two offices down, another guy is working on
> > > > the same program. Both programs
>
> > > Both programs? The same program?
>
> > > > work fine until they're conjoined
> > > > and then pow it fails. It turns out that you used lists for your
> > > > stack and he's used closures.
>
> > > Not sure if you have ever worked in a team. The same happens
> > > with teams using statically typed software. That's
> > > why teams have integration machines that check out code from
> > > the central code repository and run tests. It's called
> > > 'continuous integration'. Same problem. Two guys develop
> > > something over the day using their own environment
> > > and then they check there code in. Either the software
> > > then will not build, it will not compile, it will not link,
> > > it will not start, it will not run any tests, etc. Somewhere
> > > it WILL crash. That's why teams have a rule that after a check in
> > > of code in a repository, a build has to be tried and
> > > the tests have to be run - before the guy goes home.
> > > The typical response then is 'it runs on my machine'.
> > > But the goal is that it runs on the build and test machines
> > > and on the other developers machines too. It's all
> > > the same whether you develop software in Java, C, Lisp
> > > or anything else. The compiler finds something on the
> > > build machine, what the developer's local compiler did not find.
> > > Etc.... You will also find out that the only situation
> > > where 'two guys are working on the same part of a module' makes sense is
> > > when they do 'pair programming' and sit together.
> > > Otherwise usually there is a contract between the provider
> > > of the module and the user. What in CLOS for example
> > > is called a 'protocol'.
>
> > > > In this situation what you need to do is to agree with the team in
> > > > advance, what data structures you're using (either abstract or
> > > > concretely). Also, to stop a lot of hand-waving and 'I thought you
> > > > meant ... You didn't? Darn!' exchanges you need to formally desribe
> > > > those structures. And if, in addition, you can use this formal
> > > > description in such a way as to get the computer to guarantee that
> > > > you've all used the same data structures, then you've eliminated a
> > > > source of error. And thats exactly what type checking does.
>
> > > > Mark
>
> > > > . .
>
> > > --http://lispm.dyndns.org/-Hidequoted text -
>
> > > - Show quoted text -
>
> > Different programs. I was thinking of a situation where a number of
> > programmers are working on one large system which shares the same data
> > between them.
>
> > Of course testing is fine, it should be done and it is complementary
> > to formal verification. But testing can only show the program is
> > faulty, not that it is correct. Unless you have some formal proof
> > that your tests are somehow exhaustive, there will be a margin of
> > uncertainty. Static typing gives you the assurance that within a
> > certain class - errors will not occur.
>
> It simply will not mean that the software is correct. It just means
> that some class of errors might not occur (given the uncertainty
> of a non-formally proofed complex type checker that will have bugs,
> uncertain infrastructure, uncertain machinery, uncertain interfaces,
> etc.).
>
> Both c = a + b and c = a * b will type check just fine. Only one
> of them is correct in my program. Which is it? Will the compiler
> tell me?
>
>
>
>
>
> > My example was simplified for the purpose of a short post. The point
> > is that having a formal description of your system which is shared
> > between workers and computably enforcable by the machine, increases
> > the security of the project. Any project which aims to provide safety
> > critical software should provide this guarantee.
>
> > Mark- Hide quoted text -
>
> - Show quoted text -- Hide quoted text -
>
> - Show quoted text -
If you read my post carefully, you'll see that I didn't claim it would
prove the program correct and free from all errors. What I said was
Static typing gives you the assurance that within a certain class -
errors will not occur.
And that's true.
However by exploiting more and more powerful type systems, you can
widen this class of of errors.
Mark
On Dec 1, 4:39 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> On 1 Dec, 15:35, ·······@corporate-world.lisp.de" <······@corporate-
>
>
>
> world.lisp.de> wrote:
> > On Dec 1, 3:59 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
>
> > > On 1 Dec, 14:36, Rainer Joswig <······@lisp.de> wrote:
>
> > > > In article
> > > > <····································@j35g2000yqh.googlegroups.com>,
> > > > Mark Tarver <··········@ukonline.co.uk> wrote:
>
> > > > > On 1 Dec, 12:40, ··················@gmail.com wrote:
> > > > > > > But if you'e going to do anything safety critical, nuclear reactors,
> > > > > > > space probes, sensitive DBs, I think you really do need to have it.
>
> > > > > > > Mark
>
> > > > > > Why?
>
> > > > > Well, because the consequence of error is so serious - either because
> > > > > of litigation, loss of life or money - that you have to do everything
> > > > > you can to minimise the chances of it happening.
>
> > > > > Static typing has a lot to contribute to that goal. To give an
> > > > > example, suppose you're working on a project as part of a team and
> > > > > you're given the task of implementing a stack to receive and store
> > > > > messages from a source. Two offices down, another guy is working on
> > > > > the same program. Both programs
>
> > > > Both programs? The same program?
>
> > > > > work fine until they're conjoined
> > > > > and then pow it fails. It turns out that you used lists for your
> > > > > stack and he's used closures.
>
> > > > Not sure if you have ever worked in a team. The same happens
> > > > with teams using statically typed software. That's
> > > > why teams have integration machines that check out code from
> > > > the central code repository and run tests. It's called
> > > > 'continuous integration'. Same problem. Two guys develop
> > > > something over the day using their own environment
> > > > and then they check there code in. Either the software
> > > > then will not build, it will not compile, it will not link,
> > > > it will not start, it will not run any tests, etc. Somewhere
> > > > it WILL crash. That's why teams have a rule that after a check in
> > > > of code in a repository, a build has to be tried and
> > > > the tests have to be run - before the guy goes home.
> > > > The typical response then is 'it runs on my machine'.
> > > > But the goal is that it runs on the build and test machines
> > > > and on the other developers machines too. It's all
> > > > the same whether you develop software in Java, C, Lisp
> > > > or anything else. The compiler finds something on the
> > > > build machine, what the developer's local compiler did not find.
> > > > Etc.... You will also find out that the only situation
> > > > where 'two guys are working on the same part of a module' makes sense is
> > > > when they do 'pair programming' and sit together.
> > > > Otherwise usually there is a contract between the provider
> > > > of the module and the user. What in CLOS for example
> > > > is called a 'protocol'.
>
> > > > > In this situation what you need to do is to agree with the team in
> > > > > advance, what data structures you're using (either abstract or
> > > > > concretely). Also, to stop a lot of hand-waving and 'I thought you
> > > > > meant ... You didn't? Darn!' exchanges you need to formally desribe
> > > > > those structures. And if, in addition, you can use this formal
> > > > > description in such a way as to get the computer to guarantee that
> > > > > you've all used the same data structures, then you've eliminated a
> > > > > source of error. And thats exactly what type checking does.
>
> > > > > Mark
>
> > > > > . .
>
> > > > --http://lispm.dyndns.org/-Hidequotedtext -
>
> > > > - Show quoted text -
>
> > > Different programs. I was thinking of a situation where a number of
> > > programmers are working on one large system which shares the same data
> > > between them.
>
> > > Of course testing is fine, it should be done and it is complementary
> > > to formal verification. But testing can only show the program is
> > > faulty, not that it is correct. Unless you have some formal proof
> > > that your tests are somehow exhaustive, there will be a margin of
> > > uncertainty. Static typing gives you the assurance that within a
> > > certain class - errors will not occur.
>
> > It simply will not mean that the software is correct. It just means
> > that some class of errors might not occur (given the uncertainty
> > of a non-formally proofed complex type checker that will have bugs,
> > uncertain infrastructure, uncertain machinery, uncertain interfaces,
> > etc.).
>
> > Both c = a + b and c = a * b will type check just fine. Only one
> > of them is correct in my program. Which is it? Will the compiler
> > tell me?
>
> > > My example was simplified for the purpose of a short post. The point
> > > is that having a formal description of your system which is shared
> > > between workers and computably enforcable by the machine, increases
> > > the security of the project. Any project which aims to provide safety
> > > critical software should provide this guarantee.
>
> > > Mark- Hide quoted text -
>
> > - Show quoted text -- Hide quoted text -
>
> > - Show quoted text -
>
> If you read my post carefully, you'll see that I didn't claim it would
> prove the program correct and free from all errors.
No but you claimed that mission critical systems, must be statically
typed. Something that I disagree.
> What I said was
>
> Static typing gives you the assurance that within a certain class -
> errors will not occur.
>
> And that's true.
>
> However by exploiting more and more powerful type systems, you can
> widen this class of of errors.
>
> Mark
> Both c = a + b and c = a * b will type check just fine. Only one
> of them is correct in my program. Which is it? Will the compiler
> tell me?
Actually yes - if you write in Qi. Th type theory is much more
powerful than ML etc.
C:\Documents and Settings\User\Desktop\Qi II\Lisp>clisp.exe -M Qi.mem -
q
Qi II 2008, Copyright (C) 2001-2008 Mark Tarver
www.lambdassociates.org
version 1.0
(0-) (datatype measures
\A basic conversion type \
I : inches;
________________
(* 2.54 I) : centimeters;
___________________
(input-inches) : inches;)
measures
(1-) (define input-inches
\Ask for some inches and input a number\
-> (do (output "Input inches: ") (input+ : number)))
input-inches
(2-) (tc +)
true
(3+) (define convert-to-centimeters
{A --> centimeters}
_ -> (+ 2.54 (input-inches)))
error: type error in rule 1 of convert-to-centimeters
\oops used + for *\
(4+) (define convert-to-centimeters
{A --> centimeters}
_ -> (* 2.54 (input-inches)))
convert-to-centimeters : (A --> centimeters)
That's better.
Mark
Mark Tarver wrote:
>> Both c = a + b and c = a * b will type check just fine. Only one
>> of them is correct in my program. Which is it? Will the compiler
>> tell me?
>
> Actually yes - if you write in Qi. Th type theory is much more
> powerful than ML.
OCaml provides polymorphic variants. Qi does not.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Mark Tarver wrote:
> On 1 Dec, 12:40, ··················@gmail.com wrote:
>>> But if you'e going to do anything safety critical, nuclear reactors,
>>> space probes, sensitive DBs, I think you really do need to have it.
>>> Mark
>> Why?
>
> Well, because the consequence of error is so serious - either because
> of litigation, loss of life or money - that you have to do everything
> you can to minimise the chances of it happening.
I wouldn't trust any program that hasn't been tested thoroughly. That's
the only way to ensure that a program works under the tested conditions.
Anything else is based only on assumptions.
> Static typing has a lot to contribute to that goal.
Static typing by itself doesn't contribute to that goal. It has to be
used correctly. Like any technology. The critical factor are responsible
programmers and decision makers.
See also http://p-cos.net/documents/dynatype.pdf
And also http://doi.acm.org/10.1145/379486.379512
Pascal
--
My website: http://p-cos.net
Common Lisp Document Repository: http://cdr.eurolisp.org
Closer to MOP & ContextL: http://common-lisp.net/project/closer/
Pascal Costanza wrote:
> Mark Tarver wrote:
>> On 1 Dec, 12:40, ··················@gmail.com wrote:
>>>> But if you'e going to do anything safety critical, nuclear reactors,
>>>> space probes, sensitive DBs, I think you really do need to have it.
>>>> Mark
>>> Why?
>>
>> Well, because the consequence of error is so serious - either because
>> of litigation, loss of life or money - that you have to do everything
>> you can to minimise the chances of it happening.
>
> I wouldn't trust any program that hasn't been tested thoroughly. That's
> the only way to ensure that a program works under the tested conditions.
> Anything else is based only on assumptions.
>
>> Static typing has a lot to contribute to that goal.
>
> Static typing by itself doesn't contribute to that goal. It has to be
> used correctly. Like any technology. The critical factor are responsible
> programmers and decision makers.
>
> See also http://p-cos.net/documents/dynatype.pdf
>
> And also http://doi.acm.org/10.1145/379486.379512
BTW, apart from Clojure, I think QI is one of the coolest new
developments in the Lisp world. Congrats for that!
Pascal
--
My website: http://p-cos.net
Common Lisp Document Repository: http://cdr.eurolisp.org
Closer to MOP & ContextL: http://common-lisp.net/project/closer/
On Mon, 1 Dec 2008, Pascal Costanza wrote:
>
> BTW, apart from Clojure, I think QI is one of the coolest new developments in
> the Lisp world. Congrats for that!
>
I second that. I'm almost drooling while reading
it's documentation and just wish I had time to implement
a larger program in it.
On Mon, 01 Dec 2008 15:44:02 +0100, Pascal Costanza wrote:
> Static typing by itself doesn't contribute to that goal. It has to be
> used correctly. Like any technology. The critical factor are responsible
> programmers and decision makers.
>
> See also http://p-cos.net/documents/dynatype.pdf
>
> And also http://doi.acm.org/10.1145/379486.379512
>
Is there a more accessible version of the second article?
Matt
--
The human race is a race of cowards; and I am not only marching in that
procession but carrying a banner.
-- Mark Twain
Pascal Costanza wrote:
> See also http://p-cos.net/documents/dynatype.pdf
Just another Lisper who thinks that Java is the be-all and end-all of static
typing...
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
On 2008-12-01, Mark Tarver <··········@ukonline.co.uk> wrote:
> On 1 Dec, 12:40, ··················@gmail.com wrote:
>> > But if you'e going to do anything safety critical, nuclear reactors,
>> > space probes, sensitive DBs, I think you really do need to have it.
>>
>> > Mark
>>
>> Why?
>
> Well, because the consequence of error is so serious - either because
> of litigation, loss of life or money - that you have to do everything
> you can to minimise the chances of it happening.
The consequence of /all/ errors is serious. Type mismatch errors are the easy
ones.
The situation of a program failing due to a type mismatch is no worse than that
of failing due an array access out of bounds or division by zero.
Static typing gives us a false sense of security that we have conquered some
important class of bugs.
The true value has to be rationally judged by the total effect of static typing
upon software design, implementation, delivery and maintenance.
> Static typing has a lot to contribute to that goal.
You should know better than to promote this lie.
Static typing is an optimization technique. It eliminates the overhead of
run-time checks.
Without a question, static typing is certainly safer than no typing. For
instance, the ANSI C language is a lot safer than B. But that's not because B
is dynamically typed whereas C is static, but because B is statically typed,
just like C, only with no checking.
Static typing is unsafe compared to dynamic typing, as soon as anything has to
be done which steps outside of the assumptions verified by the compiler.
When programmers run into the limitations of static typing, and implement
unsafe forms of dynamic typing. They may request a type conversion which they
simply ``know'' to be correct, but for which neither static nor dynamic
checking is provided. More sophisticated versions of this might use a more
disciplined approach like discriminated unions. This is a Greenspunning of
dynamic types.
Another example is that dynamic typing takes place at the component level
in the form of dynamic linking and loading.
Version 1.0 of some shared library contains uses of a structure foo. Version
2.0 of the same library is compiled with a new version of the same structure
foo, which is larger due to more data members. But there are programs that were
compiled to use the 1.0 library, which pass the smaller, original structure
into it.
Since all the static type info was thrown away when these components were
built, there is a random failure. Mechanisms outside of the language are
brought in to try to make this more safe. E.g. some kind of ``type safe
linkage'' (C++) or ``symbol versionining'' (ELF shared libs, or the Linux
kernel versioned symbols).
A lot of these mechanisms are no good. Like static typing, they just reject the
dynamic linking when it can't be proven sane. ``Sorry, component X cannot load
component Y. They disagree about the version of structure foo.''
Problem is, at this level, you might have only binaries. You can't just fix
something and recompile.
In the dynamic world, programs can not only load a new version of some binary
component, but do so in the running software, while keeping instances of the
old structure foo.
> To give an
> example, suppose you're working on a project as part of a team and
> you're given the task of implementing a stack to receive and store
> messages from a source. Two offices down, another guy is working on
> the same program. Both programs work fine until they're conjoined
> and then pow it fails. It turns out that you used lists for your
> stack and he's used closures.
What about the developer time wasted assigning the same task to two developers?
How would static typing prevent two developers who are not communicating with
each other from both extending the same program with a similar feature in
different ways?
And don't you think this would usually be caught in version control?
If you and I both stick some new stack feature into the same program, and check
in these changes, unless we wrote character-for-character identical code, one
of us will get a merge conflict.
> In this situation what you need to do is to agree with the team in
> advance, what data structures you're using (either abstract or
> concretely). Also, to stop a lot of hand-waving and 'I thought you
> meant ... You didn't? Darn!' exchanges you need to formally desribe
> those structures.
You mean like putting a DEFSTRUCT or DEFCLASS into a file that everyone uses?
No wait, that can't work, it's not statically typed!
> And if, in addition, you can use this formal
> description in such a way as to get the computer to guarantee that
> you've all used the same data structures, then you've eliminated a
> source of error. And thats exactly what type checking does.
So are you arguing type checking versus no type checking, or static versus
dynamic typing, or what?
Isn't this type checking? If not, what is it?
[1]> (car 3)
*** - CAR: 3 is not a list
And look, it was done before I compiled anything, so it's static, too!
:)
> > > But if you'e going to do anything safety critical, nuclear reactors,
> > > space probes, sensitive DBs, I think you really do need to have it.
> > Why?
> From: Mark Tarver <··········@ukonline.co.uk>
> Well, because the consequence of error is so serious - either because
> of litigation, loss of life or money - that you have to do everything
> you can to minimise the chances of it happening.
So in your opinion, forcing programmers to spend most of their time
formally declaring types of *all* places where data might be
stored, both local variables and slots in structures/objects,
writing twenty different kinds of CONS cells just because they
happen to need to form twenty kinds of linked-lists each of which
can store only one type of data in CAR places, and writing twenty
different versions of each function where Lisp has a single
function such as append or position or find, or messing with C++
style "templates" for automatically generating twenty different
versions of CONS cells and twenty different versions of each
function that can be applied to the twenty different kinds of
linked lists, leaving the programmer very little time to think
about the logic of the program, is going to somehow minimize the
chance of loss of money or life??
(In case you didn't get it, the question is rhetorical, because I'm
in favor of implicit types on objects, as in Lisp, not declared
types in places, as in C or Java. But feel free to post rebuttal.)
> Static typing has a lot to contribute to that goal. To give an
> example, suppose you're working on a project as part of a team and
> you're given the task of implementing a stack to receive and store
> messages from a source. Two offices down, another guy is working on
> the same program. Both programs work fine until they're conjoined
> and then pow it fails. It turns out that you used lists for your
> stack and he's used closures.
And who exactly is the incompetant manager who failed to define the
API for the stack module? If the API is specified, and each
programmer heeds it when writing his version of the stack module,
it should work fine regardless of how it's implemented. In fact you
should be able to swap modules and conduct comparative timing tests
to see which version is faster in practice, and you should be able
to run test suites with each module and compare output to be sure
they are the same.
new Stack() -> stackObject
stackObject.push(item) -> booleanSuccess
stackObject.pop() -> item | NULL
stackObject.peek() -> item | NULL
If there are no declarations, the stackObject can be stored in
*any* place without trouble, and later recovered from that place to
pass to any of the three methods. Nobody has to write a different
stack for each kind of data it might handle. Write stack once and
for all (or different versions of equivalent stack libraries with
different innerds but directly interchangeable).
new Source(parametersWhatever) -> sourceObject
sourceObject.tryRead() -> item | NULL
sourceObject.status() -> const.itemAvail const.openNoItem const.closedOtherEnd
sourceObject.close() -> booleanSuccess ;If you can't wait for GC to close it
I used pseudo-Java syntax there, the difference being the
semantics, that in Java every thing must be type-declared, although
you can "cheat" by declaring everything to be of type Object and
the use instanceOf to perform runtime checks to defeat the whole
idea of compile-time declarations. IMO it's better not to require
declarations in the first place, so you don't need to spend energy
defeating the compile-time type system.
static tryGetAndPush(sourceObject, stackObject) -> returnCode
defined as:
(let ((item sourceObject.tryRead() ))
(if (nullp item) (values null :READFAIL)))
(let ((pushRes stackObject.push(item) ))
(if pushRes :SUCCESS :PUSHFAIL)))))
Permission slip: In pseudo-code it's allowed to CommonLisp and Java syntax.
In no-declaration code, the key is to write test cases for every
possible program branch, and run those test cases. One idea for
enforcing this rule is to put a warning message (to trace output)
along every branch. Then when you get a successful running of the
test suite, you look at the trace log and deactivate each of the
warning messages that appeared in the trace log. This can be
automated. Then see if the source contains any trace output that is
still activated, indicating a branch that was never tested. That
too can be automated. For each branch not yet exercised, write a
new test to exercise it. If every module has ASSERT-type code upon
entry to make sure it's given appropriate parameters, that should
sufficiently insulate each module from each module, and then
testing all branches should be sufficient to get rid of data-type
bugs.
> In this situation what you need to do is to agree with the team in
> advance, what data structures you're using (either abstract or
> concretely). Also, to stop a lot of hand-waving and 'I thought you
> meant ... You didn't? Darn!' exchanges you need to formally desribe
> those structures. And if, in addition, you can use this formal
> description in such a way as to get the computer to guarantee that
> you've all used the same data structures, then you've eliminated a
> source of error. And thats exactly what type checking does.
It isn't so much the type checking per se that consumes the
programmer's time, it's the type declarations, and the perverse way
that only implementational types, not intentional types, are
available as declaration types in typical languages. What you
really want is a bunch of asserts or case breakdown upon entry to
each module that protects from bad-type data coming in, such as:
(defun foo (a1 a2 &key (k1 k1DefaultWhatever))
(prog (casea1 casea2 casek1)
(cond ((typep a1 implementationalTypeMatchesIntentionalType1)
(setq casea1 :T1))
((typep a1 implementationalTypeMatchesIntentionalType2)
(setq casea1 :T2))
((intentionalType3p a1)
(setq casea1 :T3))
(otherwise (error "Bug: a1 not any valid type")))
(cond ((typep a2 implementationalTypeMatchesIntentionalType1)
(setq casea2 :T1))
((typep a2 implementationalTypeMatchesIntentionalType2)
(setq casea2 :T2))
((intentionalType3p a2)
(setq casea2 :T3))
(otherwise (error "Bug: a2 not any valid type")))
(cond ((typep k1 implementationalTypeMatchesIntentionalType1)
(setq casek1 :T1))
((typep k1 implementationalTypeMatchesIntentionalType2)
(setq casek1 :T2))
((intentionalType3p k1)
(setq casek1 :T3))
(otherwise (error "Bug: k1 not any valid type")))
...actualBusinessCode...
))
Given that this is Lisp, where code is data, a tool can make sure
every function specified as an API-advertised has boilerplate code
like that, and can collect the specifics. Programmers of course
copy this boilerplate from a template, or use a macro that builds
it automatically. The tool also looks at whereever this function is
called from elsewhere, and makes sure the dataflow going into that
point is consistent with the types (both implementational and
intentional) declared as allowable for that function call.
So what happens if somebody invents a new datatype that some
API-advertised function ought to be able to handle? If the caller
starts passing that parameter before the called function is updated
to accept it, a test run bombs out with that ERROR something is not
of valid type, or the **tool** detects the problem, depending on
whether a test run or use of the tool is done first. If the
function being called is updated first, the test-suite tool notes a
branch that is never exercised, and the supervisor asks the person
who is supposed to write that function-calling code to please get
to work on it because the function to be called is already sitting
there waiting to exercise that new case.
If all return values from functions are wrapped with (the <type>
value), then automated inspection of the code by the **tool** can
likewise capture all possible data types that might be returned by
each API function, and make sure all such possibilities are handled
by the function that called it. But there's a minor problem with
this idea, and I have an idea for a fix but it's past my bedtime
and I'm getting groggy, so I won't brainstorm any further on it
tonight.
The nice thing about runtime checks is that you can run test cases
already, without needing to *first* get the entire system with
declared types to *compile*. The various consistency tools will
warn you that there's a problem needing to be fixed, but it won't
stop your system from being built and tested for the cases not
bothered by those remaining inconsistencies. Thus testing the cases
that are already coded and might actually be correct, and writing
new code for cases not yet finished, can proceed in parallel.
·············@teh.intarweb.org (Robert Maas, http://tinyurl.com/uh3t) wrote:
> So in your opinion, forcing programmers to spend most of their time
> formally declaring types of *all* places where data might be stored,
> both local variables and slots in structures/objects, writing twenty
> different kinds of CONS cells just because they happen to need to form
> twenty kinds of linked-lists each of which can store only one type of
> data in CAR places, and writing twenty different versions of each
> function where Lisp has a single function such as append or position
> or find, or messing with C++ style "templates" for automatically
> generating twenty different versions of CONS cells and twenty
> different versions of each function that can be applied to the twenty
> different kinds of linked lists, leaving the programmer very little
> time to think about the logic of the program, is going to somehow
> minimize the chance of loss of money or life??
That's not fair. A decent statically typed language (e.g. Haskell)
will compensate the lack of flexibility in typing with polymorphism:
first :: [a] -> a -- a is a type variable. Means "for all type a".
first (x:xs) = x
I think this debate is sterile anyway. There are times when you'd like
to be statically typed (maybe never for you, but sometimes or always for
other people, and it is their right), and there are times when it gets
in the way. The only thing that really matters is freedom of expression,
or PPP[1]:
- you want to be statically typed in Haskell, you win. You want dynamic
typing, you loose.
- you want dynamic typing in Lisp, you win. You want static typing, you
don't loose (use Qi or write it yourself).
That's why dynamic languages (in fact, just Lisp) is the way to go. It
prefer a language which gives me the ability to create my own safeguards
(possibly none) rather than a language that imposes a set of safeguards
on me.
Footnotes:
[1] the Permissive Programming Paradigm; I'm quite proud of that
acronym ;-)
--
Resistance is futile. You will be jazzimilated.
Scientific site: http://www.lrde.epita.fr/~didier
Music (Jazz) site: http://www.didierverna.com
EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bic�tre, France
Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22
Didier Verna wrote:
> ·············@teh.intarweb.org (Robert Maas, http://tinyurl.com/uh3t) wrote:
>
>
>>So in your opinion, forcing programmers to spend most of their time
>>formally declaring types of *all* places where data might be stored,
>>both local variables and slots in structures/objects, writing twenty
>>different kinds of CONS cells just because they happen to need to form
>>twenty kinds of linked-lists each of which can store only one type of
>>data in CAR places, and writing twenty different versions of each
>>function where Lisp has a single function such as append or position
>>or find, or messing with C++ style "templates" for automatically
>>generating twenty different versions of CONS cells and twenty
>>different versions of each function that can be applied to the twenty
>>different kinds of linked lists, leaving the programmer very little
>>time to think about the logic of the program, is going to somehow
>>minimize the chance of loss of money or life??
>
>
> That's not fair. A decent statically typed language (e.g. Haskell)
> will compensate the lack of flexibility in typing with polymorphism:
>
> first :: [a] -> a -- a is a type variable. Means "for all type a".
> first (x:xs) = x
>
>
> I think this debate is sterile anyway.
I thought I heard these type inferencing jobbies still leave the
developer trying to convince the compiler they know what they are up to?
In which case I think a good debate can still be had on productivity.
Not on personal preference but that does not matter because anyone who
turns out to prefer the less productive approach will be taken out and
shot anyway.
> There are times when you'd like
> to be statically typed (maybe never for you, but sometimes or always for
> other people, and it is their right),
Ah, I was wondering when the Magna Carta would work its way into debate
on technology. Reminds me of the obese diabetes sufferer in a
weight-loss clinic proclaiming, "No one is going to tell me I can't have
a chocolate cake!". Well, no ma'am, the Bill of Rights indeed is not at
issue here.
> in the way. The only thing that really matters is freedom of expression,
> or PPP[1]:
> [1] the Permissive Programming Paradigm; I'm quite proud of that
> acronym ;-)
>
Yaayyyyyyyyy! We're back to the moral relativism of the "feel good"
Sixties! Please tell me hemlines are going up, too!
<sigh>
kzo
On 2008-12-09, Didier Verna <······@lrde.epita.fr> wrote:
> ·············@teh.intarweb.org (Robert Maas, http://tinyurl.com/uh3t) wrote:
>
>> So in your opinion, forcing programmers to spend most of their time
>> formally declaring types of *all* places where data might be stored,
>> both local variables and slots in structures/objects, writing twenty
>> different kinds of CONS cells just because they happen to need to form
>> twenty kinds of linked-lists each of which can store only one type of
>> data in CAR places, and writing twenty different versions of each
>> function where Lisp has a single function such as append or position
>> or find, or messing with C++ style "templates" for automatically
>> generating twenty different versions of CONS cells and twenty
>> different versions of each function that can be applied to the twenty
>> different kinds of linked lists, leaving the programmer very little
>> time to think about the logic of the program, is going to somehow
>> minimize the chance of loss of money or life??
>
> That's not fair. A decent statically typed language (e.g. Haskell)
> will compensate the lack of flexibility in typing with polymorphism:
>
> first :: [a] -> a -- a is a type variable. Means "for all type a".
> first (x:xs) = x
Now you have a function "first" which represents the set of all functions
"first" of every type for extracting an item from a list of every type.
But that list can still only hold items of one kind, and its type
must be statically apparent at the point where first is applied to it.
This is very basic, like being able to do the following in C:
int x = 1; double y = 3.0;
double z = x + y; /* polymorphic plus */
Precursors to the C language had non-polymorphic #+ for floating addition.
Kaz Kylheku wrote:
> But that list can still only hold items of one kind,
Which may be a type representing any value (e.g. in F#).
> and its type must be statically apparent at the point where first is
> applied to it.
That is incorrect. The "first" function can be called from other polymorphic
functions.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Kaz Kylheku <········@gmail.com> writes:
> Now you have a function "first" which represents the set of all functions
> "first" of every type for extracting an item from a list of every type.
>
> But that list can still only hold items of one kind, and its type
> must be statically apparent at the point where first is applied to it.
Right, as in
first (x:xs) = x
doubleTaking a f = f a : [f a]
doubleFirst a = doubleTaking a first
Don't you think it would be a good idea to acquaint yourself with
modern statically typed languages before putting forth silly claims
about the shortcomings of static typing? Such silly arguments do
nothing to increase the appeal of any variant of Lisp, and only serve
to enable people such as Harrop to go on about complaining about the
silliness of Lisp advocates.
--
Aatu Koskensilta (················@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
On 2008-12-09, Aatu Koskensilta <················@uta.fi> wrote:
> Kaz Kylheku <········@gmail.com> writes:
>
>> Now you have a function "first" which represents the set of all functions
>> "first" of every type for extracting an item from a list of every type.
>>
>> But that list can still only hold items of one kind, and its type
>> must be statically apparent at the point where first is applied to it.
>
> Right, as in
>
> first (x:xs) = x
>
> doubleTaking a f = f a : [f a]
>
> doubleFirst a = doubleTaking a first
Yes, you can make another polymorphic function out of first.
All these calls will take on some concrete static type when
the dust settles.
At the time f is called, it, the list, the element,
everything has a statically determined type.
> Don't you think it would be a good idea to acquaint yourself with
> modern statically typed languages before putting forth silly claims
> about the shortcomings of static typing?
You can do the the above in C++. Is that modern?
Is it important to be modern? *shrug*
Kaz Kylheku wrote:
> On 2008-12-09, Aatu Koskensilta <················@uta.fi> wrote:
>> Kaz Kylheku <········@gmail.com> writes:
>>
>>> Now you have a function "first" which represents the set of all
>>> functions "first" of every type for extracting an item from a list of
>>> every type.
>>>
>>> But that list can still only hold items of one kind, and its type
>>> must be statically apparent at the point where first is applied to it.
>>
>> Right, as in
>>
>> first (x:xs) = x
>>
>> doubleTaking a f = f a : [f a]
>>
>> doubleFirst a = doubleTaking a first
>
> Yes, you can make another polymorphic function out of first.
>
> All these calls will take on some concrete static type when
> the dust settles.
>
> At the time f is called, it, the list, the element,
> everything has a statically determined type.
No, that is incorrect. Compilers for these languages typically either
generate code than handled polymorphism at run-time (OCaml, Haskell) or use
a JIT compiler to do run-time specialization of generics (F#). So the
concrete type is not known statically, i.e. when the source code is
compiled.
>> Don't you think it would be a good idea to acquaint yourself with
>> modern statically typed languages before putting forth silly claims
>> about the shortcomings of static typing?
>
> You can do the the above in C++. Is that modern?
> Is it important to be modern? *shrug*
Yes. This changed since C++.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Didier Verna wrote:
> - you want dynamic typing in Lisp, you win. You want static typing, you
> don't loose (use Qi or write it yourself).
Yeah, you just Greenspun the entire static type system yourself from the
ground up in Lisp, just like you would in assembler. Except you still don't
get the benefits of a modern language: users, mature libraries, type system
features, interop, concurrent run-time, viable commercial market...
Without users having tested your type system you have no faith that your
design or implementation are correct. So it gives you no faith in the
correctness of any software that uses it. A theorem prover like Coq would
help, maybe you would like to Greenspun that too?
You might as well build an ark out of match sticks in the middle of a bog
for all that idea will get you.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Jon Harrop <···@ffconsultancy.com> wrote:
> Didier Verna wrote:
>> - you want dynamic typing in Lisp, you win. You want static typing, you
>> don't loose (use Qi or write it yourself).
>
> Yeah, you just Greenspun the entire static type system yourself from
> the ground up in Lisp
Tell me something. At the time Haskell was born, didn't somebody, sort
of, you know, write it ?
> Without users having tested your type system you have no faith that
> your design or implementation are correct.
Tell me something else. Without users having tested a Haskell
implementation, would you have faith that it is correct ?
You seem to forget that a piece of code, whether a user-level library or
a language interpreter/compiler, is just a piece of code.
Oh frack. Now I'm arguing with JH :-)
--
Resistance is futile. You will be jazzimilated.
Scientific site: http://www.lrde.epita.fr/~didier
Music (Jazz) site: http://www.didierverna.com
EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bic�tre, France
Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22
Didier Verna wrote:
> Jon Harrop <···@ffconsultancy.com> wrote:
>> Didier Verna wrote:
>>> - you want dynamic typing in Lisp, you win. You want static typing, you
>>> don't loose (use Qi or write it yourself).
>>
>> Yeah, you just Greenspun the entire static type system yourself from
>> the ground up in Lisp
>
> Tell me something. At the time Haskell was born, didn't somebody, sort
> of, you know, write it ?
Today's Haskell is the result of years of evolution. Greenspunning its type
system in Lisp is not a winning strategy. That's why nobody does it.
Indeed, Lisp leaves huge room for improvement in many directions but even
the directions that are easier to address (e.g. pattern matching) are not
addressed in real Lisp software. A handful of Lisp programmers fumble on
with car and cdr indefinitely and everyone else leaves the ancient bog for
greener pastures.
>> Without users having tested your type system you have no faith that
>> your design or implementation are correct.
>
> Tell me something else. Without users having tested a Haskell
> implementation, would you have faith that it is correct?
Exactly. Haskell's type system has been tested by orders of magnitude more
users than the whole of Qi, let alone a your hypothetical new type system
implemented in Qi.
Haskell is mature. Your Greenspunned type system is not.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
·············@teh.intarweb.org (Robert Maas, http://tinyurl.com/uh3t) writes:
> So in your opinion, forcing programmers to spend most of their time
> formally declaring types of *all* places where data might be
> stored, both local variables and slots in structures/objects,
> writing twenty different kinds of CONS cells just because they
> happen to need to form twenty kinds of linked-lists each of which
> can store only one type of data in CAR places, and writing twenty
> different versions of each function where Lisp has a single
> function such as append or position or find, or messing with C++
> style "templates" for automatically generating twenty different
> versions of CONS cells and twenty different versions of each
> function that can be applied to the twenty different kinds of
> linked lists, leaving the programmer very little time to think
> about the logic of the program, is going to somehow minimize the
> chance of loss of money or life??
Happily, a remarkable new invention was made yesterday afternoon by
G. F. Froggble, who reports "parametric polymorphism", as he calls it,
addresses this very problem in statically typed languages. The good
old G. F. Froggble no doubt has many other inventions up his sleeve,
knowledge of some of which might well save you from such embarrassing
outbursts as the above in the future.
--
Aatu Koskensilta (················@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
On 2008-12-09, Aatu Koskensilta <················@uta.fi> wrote:
> ·············@teh.intarweb.org (Robert Maas, http://tinyurl.com/uh3t) writes:
>
>> So in your opinion, forcing programmers to spend most of their time
>> formally declaring types of *all* places where data might be
>> stored, both local variables and slots in structures/objects,
>> writing twenty different kinds of CONS cells just because they
>> happen to need to form twenty kinds of linked-lists each of which
>> can store only one type of data in CAR places, and writing twenty
>> different versions of each function where Lisp has a single
>> function such as append or position or find, or messing with C++
>> style "templates" for automatically generating twenty different
>> versions of CONS cells and twenty different versions of each
>> function that can be applied to the twenty different kinds of
>> linked lists, leaving the programmer very little time to think
>> about the logic of the program, is going to somehow minimize the
>> chance of loss of money or life??
>
> Happily, a remarkable new invention was made yesterday afternoon by
> G. F. Froggble, who reports "parametric polymorphism", as he calls it,
That's covered by Robert's mention of templates. The code bloat
is still there, just hidden from you by deduction.
Kaz Kylheku <········@gmail.com> writes:
> On 2008-12-09, Aatu Koskensilta <················@uta.fi> wrote:
>
> > Happily, a remarkable new invention was made yesterday afternoon by
> > G. F. Froggble, who reports "parametric polymorphism", as he calls it,
>
> That's covered by Robert's mention of templates. The code bloat
> is still there, just hidden from you by deduction.
Alas, you're mistaken. Good old G. F. Froggble's invention is more
ingenious than that. You will find more information in any text on
implementing a statically typed functional language with a type system
with parametric polymorphism. (I believe such texts have been
published as yearly as a few hours ago.) Of course, an optimising
compiler might well decide that outputting specialised instances of a
polymorphic function is a net benefit for these or those particular
types in this or that context, but that is not at all necessary.
--
Aatu Koskensilta (················@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
Robert Maas, http://tinyurl.com/uh3t wrote:
>> > > But if you'e going to do anything safety critical, nuclear reactors,
>> > > space probes, sensitive DBs, I think you really do need to have it.
>> > Why?
>> From: Mark Tarver <··········@ukonline.co.uk>
>> Well, because the consequence of error is so serious - either because
>> of litigation, loss of life or money - that you have to do everything
>> you can to minimise the chances of it happening.
>
> So in your opinion, forcing programmers to spend most of their time
> formally declaring types...
Before type inference (i.e. over 35 years ago) that would have been a valid
argument.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Jon Harrop <···@ffconsultancy.com> writes:
> Robert Maas, http://tinyurl.com/uh3t wrote:
>>> > > But if you'e going to do anything safety critical, nuclear reactors,
>>> > > space probes, sensitive DBs, I think you really do need to have it.
>>> > Why?
>>> From: Mark Tarver <··········@ukonline.co.uk>
>>> Well, because the consequence of error is so serious - either because
>>> of litigation, loss of life or money - that you have to do everything
>>> you can to minimise the chances of it happening.
>>
>> So in your opinion, forcing programmers to spend most of their time
>> formally declaring types...
>
> Before type inference (i.e. over 35 years ago) that would have been a valid
> argument.
I don't understand why you argue.
There is nothing in the Common Lisp standard preventing an
implementation to do type inference and to generate safe code with no
run-time type checking. On the contrary functions such as
COMPILE-FILE explicitely allow global optimizations (at the file
level), and an implementation could provide a EXT:COMPILE-APPLICATION
function to do even more global analysis and optimizations.
Since you're posting on cll, you're manifestly interested in lisp, why
not take a free implementation and add the level of type inference and
the code generation you want? Be sure that if well done, most lisp
programmers would eagerly use it to compile their lisp programs.
--
__Pascal Bourguignon__
Pascal J. Bourguignon wrote:
> Jon Harrop <···@ffconsultancy.com> writes:
>> Before type inference (i.e. over 35 years ago) that would have been a
>> valid argument.
>
> I don't understand why you argue.
>
> There is nothing in the Common Lisp standard preventing an
> implementation to do type inference and to generate safe code with no
> run-time type checking. On the contrary functions such as
> COMPILE-FILE explicitely allow global optimizations (at the file
> level), and an implementation could provide a EXT:COMPILE-APPLICATION
> function to do even more global analysis and optimizations.
>
> Since you're posting on cll, you're manifestly interested in lisp, why
> not take a free implementation and add the level of type inference and
> the code generation you want? Be sure that if well done, most lisp
> programmers would eagerly use it to compile their lisp programs.
That was done 35 years ago and the implementation was progressively
improved. Today, no Lisp remains.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Jon Harrop <···@ffconsultancy.com> writes:
> Pascal J. Bourguignon wrote:
>> Jon Harrop <···@ffconsultancy.com> writes:
>>> Before type inference (i.e. over 35 years ago) that would have been a
>>> valid argument.
>>
>> I don't understand why you argue.
>>
>> There is nothing in the Common Lisp standard preventing an
>> implementation to do type inference and to generate safe code with no
>> run-time type checking. On the contrary functions such as
>> COMPILE-FILE explicitely allow global optimizations (at the file
>> level), and an implementation could provide a EXT:COMPILE-APPLICATION
>> function to do even more global analysis and optimizations.
>>
>> Since you're posting on cll, you're manifestly interested in lisp, why
>> not take a free implementation and add the level of type inference and
>> the code generation you want? Be sure that if well done, most lisp
>> programmers would eagerly use it to compile their lisp programs.
>
> That was done 35 years ago and the implementation was progressively
> improved. Today, no Lisp remains.
Which is the reason why lisp programmers are not so much interested in it.
--
__Pascal Bourguignon__
On Dec 1, 1:05 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> On 1 Dec, 09:29, Slobodan Blazeski <·················@gmail.com>
> wrote:
>
> > Sorry for spamming but now when I'm reading a lot about static typing
> > and the *benefits* I really found this comic amusinghttp://blog.rvburke.com/2006/10/10/static-typing/
>
> > bobi
>
> That's very funny. I love Larson's cartoons.
>
> The reason university teachers prefer to teach FP from statically
> typed languages is that it forces students to think about the nature
> of the data structures they're working with. So its a good discipline
> for learners.
>
> More experienced programmers often skip it if they find it gets in the
> way.
>
> But if you'e going to do anything safety critical, nuclear reactors,
> space probes, sensitive DBs, I think you really do need to have it.
>
> Mark
Static typing catches SOME errors at compile time which is better than
nothing. But on the other side, static typing comes with a overhead,
that hogs my precious brain resources. And the more resources I had
spare the more I have to dedicate to the problem. That's why languages
with uniform syntax (lisp, j/q, joy/forth) make me feel comfortable
while languages with complex syntax make me feel crumble when problem
grows. From my own limited experience with statically typed languages,
I feel the tradeof is not worth it.
In the end I believe that it all depends of the person, and I'm not
statically typed person. Maybe having type system as optional is good
idea, but then question remains what happens when typed function
calls, untyped(unchecked) one. For me the implementation should issue
a warning, and accept the code and let me continue unbotered with my
business but to the purists that's unacceptable. The devil is the
defaults.
bobi
> that hogs my precious brain resources. And the more resources I had
> spare the more I have to dedicate to the problem. That's why languages
> with uniform syntax (lisp, j/q, joy/forth) make me feel comfortable
> while languages with complex syntax make me feel crumble when problem
> grows. From my own limited experience with statically typed languages,
> I feel the tradeof is not worth it.
Empirically there's something in that. A lot of statically typed
languages do have a complex syntax. O'Caml looks a nightmare to me.
But there's no conceptual connection between static typing and complex
syntax; its just the designers of these languages made that choice.
Another issue you don't like, I expect, is the need to declare all
those ugly constructor functions in your types. This was something I
detested myself when teaching ML and is one reason Qi exists. It
allows you to write your code in a natural way like a Lisp programmer
and still type check it - hence my examples in the audio talk 'Lisp
for the C21'.
A lot of the issues people have with static typing are a product of
choices made by the designers of a certain category of languages.
They are not inherent in the idea of static typing. Qi does not
follow them.
Mark
Mark Tarver wrote:
> Another issue you don't like, I expect, is the need to declare all
> those ugly constructor functions in your types.
Then use polymorphic variants.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Mark Tarver wrote:
> The reason university teachers prefer to teach FP from statically
> typed languages is that it forces students to think about the nature
> of the data structures they're working with. So its a good discipline
> for learners.
>
> More experienced programmers often skip it if they find it gets in the
> way.
That certainly explains why nobody uses Java and C# in the real world.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Slobodan Blazeski <·················@gmail.com> writes:
> Sorry for spamming but now when I'm reading a lot about static typing
> and the *benefits* I really found this comic amusing
> http://blog.rvburke.com/2006/10/10/static-typing/
Amusing, but he's used up his type space, demonstrating the brittle
class problem (well, sort of). He's called his dog "The dog". What
is he going to paint on a second dog his kids bring home? He hasn't
thought ahead to the dynamism of real life at home.
--
Duane Rettig ·····@franz.com Franz Inc. http://www.franz.com/
555 12th St., Suite 1450, Oakland, Ca. 94607
Duane Rettig <·····@franz.com> writes:
> Slobodan Blazeski <·················@gmail.com> writes:
>
>> Sorry for spamming but now when I'm reading a lot about static typing
>> and the *benefits* I really found this comic amusing
>> http://blog.rvburke.com/2006/10/10/static-typing/
>
> Amusing, but he's used up his type space, demonstrating the brittle
> class problem (well, sort of). He's called his dog "The dog". What
> is he going to paint on a second dog his kids bring home? He hasn't
> thought ahead to the dynamism of real life at home.
I thought his "The" was like lisp's (list (the dog my-dog-1) (the dog my-dog-2)).
--
__Pascal Bourguignon__
···@informatimago.com (Pascal J. Bourguignon) writes:
> Duane Rettig <·····@franz.com> writes:
>
>> Slobodan Blazeski <·················@gmail.com> writes:
>>
>>> Sorry for spamming but now when I'm reading a lot about static typing
>>> and the *benefits* I really found this comic amusing
>>> http://blog.rvburke.com/2006/10/10/static-typing/
>>
>> Amusing, but he's used up his type space, demonstrating the brittle
>> class problem (well, sort of). He's called his dog "The dog". What
>> is he going to paint on a second dog his kids bring home? He hasn't
>> thought ahead to the dynamism of real life at home.
>
> I thought his "The" was like lisp's (list (the dog my-dog-1) (the dog my-dog-2)).
If it had been like CL, then it wouldn't have been static. Or, at
least, he would have painted the names on signs hung around the
objects. These variables could then be rearranged to hang around
other objects, e.g. a second dog or cat. You could even lie and hang
the "the dog" sign on the cat...
Of course, once the picture of this scene is taken (i.e. compilation)
the die is cast, and the picture becomes a static representation of
life.
--
Duane Rettig ·····@franz.com Franz Inc. http://www.franz.com/
2201 Broadway, Suite 715, Oakland, Ca. 94612
Slobodan Blazeski <·················@gmail.com> writes:
> Sorry for spamming but now when I'm reading a lot about static typing
> and the *benefits* I really found this comic amusing
> http://blog.rvburke.com/2006/10/10/static-typing/
The cartoon is a perfect illustration of why type inference is often
very useful.
--
Aatu Koskensilta (················@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
Slobodan Blazeski wrote:
> Sorry for spamming but now when I'm reading a lot about static typing
> and the *benefits* I really found this comic amusing
> http://blog.rvburke.com/2006/10/10/static-typing/
As one of the commenters said: his experience is so limited that he has
never come across type inference.
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u