[jeremiep]

Theres the new clojure.spec[1] in 1.9 and core.typed[2] adds an optional type system as well.

[1]: http://clojure.org/about/spec [1]: https://github.com/clojure/core.typed

The REPL-driven development of Lisps makes types not as important because everything is interactively tested as you write it. Having an optional type system makes it much easier to start with dynamic types and gradually add type annotations as your architecture stabilizes.

[yogthos]

Conversely, lack of mutability makes dynamic typing much easier to reason about. Since variables typically can't be changed via side effects, you can do local reasoning about your code vast majority of the time.

[rkrzr]

> Conversely, lack of mutability makes dynamic typing much easier to reason about.

Dynamic typing does not imply lack of mutability. Those are unrelated concepts.

Python and Ruby are dynamically typed but both are certainly mutable.

Conversely static typing actually makes it easier to reason (locally or not) about things, since you always know the type of everything.

[jeremiep]

I think he meant it in the context of Clojure, which has immutable values.

I don't feel static typing makes it easier to reason about, at all. Reasoning about values and their transformations is more important to me than reasoning about types, and since values carry types you're actually working with more information. Most of the time the types I'm interested in are closer to concepts (sequences, mappings) than concrete classes.

Thats where having immutable dynamically typed values is better than having statically typed mutable ones.

[rkrzr]

> since values carry types you're actually working with more information.

Only for the specific value that you are reasoning about. If you want to reason about all possible values, then you are de-facto reasoning about their types.

> Most of the time the types I'm interested in are closer to concepts (sequences, mappings) than concrete classes.

But sequences and mapping are also types, right? You can abstract types to type classes (i.e. whole classes of types, e.g. all types that can be iterated over, or all types that are ordered etc.) and also reason about them.

> Thats where having immutable dynamically typed values is better than having statically typed mutable ones.

Sure, ideally you want to have immutable statically typed functions and values, since you can then do some equational reasoning and prove certain properties of your program.

[jeremiep]

> If you want to reason about all possible values, then you are de-facto reasoning about their types.

True, but a variable can only ever have one value at any given time; knowing a variable is an int is good, knowing a variable is the same int value throughout its extent is better :)

> But sequences and mapping are also types, right?

Yes, but they're not concrete types and don't map to a single interface either. When they do these interfaces are compositions of smaller interfaces anyways and I prefer to reason about these smaller parts.

Which means I'm reasoning more about the shape of the data than the actual type implementing it, and that to me is closer to a value than a type. Its the same with type-classes, you're reasoning about the features of a value rather than the specific type implementing said features.

> ideally you want to have immutable statically typed functions and values

For functions we're talking about purity rather than immutability (which qualifies variables). Type systems also are very leaky abstractions; null pointer exceptions, can't limit the range of value, requiring more code which introduces its own bugs and complexity and more.

From experience I prefer a smaller dynamically typed codebase that has tests for the trickier parts over a statically typed codebase (even if tested). The productivity difference is startling and the resulting quality is about the same.

[yawaramin]

> ... I'm reasoning more about the shape of the data than the actual type implementing it, and that to me is closer to a value than a type.

The shape of the data is its type. You have been reasoning about types all this time. Check out https://en.wikipedia.org/wiki/Structural_type_system

[yogthos]

I never said dynamic typing implied lack of mutability. What I meant is that Clojure defaults to immutability, so reasoning about types becomes easier than in a language with mutable data.

In a language like Ruby or Python, it's possible for a side effect to change the type of the variable you're looking at externally. This cannot happen when you're writing idiomatic Clojure.

Static typing comes at a cost however. You have to figure out how to encode the problem using types. Effectively, you have to prove to the compiler that your code is self-consistent. Proving something is often much harder than stating it.

At the same time, static typing doesn't guarantee semantic correctness. So, it doesn't actually tell you that your code is correct in any meaningful sense.

I think that Clojure Spec packaged with the 1.9 release, provides a much better way to catch errors than types. The main reason being that it focuses on ensuring semantic correctness.

For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they're in order. This is difficult to express using most type systems out there. However, with Spec I can just write:

    (s/def ::sortable (s/coll-of number?))

    (s/def ::sorted #(or (empty? %) (apply <= %)))

    (s/fdef mysort
            :args (s/cat :s ::sortable)
            :ret  ::sorted
            :fn   (fn [{:keys [args ret]}]
                    (and (= (count ret)
                            (-> args :s count))
                         (empty?
                          (difference
                           (-> args :s set)
                           (set ret))))))

The specification will check that the arguments follow the expected pattern, and that the result is sorted, and I can do an arbitrary runtime check using the arguments and the result. In this case it can verify that the returned items match the input.

[yawaramin]

> ... you have to prove to the compiler that your code is self-consistent. Proving something is often much harder than stating it.

Not really. When you learn the properties of your type system, you can 'prove' your way through most day-to-day programming tasks fairly easily. And when you can't prove something to the compiler, you can just fall back to telling it using its 'dynamic' escape hatch. You're certainly no worse off than you are with pure dynamic typing.

> ... Clojure Spec ... focuses on ensuring semantic correctness.

Nothing in a static type system precludes something like Clojure Spec, or at least something very much like it. You can still fall back to runtime tests that your function works according to spec. In fact that's what Haskell's QuickCheck and related generative testing systems are all about.

[groovy2shoes]

Indeed, they are distinct concepts. However, in Clojure, only a small handful of datatypes allow mutation (sorta like refs in ML, but thread-safe and with various semantics depending on how that thread-safety should be handled). All of the usual datatypes are immutable (lists, vectors, hashmaps, sets, strings, etc.). If you need mutation, you need to wrap your object up in a "mutable box".

[mindcrash]

Typed data was already possible with schema [1], which is now maintained by the plumatic (former prismatic) team. Which also says something about the way Clojure is awesome. Everything is optional, you arent forced to use anything to get to a working solution. Stuart Halloway and Rich Hickey also have some great talks on this subject. If you are interested you might want to check out "Radical Simplicity" [1] by Stuart and "Simple Made Easy" [2] by Rich to see why Clojure wipes the floor with almost any other programming language, especially the likes of C# and Java.

I am not surprised at all Bob Martin loves it. Any principled software engineer would.

[1] https://skillsmatter.com/skillscasts/2302-radical-simplicity

[2] https://www.infoq.com/presentations/Simple-Made-Easy