How to go about 'proving' why dynamically typed languages are better.

[zcaudate]

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. 

[Mikera]

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.

[Chris Zheng]

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?

--
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@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+u...@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+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Greg]

I support the sentiment expressed in your email. +1

Type systems are nice, just don't force them upon anyone. Keep the C++ at bay.

--
Please do not email me anything that you are not comfortable also sharing with the NSA.

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+u...@googlegroups.com.

[Phillip Lord]

zcaudate <z...@caudate.me> writes:
> 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.

Programming is a highly fashion-centric occupation for any number of
reasons. This shouldn't be a surprise.

> 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.

Types are good. But they have overhead.

One of the curious things about Clojure is that it can turn into a
strange mix of typed and untyped. I'm building a library in clojure
that, in turn, wraps a typed Java library. The types in Java are so
complex that one of my desires was to simplify that away. But,
ironically, I use a lot of reflection underneath to make it all work. If
I had type based dispatch (i.e. and yes, I know about multimethods), I
would use it lots.

> 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`.

But they are correct. You cannot answer this because it is true.

> 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.

Classifying animals is a difficult problem, although I quite liked this
paper when I read it. Don't bother if you were using a metaphor!

http://bioinformatics.oxfordjournals.org/content/24/13/i313.full


The best source for a counter argument would be to look at the
discussion comparing UML, design-driven approaches with the various
agile methodologies; the "less-is-more" argument is hard to push, but it
can work. For me, the main advantage is that you are not forced to build
complex hierarchies just to support the type system (and this holds for
Scala type languages with good type inferencing), and that having only a
few abstractions makes it worthwhile adding lots of functions operating
over them.

Phil

[Laurent PETIT]

IMHO, the question is irrelevant. It implicitly assumes that statically typed vs dynamically typed is a black / white choice, and that either "static wins over dynamic" or "dynamic wins over static" will be a true statement whatever the context.

Bu still ... :

I assume you are talking about the difference in how types are handled between e.g. Clojure and Java. Maybe I'm totally off-topic.

What do people used to Java fear a lot to lose if forced to use Clojure :

- code completion

- compiler errors

And they are right. You have less powerful code completion in Clojure right now, by the very nature of the state of things. And you have way few compiler errors.

I too like the fact that Typed Clojure is an optional feature, because then I can quickly prototype code without bothering with entering types. But this also means that I keep this information in my head, or in my comments. Because there's no chance that my Clojure program will accept to add a String and a Long at execution time.


I tend to think more in terms of "function contract", than in terms of types. I want to choose the level of "function contract enforcement" I keep in my head, or in my comments, or in my code. And then accept the consequences of having to type more, to get faster feedback (the faster being provided by the IDE, then the compiler, then the running code - and my own ability to reason about the code floating here and there depending on the moment).

Types are an implementation detail. They are just a subset of the kind of assertions a compiler or a runtime can do over the arguments passed to a function. They are just ONE property of each argument, and we're not even talking about inter-arguments assertions, such as (< arg1 arg2), etc.

But after having said that, I still think that it will be good to be able to declare types if I feel the need, because they have proven to detect early a whole class of problems when I was doing Java !

2013/10/6 zcaudate <z...@caudate.me>

--

[Chris Zheng]

Hahaha, thanks Philip. Does it really take a doctorate to understand classification of elephants?

I think the overall consensus is that having basic type checking is good... but over doing types is bad.

Would this be a reasonable guideline for using types?

1. Types are useful for structures that HOLD data (ints, strings, maps, arrays… ) because they provide ways defining standard operations to manipulate data that make sense in the context of that type of data. It is helpful to have a type checker check that I am not accessing the 6th element of a hashmap or that I am adding 10 to "Hello".

2. When a particular data-structure is sufficient for holding information, then its better to just use the data-structure because we have so many generic operations predefined.

> For example, if I have to model customers in a line. I wouldn't have type CUSTOMER and type LINE. I would just represent this as a QUEUE of
MAPS….

----

However… I find that I am writing a lot of statements like this:

(cond (hash-map? v)
……

(vector? v)
……

(list? v)
…..

:else …..)

I'm not sure a type checker will help in that instance.

[Jason Lewis]

I think what you're banging your head against is the tension between computer science qua pure science, versus software engineering qua engineering practice.

This tension isn't unique to our field; mathematicians look down on theoretical physicists, who look down on practical physicists, who look down on engineers, all the way down to the humanities, who are generally ignored. Or, to summarize:

So, sure, from a theroetical standpoint, oriented toward proofs and provable correctness, type systems are superior. OTOH, for practicing software engineers, who care more about reliably and efficiently building shit, language flexibility is a massive boon, and we compensate for the lack of "provable correctness" with strategies like TDD.

I agree w/ Laurent; it's not a black/white issue... to me it's more apples and oranges, dispatching on intent. Are you trying to prove a theorem, or build software? Not that you can't build scalable web services in Haskell, but I don't know anyone within a standard deviation of "sanity" who has ever done so for production code. The beauty of Clojure is that it gives us the ability to create realiable, robust, real-world solutions without sacrificing elegance; not because it's dynamically typed or because it has an optional type system (although both of those aspects are great), but because it combines power and simplicity. 

Holy wars are fun for a while (if I wanted to start one on this list, I'd go into the superiority of vim over emacs), but if your real goal is building things, you gotta let them go, and when people start heckling the fact that Clojure doesn't implement Hindley-Milner type inference... just shrug, point to the reliable, scalable architecture you built in two weeks, and get back to work.

Just my US$0.02.

Jason

[Paul Butcher]

On 6 Oct 2013, at 04:35, zcaudate <z...@caudate.me> 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.

This debate is as old as the hills (it certainly predates object-oriented programming). There's no question that there is a valid debate to be had about static versus dynamic typing, but most such debates are hamstrung by basic misunderstandings. 

The best explanation of these misunderstandings I've come across is "What to Know Before Debating Type Systems":

http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/

In particular it asserts (correctly in my view) that what static type system proponents mean by "type" and what dynamic type system proponents mean by "type" are very different things. Most debates founder on a failure to recognise that difference.

--
paul.butcher->msgCount++

Snetterton, Castle Combe, Cadwell Park...
Who says I have a one track mind?

http://www.paulbutcher.com/
LinkedIn: http://www.linkedin.com/in/paulbutcher
MSN: pa...@paulbutcher.com
AIM: paulrabutcher
Skype: paulrabutcher

[Phillip Lord]

Chris Zheng <z...@caudate.me> writes:
> Hahaha, thanks Philip. Does it really take a doctorate to understand
> classification of elephants?

I have a doctorate in how yeast divide. Trust me, computers are easy in
comparison to elephants.

> I think the overall consensus is that having basic type checking is
> good... but over doing types is bad.
>
> Would this be a reasonable guideline for using types?
>
> 1. Types are useful for structures that HOLD data (ints, strings,
> maps, arrays… ) because they provide ways defining standard
> operations to manipulate data that make sense in the context of
> that type of data. It is helpful to have a type checker check
> that I am not accessing the 6th element of a hashmap or that I am
> adding 10 to "Hello".

This would be useful indeed. Although, a hard core type head would say
"I want to distinguish between a string that is an email, someones name,
and a day of the week". This is not unreasonable.

> However… I find that I am writing a lot of statements like this:
>
> (cond (hash-map? v)
> ……
>
> (vector? v)
> ……
>
> (list? v)
> …..
>
> :else …..)
>
> I'm not sure a type checker will help in that instance.

A type-checker wouldn't no, but a type system would; pretty much
every language with a static type system has a type based dispatch
somewhere. It would be nice to be able to do

(defun fn
([^vector v] ...)
([^list l] ...)
([else] ...)


I guess that core.logic will support this at some point.

Phil

[John D. Hume]

On Oct 8, 2013 5:35 AM, "Phillip Lord"

>
> > However… I find that I am writing a lot of statements like this:
> >
> > (cond (hash-map? v)
> >             ……
> >
> >            (vector? v)
> >             ……
> >
> >            (list? v)
> >            …..
> >
> >             :else …..)
> >

zcaudate, in what context(s) do you find yourself writing a lot of expressions like that? I rarely want to allow so much flexibility in arguments. I'm wondering if there are idioms to avoid it.

> > I'm not sure a type checker will help in that instance.
>
>
> A type-checker wouldn't no, but a type system would; pretty much
> every language with a static type system has a type based dispatch
> somewhere. It would be nice to be able to do
>
> (defun fn
>   ([^vector v] ...)
>   ([^list l] ...)
>   ([else] ...)

How is Clojure's protocols feature different from what you're describing?

[Nando Breiter]

>
>   1. Types are useful for structures that HOLD data (ints, strings,
>      maps, arrays… ) because they provide ways defining standard
>      operations to manipulate data that make sense in the context of
>      that type of data. It is helpful to have a type checker check
>      that I am not accessing the 6th element of a hashmap or that I am
>      adding 10 to "Hello".

This would be useful indeed. Although, a hard core type head would say
"I want to distinguish between a string that is an email, someones name,
and a day of the week". This is not unreasonable.

Perhaps some may see this as an oversimplification, but ...

If you try and add 10 to "Hello" in a typed language, you get an error. If you try to do the same in a dynamic language, you get an error. The only difference seems to be that in a dynamic language, you need to run the code to get the error, rather than compile it. 

That said, not all programming errors in a typed language will be found at compile time, so these need to be run anyway to test them.

As I understand it, in a dynamic language, if you want to check if a string is an email, you need some function like defn (email? [str]). You'd need the same in a typed language.

I've never understood the essential distinction here. (+ 10 "Hello") doesn't work in both dynamic or typed languages because, well, 10 and "Hello" are different types of things. Both dynamic and typed languages interpret them as different types. 

I do understand, however, that typed languages are more difficult to learn and program in, and that the same task can take longer in a typed language. 

It also seems to me that it is easier to lose the forest for the trees in a typed language. When we speak with each other, we don't generally say "The number 6 plus the number 4 equals the number 10." There's a good reason for that. "6 plus 4 equals 10" is not only sufficient, but easier to understand. The incidental complexity that type systems add can foster programming errors, even as typed languages are supposed to prevent them. 

[Joseph Smith]

 Just bc it's dynamically typed doesn't mean you can't leverage types for dispatch. Remember, you can single dispatch on type (using protocols), or multi-dispatch using a function applied to the arguments (multimethods). 

---

Joseph Smith

j...@uwcreations.com

@solussd

--

[Robert Day]

On 08/10/13 13:49, Nando Breiter wrote:
>
>
>
> If you try and add 10 to "Hello" in a typed language, you get an
> error. If you try to do the same in a dynamic language, you get an error.

Not necessarily...

$ perl
print 10 + "Hello", "\n"


^D
10
$

Rob

[Laurent PETIT]

2013/10/8 Robert Day <rober...@gmail.com>

Then don't use Perl :-p

[Gary Trakhman]

I think there's a case to be made for a theoretical subjectivity.

Mathematical purity is nice and elegant, sometimes useful, but 'useful' refers to utility.  The ease or the cost of making some valuable change to code in the possibility-space of changes you might make, and the ramifications of that change are directly proportional to utility.  Understanding the theoretical, but discerning the 'useful' is what makes an engineer effective, and that's the difference between an engineer and a theoretical computer scientist.

I can say objectively that clojure is useful, because programs are read and languages are worked in subjectively by subjective humans, and I find it more useful than other things.  That's at least a statistical measure (mathematicians frown on statistics too?  Statistics are definitely useful, as anyone with a working cell phone should appreciate).

If there's a theory that I could explore more to make a case, it would be one of cognitive load, mental 'overhead', and the convenience of removing classes of worries (say, action at a distance), letting you reason about your program in side-effect-free chunks.  The easier it is to draw lines around chunks of your program, or the lower the time/effort cost of changing code to make the first easier, the less benefit there is to be had in types/contracts, in my opinion.  Practical engineering is about the economics of the process, and it's about how our tools plus outside constraints limit our solutions.

Mathy guys value 'objectivity', as that's the accepted social currency that's ingrained in techies.  Clojure has a rich/proven heritage and a coherent/enabling design, and programs are written and read by people, so I think it's ok to admit that the subjective is 'useful' when there's enough objective common ground.  We will be the most persuasive when we understand the theory and point of view of the other side of the argument, and we can effectively engage in the economics of that kind of reasoning.

--

[Phillip Lord]

"John D. Hume" <duelin....@gmail.com> writes:

> On Oct 8, 2013 5:35 AM, "Phillip Lord"

>> > I'm not sure a type checker will help in that instance.
>>
>>
>> A type-checker wouldn't no, but a type system would; pretty much
>> every language with a static type system has a type based dispatch
>> somewhere. It would be nice to be able to do
>>
>> (defun fn
>> ([^vector v] ...)
>> ([^list l] ...)
>> ([else] ...)
>
> How is Clojure's protocols feature different from what you're describing?

Yeah, I picked a bad example, following on from the previous.

I was thinking where the classes are defined in Java and there are
several of them -- class based overloading in otherwords.

Phil

[Angel Java Lopez]

Short comment in bad English:

I found that TDD is the great equalizer btw "dynamic and static" languages. I don't have any trouble writing code in dynamic language wo/code completion, etc.. if I wrote "baby steps" using TDD. And then, the dynamic nature (less ceremony, etc...) starts to shine.

I use typed language for performance reasons. 

Angel "Java" Lopez

@ajlopez

[Phillip Lord]

Nando Breiter <na...@aria-media.com> writes:
>> > 1. Types are useful for structures that HOLD data (ints, strings,
>> > maps, arrays… ) because they provide ways defining standard
>> > operations to manipulate data that make sense in the context of
>> > that type of data. It is helpful to have a type checker check
>> > that I am not accessing the 6th element of a hashmap or that I am
>> > adding 10 to "Hello".
>>
>> This would be useful indeed. Although, a hard core type head would say
>> "I want to distinguish between a string that is an email, someones name,
>> and a day of the week". This is not unreasonable.
>>
>> Perhaps some may see this as an oversimplification, but ...
>
> If you try and add 10 to "Hello" in a typed language, you get an error. If
> you try to do the same in a dynamic language, you get an error.

This depends on the type coercions which are available, rather than the
static/dynamic type system divide.

echo print 10 + "10" | perl
20

for instance.

> The only difference seems to be that in a dynamic language, you need

> to *run* the code to get the error, rather than compile it.

This is a big difference, especially, if the code is hard to test.

> As I understand it, in a dynamic language, if you want to check if a string
> is an email, you need some function like defn (email? [str]). You'd need
> the same in a typed language.

To a first approximation, yes, but once you have constructed an "email"
type, and got a value into that type, then in a strongly typed language,
you know that you have an email. You cannot accidentally pass a string
which is not an email by mistake.

> I do understand, however, that typed languages are more difficult to learn
> and program in, and that the same task can take longer in a typed language.

I think "learn" is true. The second conclusion I think is wrong. The
joyful experience of passing a map of lists when you were expecting a
map of sets, or typing a keyword wrong happens to most people; and it
can take a long, long time to find out where.

> It also seems to me that it is easier to lose the forest for the trees in a
> typed language. When we speak with each other, we don't generally say "The
> number 6 plus the number 4 equals the number 10." There's a good reason for
> that. "6 plus 4 equals 10" is not only sufficient, but easier to
> understand.

Hmmm. So when you are teaching programming to beginers and you try to
explain why 20 + "20" crashes, how do you describe in, using the terms
that you find sufficient?


> The incidental complexity that type systems add *can* foster

> programming errors, even as typed languages are supposed to prevent
> them.

This hasn't been my experience; I do sometimes find that it take take so
longer to shut the damn compiler up and just have it do what I know
will work that it's not worth the effort.

Phil

[Softaddicts]

I am now allergic to integrated type systems mostly because of the lack of
efficiency that they impose, at least in my world.

If I can spare some time, I would like to immerse myself in Haskell to see
if I can cope with its type system on a daily basis.

Still I would think twice before switching to a language that imposes one on me
again.

Clojure.type looks to me reasonable because it's optional and annotations
have no effect on the running code.

My academic track record is thin, I always preferred to deliver projects
than work on academic studies and this taints my opinion.

I do not reject academic thinking, it's needed at some point to create new
foundations for practical applications. Clojure is a good example of this
interaction.

However I am always cautious about debates like this vs
real life project comparisons, like any tool they are limits to
what theory can prove. Program correctness has been in their air for several
decades however in real projects, its applicability has been scarce to
non-existent.

I know of a Swiss engineer that was building bridges using concrete and
none of his designs could be proven by mathematical models in his
lifetime. He was using 1/3 of the concrete is competitors were using...
Is bridge designs are elegant and sophisiticated.

I think there is still a huge gap between academic thinking and real life software
projects in general.

This is not a criticisim, theory as to lead practical applications, however
proofing has to be based on facts otherwise discussions are circling around.

A solid basis for a real debate would require some extensive survey of software
projects and maintenance with a number of facets (cost, timeline, #bugs,
language used, ....)

Luc P.

> 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

> --
> --
> You received this message because you are subscribed to the Google
> Groups "Clojure" group.
> To post to this group, send email to clo...@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+u...@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+u...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>

--
Softaddicts<lprefo...@softaddicts.ca> sent by ibisMail from my ipad!

[Michael Swierczek]

On Tuesday, October 8, 2013 6:26:20 AM UTC-4, Paul Butcher wrote:

The best explanation of these misunderstandings I've come across is "What to Know Before Debating Type Systems":

http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/

In particular it asserts (correctly in my view) that what static type system proponents mean by "type" and what dynamic type system proponents mean by "type" are very different things. Most debates founder on a failure to recognise that difference.

--
paul.butcher->msgCount++

Thanks for that link, it's a pretty good article.

No amount of proof is going to make your software ironclad.  You could start the program, but the operating system only has half as much memory available as it requires.   Your network connection could be down.  The database could be off, or someone could have changed the user account password.   The configuration file could be corrupted.  The SQL statement in your code (or properties file, or whatever) could have a spelling error.  You could have a dependency on a library with an undiscovered bug. 

We take for granted that outside of our programs' specific internals, the rest of the world can go insane, break our software completely, and there's nothing we can do but try to detect the error early and fail gracefully.   I like the Scala language, but even if you push its static type system to its limits, it's like building a house with invincible walls on one side - you better hope the tornado winds all blow from that direction, because otherwise you're in just as much trouble as the people living in a lean-to. 

But back to practicality - Ebay was originally written in Perl.  Myspace was written in ColdFusion.  Facebook was written mostly in PHP.  Youtube was written in Python.  Twitter was writtin in Ruby.  Most of the tools around KVM virtualization in the Linux kernel are written in Python.  Slashdot was written in Perl.   Of course most or all of these sites had to do extra work once they were dealing with a massive volume of traffic, but how many of us have that problem?  When I'm making a million dollars a month and programming language X has some fundamental aspect that prevents better scaling, I'll look into languages with better performance.   But I see the state of the modern web as proof enough that non-static type systems work just fine for an overwhelming number of use cases.

-Mike

[Phillip Lord]

Laurent PETIT <lauren...@gmail.com> writes:
>> print 10 + "Hello", "\n"
>>
>>
>> ^D
>> 10
>> $
>>
>>
> Then don't use Perl :-p

PHP does the same thing and it's really useful. We all think that the
ability to build DSLs in Clojure is good; ultimately, what this means is
that we think that good language behaviour is domain specific. For
webpages, I think this kind of coercion can be good.

It would be easy to get Clojure to behave in the PHP way, while it is
rather harder to stop PHP from doing this.

Phil

[Greg Bowyer]

js> Array(16).join("wat" - 1) + " Batman!"

"NaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaN Batman!"

js> 

[Laurent PETIT]

2013/10/8 Greg Bowyer <gbo...@fastmail.co.uk>

js> Array(16).join("wat" - 1) + " Batman!"

"NaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaN Batman!"

js> 

 

One of the many reasons we're using Clojurescript and not raw javascript :-) 

On Tuesday, October 8, 2013 6:07:47 AM UTC-7, Laurent PETIT wrote:

2013/10/8 Robert Day <rober...@gmail.com>

On 08/10/13 13:49, Nando Breiter wrote:

If you try and add 10 to "Hello" in a typed language, you get an error. If you try to do the same in a dynamic language, you get an error.

Not necessarily...

$ perl
print 10 + "Hello", "\n"


^D
10
$

Then don't use Perl :-p

--

[Cedric Greevey]

On Tue, Oct 8, 2013 at 8:49 AM, Nando Breiter <na...@aria-media.com> wrote:

If you try and add 10 to "Hello" in a typed language, you get an error.

Interesting. I hadn't realized that the following's language was not typed:

package foo.bar;

public class Main {

    public static void main (String[] args) {

        System.out.println("Hello" + 10);
    }
}

% javac Main.java

% java foo.bar.Main
Hello10
%

:)

[Jonas]

On Tuesday, October 8, 2013 10:19:07 PM UTC+3, Laurent PETIT wrote:

2013/10/8 Greg Bowyer <gbo...@fastmail.co.uk>

js> Array(16).join("wat" - 1) + " Batman!"

"NaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaNNaN Batman!"

js> 

 

One of the many reasons we're using Clojurescript and not raw javascript :-) 

ClojureScript is an improvement, no doubt about that! But javascript idiosyncrasies does leak through on occasion: http://cljsfiddle.net/fiddle/jonase.batman

[Joe Smith]

The string concatenation operator in java calls 'toString' on it's args.

---

Joseph Smith

j...@uwcreations.com

@solussd

[Luc Prefontaine]

Hopefully, we all knew it :))

And you should add that auto boxing
Is done on the literal, otherwise this
magic would not work.

Otherwise, Java would be the most
brittled language.

It probably is anyway :))

Luc P..

--
Luc Prefontaine<lprefo...@softaddicts.ca> sent by ibisMail!

[Chris Zheng]

>> "Holy wars are fun for a while (if I wanted to start one on this list, I'd go into the superiority of vim over emacs),"

It wasn't me =)

Don't get me wrong, I'm not ANTI-type. I'm ANTI-ANTI-untype… which is a much more partial position to take =)

On 08/10/2013, at 11:46 PM, "John D. Hume" <duelin....@gmail.com> wrote:

> > (cond (hash-map? v)
> >             ……
> >
> >            (vector? v)
> >             ……
> >
> >            (list? v)
> >            …..
> >
> >             :else …..)
> >

zcaudate, in what context(s) do you find yourself writing a lot of expressions like that? I rarely want to allow so much flexibility in arguments. I'm wondering if there are idioms to avoid it.

I do it for operator overloading/syntactic sugar…. http://z.caudate.me/ova/#indices-selection

Also, they are quite useful for macros… https://github.com/zcaudate/purnam

As well as custom representation of data and also for traversing nested maps… https://github.com/zcaudate/adi

-----------

Chris.

[Chris Zheng]

I have another question re types…. I find it hard to express the absence of properties….

Like in Haskell… if you want to display something.. you have to derive Show for that object… which I think is allowing .toString to work

Wouldn't it be more helpful to have a type Unshow which stops the object from being shown?

There are some things that are universal and it is the absence of that which is unique. Is there a way to model this with types?

[Kendall Shaw]

Some things that I see most of the time when I read debates about dynamic vs static are:

1. Statically defined types don't solve everything, so they are not useful.

Some help is better than no help even if the help doesn't solve all of your problems.

Yes, you should wash your hands before dinner, even though we are all going to die in the end anyway.

2. I like static typing as long as it is optional

In the case where the point of using statically defined types is to have a compiler catch problems instead of you needing to predict their occurrence then static typing would have to be non-optional.

3. You don't need the compiler to warn you about types, because you can write tests.

A difficult problem is one that occurs on a rare occasion in some place that you would not have thought to check. So, you can't expect to be able to catch them with tests. If the problem is one that would have been flagged as a compile-time error, then in that case it would have been useful to have been using static typing.

I am still unsure. It seems likely that the usefulness of statically defined types would depend upon the application. When using statically defined types makes development slower to an extent that outways the benefit, then it is bad. If  faster initial development as a result of dynamic typing ultimately ends up taking more time because of problems that would have been caught by a compiler, then it is bad. If statically defined typing makes you not discover things you would have because of the overhead of dealing with the static typing, then that is bad.

Kendall

On 10/05/2013 08:35 PM, 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 clo...@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+u...@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+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

-- 
ThisIsHardToRead, asIsThis. This_is_easier, unless_it_is_underlined. This.is.easy. This-is-easy-too. Almost as easy to read as this.

[Joseph Smith]

This is Clojure- we can have both, at the same time! 

clojure.core.typed

---

Joseph Smith

j...@uwcreations.com

@solussd

[Dennis Haupt]

while i can see the strengths of both sides, the ideal solution is imho
this:

everything is statically typed. always. but you *never* have to write
the type explicitly. you *can* do it, but it is always optional.

i made good experiences with both scala and haskell (although i just
wrote minor things in the latter). the compiler really helps spotting
oops-errors early on, and the ide (in case of scala) has a lot of
information about the code and can assist you in ways that are simply
impossible without static typing.

please, do not confuse "java" with static typing. static typing could
also track all supported methods of an object as its type. imagine java,
but let every class implement one interface for each method that can be
called on it - its inferred type is, instead of just a simple class, the
set of interfaces necessary for the code to compile.
to actually write that would be completely annoying, but if a compiler
actually does the work for you and breaks it down, you would have a lot
of error checking and static information without losing much flexibility

>> Typed Clojure project because it gives me the *option *of using

[Softaddicts]

Yes the kind of app you are working on may make your mileage vary.
But not only this criteria impacts how good you can fare with
imposed data types.

One tendency in software development is to normalize everything up to
a point where two values are identical but because they have been typed
differently they are not comparable anymore or interchangeable.

The perversion here is that data typing at some point becomes a pain in
the a... Especially when you want to make changes to your software.
You inherit rigidity along the way and you have to pay for it as you go and
an extra fee later.

Having optional type checking allows you to pay the price where it's needed.
I do not see why this is a problem. In any project you have to compromise
on many factors.

One great example is documentation, this is
the first thing that gets axed when the schedule gets tight.

Why not have this flexibility with the data type system ?
Some components might benefit from it while others will not.
You may consider data typing as a form of documentation but
do you want to pay the price down to this level ?

Low level documentation fail at describing component interactions
(javadoc is a great example of verbosity w/o useful content).

Better dedicate some time to write a higher level document than
painfully type all the values in your software wall to wall.

Luc P.

> > Typed Clojure project because it gives me the *option *of using

[Nando Breiter]

The best explanation of these misunderstandings I've come across is "What to Know Before Debating Type Systems":

http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/

I have learned quite a lot from reading this article and following this discussion, particularly that "type" and "type checking" is much more nuanced and complex than I have understood until now, and that the terms "static" and "dynamic" expand into a much larger range of issues upon close examination, such as the difference between explicitly declaring types (as in Java) and implicitly inferring types from code context. Quoting from the article:

Many programmers approach the question of whether they prefer static or dynamic types by comparing some languages they know that use both techniques. This is a reasonable approach to most questions of preference. The problem, in this case, is that most programmers have limited experience, and haven’t tried a lot of languages. For context, here, six or seven doesn't count as “a lot.”

So I can say I prefer dynamic typing, but the reasons are more personal, and molded by my development experience. 

[Dennis Haupt]

let's see...

really used:

sql

java

javascript

basic

pascal/delphi

scala

experimented with:

logo (some old language intended to teach people to make their first steps)

haskell

kotlin

clojure

seen in action:

php

groovy

still prefer smart static typing :D

2013/10/9 Nando Breiter <na...@aria-media.com>

--

[Softaddicts]

Let's see:

strong data typing:

Fortran
Cobol
Pl/1
Pascal
C/C++
Java
C#
Ruby

à la carte data typing or no data typing at all:

Basic (more or less depending on the implementation)
Lisp
Clojure
A dozen assemblers
A dozen scripting languages

And I probably forgot some while excluding the ones I worked with
(Algol, Simula, GPSS, ...) in academic projects. I used the above ones
on real projects at work and not small projects.

Lets keep SQL out of the picture, it's an exaggeration to call this a programming
language.

Still prefer less data typing or no typing at all :)

Luc P.

> > *Many programmers approach the question of whether they prefer static or

> > dynamic types by comparing some languages they know that use both
> > techniques. This is a reasonable approach to most questions of preference.
> > The problem, in this case, is that most programmers have limited
> > experience, and haven’t tried a lot of languages. For context, here, six or

> > seven doesn't count as “a lot.”*
> > *
> > *

[Dennis Haupt]

especially haskell & scala are missing in your list :)

as long as you haven't at least seen haskell, you haven't seen the creme de la creme of statically typed languages

2013/10/9 Softaddicts <lprefo...@softaddicts.ca>

[Angel Java Lopez]

And JavaScript is missing (OK, "a dozen scripting language")

But today, JavaScript is very important in the picture.

Even Clojure has ClojureScript

[Softaddicts]

That's what I said earlier, I need to find some type to dive into it.
As far as Scala is concerned, it's not on my list of items to learn.
Too Java-ish to me and clunky. It's not because you mix all the latest
features in a single language that the result is a significant landmark.


It took a significant amount if time to Haskell designers to think about

feature set, it's not the same caliber at all.

Before choosing Clojure for our product, I looked at it and rejected it and
still have no regrets doing so.

Java in it's future releases will follow on the same slippery road of feature
aggregation w/o coherency, the "let's please everyone" approach
never led to anything exceptional.

It makes only things more confusing thanks to these guys...

http://search.dilbert.com/search?p=R&srid=S3-USESD01&lbc=dilbert&w=marketing%20idea&url=http%3a%2f%2fdilbert.com%2fstrips%2fcomic%2f1999-02-06%2f&rk=7&uid=203834662&sid=2&ts=custom&rsc=YmDLFs%3as9q%3aosTfU&method=and&isort=date&view=list&filter=type%3acomic

Luc P.

[Softaddicts]

Yeah but I hate JavaScript so no wonder it's not on the list.
I do however code in ClojureScript and avoid JS interop like
the plague as much as possible :)

I had to deal too much with browser based GUIs before things like JQuery

and similar things came to life or because the back end framework did not
allow me to use something more brilliant than plain JS... it got me disgusted
pretty much.

ClojureScript has changed my approach to browser based apps but
w/o JS as much as possible, now I can conceal my app logic in the
browser while using the back end as a resource provider.

No more Dr Jekyll and Mr Hide syndrom...

Luc P.

[Angel Java Lopez]

Oh!

I don't hate JavaScript ;-)

I'm not a Clojure programmer, (and not a ClojureScript programmer). But I usually program in C#, Java, PHP and JavaScript. I know Lisp, Ruby and Python, but I don't "work" with them, only toy projects.

I found JavaScript the most flexible programming language (less ceremony than Ruby or Python), and combined with Node.js at server, browsers at client, JSON for messaging, and TDD, it shines!

Any quirk on JS language is easy to circumvent (ie. using module pattern, build and exercised with TDD), and IMO, it pays a lot to use it.

Angel "Java" Lopez

@ajlopez

For more options, visit https://groups.google.com/groups/opt_out.

[Softaddicts]

I hate "quirks", too many things to achieve, less time remaining, less
brain estate to remember quirks :)

Luc P.

[zcaudate]

@philip lord.

Where would mutant elephants and the elephant god Ganesha fit in that classification?

[Phillip Lord]

zcaudate <z...@caudate.me> writes:
> @philip lord.
>
> Where would mutant elephants and the elephant god Ganesha fit in that classification?

It might surprise you to know that there is actually quite a lot work on
both of these.

The problem with mutant elephants generalises into the problem with
abnormalities; for example, if I build a model of a human which says,
"humans have two hands, and two legs" then there are plenty of counter
examples, having more or less than two hands (mostly less). If, on the
other hand, you have a model which can cope with these exceptions, then
it gets too complex to handle, and you can rarely conclude anything
useful.

Ganesha causes a different problem: that is does he exist at all, and if
he does, is he an elephant. Now there are those who say no he isn't, so
he shouldn't be in the model. And, there are those (like me) who say,
well it depends on your application and what you are trying to achieve.

Farcical as all of this sounds, it does actually have implications for
the way that we build data models, particularly for biology and
medicine. If you are interested, you can read my paper on the subject
here:

http://www.russet.org.uk/blog/1713

And a companion article by my co-author. It's about unicorns, but most
of it probably covers Ganesha also.

http://robertdavidstevens.wordpress.com/2011/05/26/unicorns-in-my-ontology/

Phil

[Dennis Haupt]

in my mental world, there is a "pure human", and a 4 armed human would probably be a 95% human or something, just like a hobbit would be. the other way round, a human would be a "95% hobbit". an elephant would be 4% hobbit on that scale.

this model is flexible, covers everything, and is not really helpful when you ask "what is it?" you have to ask "is this at least 90% cat?"

2013/12/20 Phillip Lord <philli...@newcastle.ac.uk>

[Chris Zheng]

Thanks Phil.

I'm exploring how type theory works at doing partial classifications, especially where there can be arbitrary models on the same object. I'm not sure that it does and I'm of the opinion that in these cases, type systems aren't really that useful.

Ganesha is surgically grafted elephant.. Only his head is because it got cut off and they stuck an elephants head on him.... Then we can have undead elephants.   I would still call it an elephant.. But is it even alive?

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+u...@googlegroups.com.

[Chris Zheng]

@dennis - how would this model work on a type system?

----

I also believe that type systems are very awkward for modelling change - whereas a schema system like datomic is do much better because it is a lot looser in the constraints. For example, if we are modelling the stages if growth of a person, as well as the functions that they perform - baby, teen, further study/ work, career change, two jobs, parenting, etc... The type 'person' would have to be very generic, and pretty much the same as type 'nested map'. 

I like that typed clojure supports map checking and so it is not really 'typed clojure' in the traditional sense, but 'schema clojure' in the way datomic advocates use of data types.

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+u...@googlegroups.com.

[Richard Cole]

The things is that dynamically typed languages are easier to implement than statically typed languages. Static typing comes down to making statements about the program and deriving other statements from them. It leads to all sorts of interesting work including I think into systems like Z. However theorem provers are limited in what they can do, and it can be both limiting and a big distraction to you as programmer to get into a dialogue with the theorem prover about your program. It can distract you from your original intention which was to write a program to do something in particular.

So simply put, dynamic languages are better than static ones because they don't distract you with type discussions that can end up being unprofitable or limiting. Static languages are better because sometimes the type discussions lead to early and convenient detection of bugs and can also in some cases make it easier for other people to understand you program or how to use your library. Static types I think also help refactoring tools.

Having optional typing in clojure is very nice. It allows for a lot of experimentation and research on type systems and for them to be used to the extent that people find them useful in their work.

It is why I guess Alan Kay said that lisp is not a language, it's a building material.

If you want to know what are the current problems in static typing you going to have to start learning what people are doing in that field, e.g. is their foreign function interface from Haskel to Java? Why not? Can a well typed program still exhibit bugs? If the type checking is so powerful why do bugs persist? You might also look at what Gilhad Brakka was attempting to do with newspeak and his notions of types being anti-modular. You are not going to find a proof that that line of enquirely is fruitless, you'll instead find what people can do today in that field and where they're pushing the bounds.

regards,

Richard.

[Manuel Paccagnella]

Just a link to the Gilad Bracha post Richard Cole is referring to: Types Are Anti-Modular.

[Korny Sietsma]

This ties in nicely to my summary of how I feel about static typing: Static typing is a premature optimisation.  Like most optimisations, it has genuine value, but if you apply it globally and too early, you end up causing more pain than you gain.

"sometime type discussions lead to lead to early and convenient detection of bugs" - I'd agree with this; but in my experience, most of the bugs caught by type systems are relatively simple and straightforward, and not the sort of bugs that make it into production.  I've almost never seen a _serious_ bug caused by dynamic typing - and I've seen plenty of serious bugs that type systems would not have caught.

Static types also help with rapid IDE/compiler feedback of errors - but you often pay for this with slow compilation, especially when you need global type inferencing; and with complex (and often buggy) IDEs/compilers.  I had huge pain getting the Scala IDEs to work reliably, last time I worked in Scala (admittedly this was a few years ago) - and they are still having lots of pain with performance, even though Scala doesn't have global type inference.

Statically typed code generally performs better - but if there's one major rule I've learned in 25 years in IT, it's that code performance is not your real problem, 99% of the time. Your real problem is more likely to be IO, or poor algorithm design, or inefficient scalability, or slow speed of development, or difficulty diagnosing bugs, or unreadable unmaintainable code.  I had people telling me that C++ was too slow, I should stick to C.  Then, that Java was too slow, I should stick to C++.  Then, that Ruby/JavaScript was too slow, I should stick to Java.  None of these people were right.  These days, I'd generally optimise first for expressive code so it's fast to develop and maintain; then for powerful flexible languages that can do anything I need them to do, and last for raw performance.

I'm quite attracted by optional static typing, because it means I can rapidly code in a flexible dynamic language, and if I get to the point where I really need types, I can add them.  But I suspect that most of the time, I'll never get to that point - or I'll use something like Prismatic Schema to define constraints at my external interfaces only, which is where I generally find I need them.

- Korny

--

--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@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+u...@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+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

--

Kornelis Sietsma  korny at my surname dot com http://korny.info

.fnord { display: none !important; }

[Jon Harrop]

Do you guys have any concrete examples?

Sent from my iPhone

[Luc Prefontaine]

I agree entirely with Korny's
statements.

As for concrete examples ?
Hard to enumerate some, I can only
say I agree after more than 30 years
coding in various languages and
finally getting out of Java hell.

When I started there were a variety
of dynamic languages used in the
industry and given the kind of
hardware we had at our disposal
(more or less the power of today's
cheap pocket calculator) the so-called
"Performance hit" was rarely a
problem.

With the hardware available today,
this is not a bigger issue than 25
years ago, except maybe for some
highly specific problems.

I saw enough typed language driven
systems performing poorly to say
that statically typed languages are not
bullet proof performance wise.

As for "discovering" significant errors,
that's a false claim. So good a
compiler may be, nothing can replace
your brain.

If the language and its related tools
make your job so complex that your
brain overloads then you are
shooting yourself in the foot.

Luc P.

[Mikera]

This article makes some interesting points, but it seems to draw the wrong conclusions.

The thing that is anti-modular isn't the types: it is depending on the internal implementation details of another module. If you expose too much of the implementation details in your interface declaration, that's not the fault of types: it's just bad API design. 

You have exactly the same problem with dynamic typing, e.g. if you place too many implicit requirements on the specific contents of a nested map data structure in your API contract. Except now your dependency on the internal implementation just blows up at runtime rather than being enforced at compile time. Ever had to debug a NullPointerException because you forgot to include some specific key in a parameter map?

The obvious solution (in the static typing case at least): Use a well defined interface at the module boundaries that uses types from common/standard libraries  (like, say, clojure.lang.IFn, java.lang.List etc). This removes the compilation cross-dependencies between modules, while still providing enough static type information to be practically useful (i.e. checking you aren't passing a String when the parameter should have been a List of characters.....)

[Mars0i]

I came to this thread late, and have only skimmed some of the answers, but I think that the following, somewhat oblique, opinion hasn't yet been expressed about the, I don't know, maybe ... harassment by "type weenies" that zcaudate feels.  Apologies in advance if I've missed a similar point.

First, I'll note that I agree with many of the comments so far.  To everything there's a season.  That goes for type systems.

In what I say next, I'm not trying to offend anyone.  I'm expressing half-baked opinions about what I feel are general tendencies.  I am certain that there are exceptions to every generalization I make.

My personal opinion:

Many of us who like programming like it partly because we like order, systematicity, and elegance, at least in our thinking.  We like things to make sense.  Some people have a greater need for this than others, at least at certain stages of their life.  So things that seem more clean and neat are attractive.   Full-fledged static typing has this character.  It's appealing because it's orderly in a very, well, strict sense.  I think it's probably easier to be religious about static typing and provable correctness as a universal goal if you don't have to deal with a lot of pragmatic concerns.  So I suspect that many type zealots are students or were recently, and that they'll end up lightening up in several years, after they've got more experience with meeting the demands of practical coding.  (That's not to imply they'll necessarily give up affection for static typing, but it's hard to be a zealot after you've freely chosen, many times, to compromise on formerly rigid principles.)  Dynamical languages are above all oriented toward practical programming needs in certain contexts--in other contexts, static typing is more practical.  Maybe some of the hard core static type advocates will see the potential benefits dynamic typing when they get more experience.  But you can't prove, mathematically, that dynamical typing is better sometimes.  Its advantage comes out in actual practice in real-world situations.  ("Real world" doesn't mean business.  I'm an academic coding solely for research purposes (and fun!).)

My 2c.

[Mark Hamstra]

Dynamical languages are above all oriented toward practical programming needs in certain contexts--in other contexts, static typing is more practical.

Agreed -- which is why I find your speculation about "lightening up" with "more experience ... meeting the demands of practical coding" to be unsound.  For those of us whose "practical programming" context includes a high cost associated with most any runtime bug, greater embrace of static typing, not "lightening up", comes with more practical experience.  I can be happy using a dynamically typed language when the price to be paid for getting it wrong isn't as high; but all of my experience goes against "lightening up" in the demanding programming context where I work every day.

[Michael Swierczek]

>
> Agreed -- which is why I find your speculation about "lightening up" with
> "more experience ... meeting the demands of practical coding" to be unsound.
> For those of us whose "practical programming" context includes a high cost
> associated with most any runtime bug, greater embrace of static typing, not
> "lightening up", comes with more practical experience. I can be happy using
> a dynamically typed language when the price to be paid for getting it wrong
> isn't as high; but all of my experience goes against "lightening up" in the
> demanding programming context where I work every day

We're arguing in circles. I think the fundamental question is between
two issues. On the potential drawback of strong static types, you
have trying to model all of the complex interlocking concepts in a
static type system and possibly dealing with long compile times. On
the potential drawback of dynamic typing, you have the risk of a
runtime type error. The question, then, is whether the flexibility of
dynamic types lets you develop, test, unit test, and system test code
so much faster than you would in a language with strong static types
that you are able to prevent all runtime type errors anyway.

The difficulty in deciding the question is that the benefits and
drawbacks of either approach don't really manifest until your project
is huge. It's relatively straightforward to get your dynamic typing
right in a 500 line program, and it's relatively straightforward to
not have any issues modeling your logic and data with static types in
a 500 line program, and the speed difference in development between
the two isn't significant. Once you get to hundreds of thousands of
lines of code, things get interesting - and it also gets much harder
to compare between the two.

If you look at Youtube, Reddit, Twitter, Github, Tumblr, and Facebook,
they were written in languages with dynamic types. A lot of them
switched partly or totally to languages with static types for
performance reasons once they got big enough. But I really think they
stand as testimonial to the fact that dynamic types allow for faster
development than static types. If you're guiding a rocket or
controlling medical equipment, stay static. But for other use cases,
that's a pretty compelling case.

-Mike

[Mars0i]

I don't think we disagree.  The guesses I gave in my post only concerned people like those who frustrated zcaudate, and who, from what was said, seemed to feel that anything other than strict static typing was wrong in all contexts.  Maybe I'm reading too much into zcaudate's post, though.

(Also, so no one will misunderstand, when I said "'real world' doesn't mean business", I of course meant not just business.  A lot of my programming experience was in the business world, actually.)

[Chris Zheng]

@Richard. I would have said the same as you before I joined a relatively large organisation heavily influenced by scala and the Coursera FP lecture series. We are slowly moving into Clojure code but there now seems to be a huge misconception that FP and Type Systems are joined at the hips.

My conversations with one or two scala fanboys goes something like this:

Them: "What's so good about clojure anyways? I'm really worried that it's going to fail in large projects."

Me: "Well.. Here is a large project. Check out this macro I wrote. it abstracts out all these underlying complexities and it would be really hard to this write the code with a type system."

Them: "But you need types because types are mathematically provable... You can't write correct programs if you don't have types."

 

After a couple of these conversations.  I find it useful to avoid them. However, when push comes to shove, I have a list of examples where having type systems are not natural to solving the underlying problem - modelling relationships, querying databases, translating JSON, classifying elements in non-treelike structures, dealing with change in specifications, dealing with uncertainty in specifications... All very 'real world' problems that are an unnatural fit with the type system.

In those examples - there are ways of wrangling the type system to deal with the problems, but they end up using an existential type - http://www.haskell.org/haskellwiki/Existential_type , or a type of types - http://ktoso.github.io/scala-types-of-types, or something meta like template haskell. It seems quite silly to have the 'any' type when it is probably best to not use types at all. Doesn't this remind you of the story of 'the emperor's new clothes'?

I completely agree with Korny that types are a premature optimisation. Therefore understand why and how it is a premature optimisation is really important to convince organisations to firstly understand, trust and then use clojure in production. Sometimes, writing good programs and having good use cases are not enough. We don't need a complete mathematical proof, but we still need something to substantiate design decisions to those that may not be as clojure friendly.

----

--
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@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+u...@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+u...@googlegroups.com.

[Ben Wolfson]

I'm not sure what you mean by invoking the putative silliness of an "any" type, but existential types aren't just a way of saying "anything goes here, typewise"---they do enable further substantive static guarantees (such as those used by e.g. Haskell's ST system).

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+u...@googlegroups.com.

For more options, visit https://groups.google.com/groups/opt_out.

--
Ben Wolfson
"Human kind has used its intelligence to vary the flavour of drinks, which may be sweet, aromatic, fermented or spirit-based. ... Family and social life also offer numerous other occasions to consume drinks for pleasure." [Larousse, "Drink" entry]

[Angel Java Lopez]

About:

" The question, then, is whether the flexibility of
dynamic types lets you develop, test, unit test, and system test code
so much faster than you would in a language with strong static types
that you are able to prevent all runtime type errors anyway."

Yes! In the past years, I coded in typed languages (Java, C#), and in dynamic language (JavaScript). And dynamic language (using TDD) is faster and more solid, in my experience.

The key part is TDD: it is the new compiler. It catch the errors, but not the type errors, but the behavior errors. And to me, this feature is more important.

I only would switch to typed language for efficiency reasons, or some specialized domain.

[Chris Zheng]

@mars0i That is how I feel. Of course static typing has its use. For starters, it makes my programs go faster. 

However, the more i write lisp code, the more i realise that types has its drawbacks. I'm not sure of the answer here but I have my suspicions: Can typed clojure be written in typed clojure? 

Anyways... the caption of this thread is slightly misleading... it was a bit of an attention seeking title :)

--
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@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+u...@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+u...@googlegroups.com.

[Ben Wolfson]

On Mon, Dec 23, 2013 at 2:34 PM, Chris Zheng <z...@caudate.me> wrote:

However, the more i write lisp code, the more i realise that types has its drawbacks. I'm not sure of the answer here but I have my suspicions: Can typed clojure be written in typed clojure? 

Why in the world couldn't it be? At the most boring level, if there were some difficulty, one could just project everything into some universal type, then do case analysis based on what sort of thing you had. (Which is the nub of Bob Harper's claim that "dynamically typed" languages are just a special case of statically typed languages, if I understand it.)

[Rich Morin]

On Dec 23, 2013, at 14:16, Chris Zheng wrote:
> I completely agree with Korny that types are a premature optimisation.

My take is that required types may force premature optimization and may
inhibit the creative process. So, I like dynamic languages. However,
optional types (preferably with type inference) give me the choice to
add typing if, when, and how I think it will be worthwhile. So, I may
still premature, but at least it's my mistake to make...

Any time that a function is going to be distributed beyond its initial
project, I would assert that appropriate forms of typing (eg, schema,
Typed Clojure) should be evaluated (and probably used).

Going a bit further, I'd like to assert that every publicly-distributed
function (etc) in the Clojure ecosystem should have appropriate use of
typing. This should be integrated into the online documentation and
testing support, to make it readily and usefully available. And a pony.

-r

--
http://www.cfcl.com/rdm Rich Morin r...@cfcl.com
http://www.cfcl.com/rdm/resume San Bruno, CA, USA +1 650-873-7841

Software system design, development, and documentation

[Mars0i]

On Monday, December 23, 2013 5:39:54 PM UTC-6, Rich Morin wrote:

My take is that required types may force premature optimization and may
inhibit the creative process.

That's an interesting point.  I like it.  Kind of off topic, but my earlier remark about psychological factors that might contribute to static type zealotry made me think about one static type fan (zealot, maybe) I knew who, I think, at one time endeavored to avoid thought processes that couldn't be made rigorous.  I keep thinking I should have said that I think creativity often requires a intermediate stage of messiness.  Then you have to clean it up to get something interesting, in many cases, but you wouldn't have gotten to some place new and interesting if you only went via purely rational, rigorous steps.

Maybe this is the argument that zcaudate should use: Static typing is the death of creativity.

Just kidding.

[Chris Zheng]

 Can typed clojure be written in typed clojure? 

 could just project everything into some universal type, then do case analysis based on what sort of thing you had. (Which is the nub of Bob Harper's claim that "dynamically typed" languages are just a special case of statically typed languages, if I understand it.)

I'm confused... was that supposed to be taken seriously? It was very dry if it was meant to be a joke :-)

[Rich Morin]

On Dec 23, 2013, at 16:03, Mars0i wrote:
> ... creativity often requires a intermediate stage of messiness.

> Then you have to clean it up to get something interesting, in
> many cases, but you wouldn't have gotten to some place new and
> interesting if you only went via purely rational, rigorous steps.

If you haven't seen Bret Victor's talks on computers and creativity,
I strongly recommend doing so. The most recent one is probably the
best place to start; you can go back to the earlier ones if you get
hooked...

Media for Thinking the Unthinkable:
Designing a new medium for science and engineering
http://worrydream.com/MediaForThinkingTheUnthinkable/

[Cedric Greevey]

On Mon, Dec 23, 2013 at 7:37 PM, Rich Morin <r...@cfcl.com> wrote:

  Media for Thinking the Unthinkable:
  Designing a new medium for science and engineering
  http://worrydream.com/MediaForThinkingTheUnthinkable/

Is this available in a form that is skimmable, is greppable, is cheap for mobile users, can be perused at leisure, fits on a thumb drive, is convertible for Kindle use, and doesn't require installing and enabling notoriously insecure browser plugins to view, or is it only available as video? :(

[Rich Morin]

There is a video presentation, which could be downloaded and watched
at leisure (eg, on a smart phone). I don't think this presents any
security issues. The video is supplemented on the web page by several
interactive examples. These require use of JavaScript and probably
would look pretty cramped on a cell phone's screen.

[Chris Zheng]

Maybe this is the argument that zcaudate should use: Static typing is the death of creativity.

Just kidding.

I'm doing a short study of how hair affects language design.

http://z.caudate.me/language-hair-and-popularity/

I'd be more than happy to draw up a chart of how many hours a person has spent proselytising static typed languages versus how many real world problem they have solved (although we may have to think this matrix because it is unclear to me how to get the data. I was thinking lines of code, but then java devs would win hands down).

[Cedric Greevey]

On Tue, Dec 24, 2013 at 12:23 PM, Rich Morin <r...@cfcl.com> wrote:

On Dec 24, 2013, at 02:09, Cedric Greevey wrote:
> On Mon, Dec 23, 2013 at 7:37 PM, Rich Morin <r...@cfcl.com> wrote:
>   Media for Thinking the Unthinkable:
>   Designing a new medium for science and engineering
>   http://worrydream.com/MediaForThinkingTheUnthinkable/
>
> Is this available in a form that is skimmable, is greppable, is cheap for mobile users, can be perused at leisure, fits on a thumb drive, is convertible for Kindle use, and doesn't require installing and enabling notoriously insecure browser plugins to view, or is it only available as video? :(

There is a video presentation, which could be downloaded and watched
at leisure (eg, on a smart phone).  I don't think this presents any
security issues.

Oh, I don't doubt that the *video* doesn't present any security issues. It's the Flash plugin needed to watch it that presents security issues.