Thanks Mike for your reminder to be pragmatic. It is definitely the way to go.
Clojure's an incredible language for this.
This is going to be a longish post as I should better explain my position. It
is just a brief sketch of the problem but I think that we should be thinking
about it more as a fun exercise rather than a way to troll the haskell/scala/ml
mailing lists.
I'm not the type of person to get overly academic but I still want to have
`faith` in the tools that I'm using. In Indian traditions of philosophy, the
term `shraddah` is translated as `faith` but it literally means `that which
binds you` or `that which is unwavering`. Logical foundations of practices and
beliefs are debated by practitioners and scholars alike. To debate and win
against those in opposition, one has to have a good reason to believe in their
practice. In other words, academics is a VERY powerful tool for faith.
Because of the vast amounts of academic work around types, we now have a `type`
priesthood and an increasingly mass of `type converts` who are very
inflammatory against anything non-typed languages. The cult of haskell will
always look down on the cult of lisp/javascript/python/ruby, laugh and say `you
guys suck because you don`t have A, B, C which are features of type inference`.
Now with the `cult of clojure`, we can say YES WE DO (Typed Clojure)… but not
only that, we should also be able to say:
"Because we have optional typing, here are a bunch of problems that we can
solve very easy because X, Y and Z are not restricted by type inference."
Now The the debate actually moves forward, so that we ask ourselves whether
type-inference is suitable for solving a particular class of problems rather
than putting ourselves into opposite camps.
I have to come back to Godel's work as it is (quoting the lecturer) `The most
profound result to have come out of logic for the last 2000 years, ever since
the time of Aristotle`. What Godel did, was to write a hack that crashed a what
was thought to be an uncrashable system.
Principia Mathematica (PM) was a huge book which described how one can of about
using a subset of mathematics to reason without running into Russell`s Paradox
(which is the mathematical equivalent of saying `this statement is false`). It
was found that ANY system that referred back to oneself had the potential to
have this problem and so all of this circular referencing had to be eliminated.
The reason why the book was so thick was because most of the book was devoted
to teaching people how to write mathematics without using circular reference.
It was dense.
Godel constructed an equivalent system of calculation to that of PM and showed
that anytime the `+` operator was in the system, then it was possible to get
the system to talk about itself. Therefore, the phrase `This statement is
unprovable using our system` will result in a paradox in a system that was
thought the be free of them. Thus, Godel used the logic presented in the
framework itself to cause its own downfall.
This result put mathematics in its place, not as the single source of truth as
Russell and Whitehead, the authors of PM had wanted, but as an incredibly tool
despite its inconsistencies. It also eliminated the need for future
mathematicians to waste their time in order to build a complete system of
mathematics - Godel had proved beyond a shadow of a doubt that this was an
impossible task.
I see history repeating itself with the offspring of PM (type theory). Like PM,
It is brilliant and to be honest, it is too abstract for me. However, it is my
understanding that a lot of the leading research is repeating that of PM but
with an emphasis on computation. To avoid Russell`s paradox, types are always
hierarchical, never circular. To express circular referencing of types in a
none circular way requires a lot of time of a lot of smart people.
There is therefore a lot of pomp and ceremony in order to create a `correct`
and `complete` system of programming I don't think any of the researchers claim
this but it is sure marketed that way.
I believe that we have to put type theory in its proper place as a tool for
programmers and not as the saviour for programming (that mantle belongs to lisp
of course =p ) For example:
- one area that is difficult using types is to define multiple hierarchies
over objects - like properies of can-fly, can-swim, can-run over birds, mammals
and reptiles.
- Another area is with partial data. That is, when does a rose not become a
rose? when it looses its colour? fragrance? shape?. For example… can {:colour
:red} be considered a rose, even though a rose may be red?
On 06/10/2013, at 6:02 PM, Mikera <mike.r.anderson...@gmail.com> wrote:
> I suspect you are going to have zero success "proving" the superiority of
> dynamic languages (in an academic proof sense). For a start, people are even
> going to disagree about the precise definition of "better". What matters
> more: Runtime performance? Flexibility with respect to changing requirements?
> Ease of learning? Minimisation of typing? Ease of language implementation?
> Etc..... Any such "proof" based on your own definition of "better" isn't
> likely to convince others who hold different views.
>
> My suggestion: just don't worry about it, be pragmatic and use whatever you
> find helps you to build useful software. Ultimately, that is the main measure
> of success for a practical general purpose programming language.
>
> In particular, I suggest ignoring anyone who launches a "barrage of abuse".
> Language trolls probably aren't going to give you a sensible conversation in
> any case.
>
> On Sunday, 6 October 2013 11:35:20 UTC+8, zcaudate wrote:
> I'm a little bit miffed over this current craze of `types` and `correctness`
> of programs. It smells to me of the whole `object` craze of the last two
> decades. I agree that types (like objects) have their uses, especially in
> very well defined problems, but they have got me in trouble over and over
> again when I am working in an area where the goal is unclear and requirements
> are constantly changing.
>
> BTW... This is no means a criticism of all the type system work that is going
> on in the clojure community. I am a huge fan of Ambrose's Typed Clojure
> project because it gives me the option of using types... not shoving it down
> my throat. I like the freedom to choose.
>
> My experience of programming in clojure has freed me from thinking about
> types and hierarchies and this article rings so true:
> http://steve.yegge.googlepages.com/is-weak-typing-strong-enough.
>
> However, everywhere I look, there are smug type-weenies telling me that my
> dynamically typed program is bad because it cannot be `proven correct` and
> not `checked by the compiler`. This question on SO really makes me angry....
> http://stackoverflow.com/questions/42934/what-do-people-find-so-appealing-about-dynamic-languages....
> because no one is defending dynamic languages on there. The reason is very
> simple..... because we don`t have a theory to back us up!
>
> I do want to put up an counter argument against this barrage of abuse against
> dynamic languages. And I want to put some academic weight behind this. The
> only counter I could come up with was to use Godel's incompleteness theorem.
> For those that don't know... here is an introduction to the man and his
> theory. http://www.youtube.com/watch?v=i2KP1vWkQ6Y. Godel's theorem,
> invalidated Principia Mathematica as a complete system of description.
> Principia Mathematica btw.... effectively led to Type Theory.
>
> According to http://en.wikipedia.org/wiki/Type_theory. "The types of type
> theory were invented by Bertrand Russell in response to his discovery that
> Gottlob Frege's version of naive set theory was afflicted with Russell's
> paradox. This theory of types features prominently in Whitehead and Russell's
> Principia Mathematica. It avoids Russell's paradox by first creating a
> hierarchy of types, then assigning each mathematical (and possibly other)
> entity to a type. Objects of a given type are built exclusively from objects
> of preceding types (those lower in the hierarchy), thus preventing loops."
>
> I'm hoping to collect a few more `proofs` from the clojure community... for
> example... if there is a paper on "why are type systems so bad at classifying
> animals"... then please forward it on.
>
> --
> --
> You received this message because you are subscribed to the Google
> Groups "Clojure" group.
> To post to this group, send email to clojure@googlegroups.com
> Note that posts from new members are moderated - please be patient with your
> first post.
> To unsubscribe from this group, send email to
> clojure+unsubscr...@googlegroups.com
> For more options, visit this group at
> http://groups.google.com/group/clojure?hl=en
> ---
> You received this message because you are subscribed to a topic in the Google
> Groups "Clojure" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/clojure/0I7u5yn01qU/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
> clojure+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
--
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clojure@googlegroups.com
Note that posts from new members are moderated - please be patient with your
first post.
To unsubscribe from this group, send email to
clojure+unsubscr...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en
---
You received this message because you are subscribed to the Google Groups
"Clojure" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to clojure+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
