16 ms·

Clojure vs. The Static Typing World

83 points by keymone 9y ago

keymone 9y ago
it's interesting that the article never mentions clojure.spec nor fully-qualified keywords in clojure maps. imo without those the argument (to anyone outside Clojure world) appears to be "lets just use open maps for everything", which is not really conveying the larger point - that one can have reasonable structure and description/enforcement of that structure using predicate language, which to some extent can be applied during compile time and enables static analysis tools. it's a compromise between rigidity of haskelly type system and the wild-west of tossing open maps around.
throwawayjava 9y ago
With apologies to the author, the piece was very well-written but I didn't find any of the arguments or observations in this article comepelling :-( > This is just a guess, but at the time he wrote Clojure, those type systems most likely were Java-style (Java, C++, C#) and Haskell SML and OCaml pre-date some of the languages in that list, and certainly pre-date clojure. The "positional semantics" section -- and that whole class of arguments -- never made any sense to me. All languages have hash maps, so this is about program design rather than language design. Or perhaps, at most, an argument for having nice syntactic sugar for hash maps. In any case, I'm not sure what this has to do with fundamental language design issues. The "can Haskell..." stuff has a similar smell to it. The answer is always "yes, Haskell (and everyone else) have hash maps and HOFs." At best, it's an argument that those languages should provide a bit of extra syntax around the "everything is a map" programming style. Which, I won't disagree with :) > In the kinds of systems Rich is talking about, any data could possibly be missing... At the limit, you would need to make everything Maybe Which is why ML-family languages have both exceptions and algebraic data types. The discussion of abstraction is just confusing. The author seems to define "abstraction" as "literally any list of information". And I guess it's true that pathologically bad abstractions do exist, but... what point is being made here? I don't get it. The "screwing around in the type system syndrome" thing actually makes sense, but you can see the same thing in dynamic languages (e.g., with meta-object protocols or macros). There's something more fundamental here, and it's more about human psychology than language design. I have to agree with keymone, though, that the really interesting thing about clojure is not its design but rather clojure.spec. Sure, you lose a lot of static guarantees, and along with them some of the maintainability/correctness that come along with statically typed languages. But perhaps recovering static checks, and tooling based on static checks, is best done on a library-by-library basis via compositional specification checkers specialized to the particular library. Rather than by a single general-purpose type theory that's rich enough for the "real problems in the messy world" type of programming. And the article kinda starts hinting at this toward the end. But I think keymone really hits the nail on the head when it comes to what you should take away from learning/working in clojure.
- platz 9y ago
  > The "can Haskell..." stuff has a similar smell to it. The answer is always "yes, Haskell (and everyone else) have hash maps and HOFs." +1 ! If necessary you don't need to use and ADT+pattern matching on JSON. You just work with the hashmap directly.
  - keymone 9y ago
    What is the type signature for json hashmap in Haskell and how using it is different from using a dynamically typed language?
    - chowells 9y ago
      The easiest way to use JSON as dynamically typed data in Haskell is with the lens[1] and lens-aeson[2] packages. The type signatures those use are astounding, and not trivial to understand. But the code that results is very simple while remaining strongly typed. It ends up being not that different in style from something like hpricot in ruby. [1] https://hackage.haskell.org/package/lens https://hackage.haskell.org/package/lens [2] https://hackage.haskell.org/package/lens-aeson https://hackage.haskell.org/package/lens-aeson
    - platz 9y ago
      A json object has the type signature: type Object = HashMap Text Value which is A JSON "object" (key/value map). The keys of the hashmap are Text and the leaves are "Value" which contain more JSON here are different well-formed json values that both resolve to the same type, A.Object (either you get a parse error String for not-well-formed json, or an A.Object) >>> A.eitherDecode "{ \"name\": \"Joe\", \"age\": 12 }" :: Either String A.Object Right (fromList [("age",Number 12.0),("name",String "Joe")]) >>> A.eitherDecode "{ \"name\": \"Joe\", \"age\": {\"foo\": \"12\"} }" :: Either String A.Object Right (fromList [("age",Object (fromList [("foo",String "12")])),("name",String "Joe")]) Then you can access values in the HashMap by key just like a hashmap in any other language. Or, as noted by chowells, you can use lens-aeson which can be thought of as a DSL to perform queries in a dynamic fashion: retrieve value of "foo" in "age" >>> s = "{ \"name\": \"Joe\", \"age\": {\"foo\": \"12\"} }" :: String >>> s ^? key "age" . key "foo" Just (String "12")
Verdex_3 9y ago
The thing about static typing is that there's a lot of research behind it and it's getting better every day. Eventually it will get to the point where it's nearly almost the same as dynamically typed systems, but with type checking (but today is definitely not that day). Checkout liquid types [1]. It's a way to get type inference with nearly dependent types. Cool stuff. Dynamically typed languages, on the other hand, don't really have that much more research that can even be done with them. Can't do any more research on the type system because there isn't much of one. Really the only thing you can do is introduce language features that are difficult to type in a static system, but at that point you're just giving more theory CS phd students targets of things to find a novel way to type. That being said, the problem with static type systems is that there is a lot of details that you need to figure out to A) be able to use it and B) be able to avoid the edge cases. You'll eventually need to learn about type theory ... which isn't just one thing. Agda and Idris have incompatible definitions of equality and that has an impact. Are your dependent types intensional or extensional? It matters. And that's just the theory side. Two different type systems with the same theory might have different implementation details that impact the programmer. Are you using ML? Is that an applicative functor or a generative functor? Hey, you're using first class modules, cool. Btw you can't use that with applicative functors, don't ask why it has something to do with complicated type theory stuff that took people years to figure out. Using haskell? Is it GHC or is it some alternative ... because that impacts some type class definitions that are possible. Eventually the static types are going to win because we'll slowly figure out how to type everything (well, nearly everything) and we'll slowly figure out how to package that power in a way that everybody can understand. However, in the mean time there is a very real cost to having to learn any given static type system that doesn't exist if you live in a dynamically typed system. Additionally, if you do understand some type theory you can bring over the lessons learned to your dynamic system. You won't get type checks at compile time, but you will get a more disciplined way to produce code. [1] - http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=029D52B462162562BA423FE3B7A3A37B?doi=10.1.1.205.2089&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=029...
- throwawayjava 9y ago
  I'm not sure I agree that "eventually the static types are going to win". The problem is that a lot of program specifications are possible and even economical to write down, but not at all interesting from a research perspective. I do agree that "eventually statically checked specifications are going to win", but I'm not sold that those specifications will take the form of (something easily recognizable as) a type theory. (However, neither outcome would surprise me).
GreaterFool 9y ago
This post is seriously misguided. > The tools Haskell gives you are great at some things, but dealing with arbitrarily nested ADTs is not one of them. There's nothing more natural in Haskell than recursion and processing of ADTs. There are dozens incredibly well-research patterns for processing just about anything under the sun. > What we wound up doing was nesting pattern matching to get at the value we wanted. The deeper the JSON nesting, the deeper our pattern matching. In my experience that works great for moderately complicated and ugly JSON messages. Tried that in Haskell, OCaml and Rust. Rust was most clunky due to the way things are represented in serde (I expect that's more performant though) but still worked nicely. Alternatively, lenses would allow for incredibly easy access to just about anywhere in any JSON document. Want to hit multiple nested targets in weird locations? No problem! > But imagine if more and more of your code is dealing with JSON. It would be nice if there were some easier way. Sadly the author skipped explaining that mythical "easier way".
- thedufer 9y ago
  > There's nothing more natural in Haskell than recursion and processing of ADTs. There are dozens incredibly well-research patterns for processing just about anything under the sun. MLs are widely cited as some of the best languages for implementing compilers in, and large chunks of a compiler consist of transforming various ASTs. An AST being a particularly complex recursive ADT, it seems strange to claim that's a weak point of statically-typed languages.
  - emeraldd 9y ago
    The weak point he's highlighting isn't in processing the ADT itself. The problem is that there's a loss of semantic meaning about the information stored in the ADT. i.e. The ADT itself cannot dictate that the semantic structure of the information it stores is correct even though it may represent a well formed "Document"
    - GreaterFool 9y ago
      Clearly the best way to store a document is a blob of text!
m12k 9y ago
> I sometimes wish I could tighten down some Clojure code with static type guarantees. These are in small, remote portions of the code that have intricate algorithms. Static types would be very useful there. But that's the exception. In general, I like the flexible information model approach of Clojure better than the statically-typed approach of Haskell. I feel the opposite way. I find a dynamic approach useful in some places, but in most places I miss having static typing to help catch errors faster and give my IDE better auto-completions and make exploring new APIs faster without constantly needing to look things up. And rather than small intricate algorithms, I find the most important place for static typing to be when making big refactorings that span the whole codebase. I think my ideal language would have static typing by default but you could disable it in places.
- kochthesecond 9y ago
  My sentiment as well. Local segments with dynamic typing could be nice, but especially along api borders I want static typing. In most cases static type inference would be enough, I generally don't feel the need for dynamic typing then.
  - emidln 9y ago
    I've been writing Clojure for several years with ^:always-validate'd Schemas at the API boundaries in for library boundaries and compojure-api enforcing the Schemas for input passed in via http or queues (via constructing a ring map out of an input queue and turning a ring response map into a response on a different queue). My tooling (emacs/Spacemacs) has good support for introspection/autocompletion/automatic doc popups/testing and I also get cheap to free generative testing via test.check. The water is nice, you should jump on in.
  - mamcx 9y ago
    My sweet spot is local type inference (inside functions, methods) and explicit type annotations (for types, parameters, etc), and a way to have a dynamic type with low ceremony, like just sugar over a hasmap....
- weavie 9y ago
lkrubner 9y ago
Here is a long excerpt from Professor Mark Taver (inventor of the Qi/Shen language), which I think sums up both sides of the argument nicely: -------------------------------- (quote from someone named Racketnoob) “I have the strange feeling that types hamper a programmer’s creativity.” The above sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages — that they are losing something, a degree of freedom that the writer identifies as hampering creativity. Is this true? I will argue, to a degree — yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel’s incompleteness proof, is that the human ability to recognize truth transcends our ability to capture it formally. In computing terms our ability to recognize something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work. That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding. The invitation of adding types was thus taken up by myself, and the journey to making this program type secure in Shen emphasizes the conclusion in this paragraph.http://www.shenlanguage.org/library/shenpaper.pdf http://www.shenlanguage.org/library/shenpaper.pdf
- emidln 9y ago
  The allure of Shen is that it offers a type system that is, roughly speaking, very similar to what you get with clojure.spec. You construct "predicates", what Shen calls sequents, which hold about your data. Shen goes a step further than clojure.spec in that it offers a way to prove that those predicates hold locally to each function and globally through your program. I wonder if it might be possible to feed predicates from clojure.spec to the inference engine/type checker from the Shen java port to gain static type checking. I wish I had more time to work on this kind of fundamental research, but alas I'm merely a working programmer schlepping data to and fro.
wellpast 9y ago
This post seems to miss the fact that in Rich's talk he rails on ADTs even more than he does on static typing. Rich's biggest complaint is that our tools should be a la carte not forced down our throat at every turn. Type verification (static or not) should be a tool, not a religion. (In this way, Rich renders the perennial static vs. dynamic debate stupid: it's a false dichotomy that most statically typed languages needlessly force us into.) In Rich's talk, the bigger target of his attack is ADTs -- that is, processing information in any way that doesn't make properties first-class. (It's easy to mix up his argument against ADTs and static types, probably because ADTs are kind of like the go-to idioms for people programming in statically typed languages.) I think one of Rich's one-trick ponies (i.e., one of his goals) is to remove the impedance between thinking and coding. We humans don't naturally think in terms of ADTs (e.g., when you open a dictionary, you see vocabulary/words, not categorical types/ADTs.) Computers only ask us to be precise and ADTs are unnecessary to achieve precision -- properties ("words") capture all of the precision needed to solve our information-processing problems. All Rich is doing is trying to remove that impedance between thinking and coding. Static types are also unnatural and unnecessary to the precise expression/coding of solutions to our "situated" programming problems. I don't think any static typing enthusiast would disagree. What the static typer would say, though, is that they've done something clever: they're adding the extra impedance of type verification to achieve a higher level of problem-solving throughput. (Because their static types reduce other impedances: bugs, refactoring ease, etc.) Are the static typers right? Rich seems to imply no. (Because even though he says typing should be a la carte, you can clearly see in the talk that he has his predilection.) The fight here is usually left to our intuitions and habit, but my guess is that someone smarter than me could model this programmer-productivity problem as an optimization formula, showing how over time software-construction slows down due to certain constant impedances like juggling static types and certain accumulative impedances like coupling and code quality in a large code base. My guess is that this formula would show that in low-quality code bases with lots of coupling, the static typing tax would win. But that in higher-quality codebases the static typing tax wouldn't pay for itself. This jives with my instincts of course but you also find that the better programmers (the ones that know how not to couple shit) favor dynamic typing while those that regardless of experience haven't learned how to keep coupling at bay prefer static types.
- 9y ago
taeric 9y ago
The thing that baffles me on this is the idea that static typing is limited to something only the compiler can do. If instead it was merely a form of static analysis, then it could easily be seen as something that can be added. Which, in many languages, it can be. The forms of analysis the advanced tools can give for C codebases is quite impressive. All without having to rewrite the system with more precise types. Similarly with LISP. It is widely lauded as a very popular dynamic language. However, there is nothing stopping you from statically analyzing it. Obviously some practices make this more difficult, but sometimes just having an escape hatch for the developer is enough. Just as obviously, these practices that truly make it hard to analyze statically aren't used that often. That is, a decent sized program will almost certainly use the features in a few spots. But only a few and the majority of the code can still be analyzed easily statically.
- always_good 9y ago
  > there is nothing stopping you from statically analyzing it Well, sure there is. Someone has to decide it's worthwhile to build it, then they have to build it, and polish it to a point where it's usable which generally means a community has to form around that tool. Years of work. Doesn't surprise me that people think it's more worthwhile to just use a statically-typed language.
  - taeric 9y ago
    That isn't stopping you from doing it. That is just making it more difficult. But, and this is my point, this was effort that had to happen in creating the static languages, too. Just now we locked out the benefits to existing problems to problems that are rewritten in the new languages. Contrast this with hardening existing codebases by running enhanced tooling against them.
- jahewson 9y ago
  The analysis tools for C codebases are quite impressive mostly because it’s a statically typed language which is amenable to such analysis.
todd8 9y ago
I've always felt comfortable programming in Lisp or Python, and I don't seem to miss strong typing very much. While programming Java though, with it's extensive library of functions, the more intelligent autocompletion provided by my IDE is very welcome. So I see both sides of the points being made here, but I do have a question for those HN readers that are closer to research in program correctness than I am. Why are types beleived to be so useful in insuring that programs express the intent of the programmer? It seems to me, that types are useful for useful for expressing the boundaries of components, but they seem rather awkward constructs to be wrestled with to express the invariants and predicates about the state of the program that I invariably end up using in my head to insure that my code is correct. For example, one might simply want to insure that three variables, say x, y and z, satisfy the relation (x <= y && y <= z) while inside a loop. The x, y and z might be integers or account-numbers or zip-codes or anything else with the <= predicate. What I want is not to twist the type system around to say that just while in this loop the type guarantees that (x <= y && y <= z). What I want in a programming language is to be able to express this as a claim I'm making about the program at this point and to have help from an interactive theorem prover that it is so. I'd expect some sort of dialog with my tooling that would point out where I needed to make changes to guarentee this or to indicate that it is a claim stronger than needed for the program to run correctly (and satisfy it's specifications). Type systems just don't seem very natural for this; I would think we would use something like Dijkstra's weakest-preconditions or temporal logic over program states. I really am asking for help in understanding where research on programming correctness is currently headed. (You don't have to explain it like I'm a fifth grader, I've been programming for 50 years, many in grad school.)
- christophilus 9y ago
  Clojure's spec basically provides that, but it does so at run-time while in development mode. I think Idris may have some similar capability there at compile-time. I suspect the wrangling involved to get a static type checker to precisely describe this would probably not often be worth the effort.

83 points by keymone 9y ago

it's interesting that the article never mentions clojure.spec nor fully-qualified keywords in clojure maps. imo without those the argument (to anyone outside Clojure world) appears to be "lets just use open maps for everything", which is not really conveying the larger point - that one can have reasonable structure and description/enforcement of that structure using predicate language, which to some extent can be applied during compile time and enables static analysis tools. it's a compromise between rigidity of haskelly type system and the wild-west of tossing open maps around.

throwawayjava 9y ago

With apologies to the author, the piece was very well-written but I didn't find any of the arguments or observations in this article comepelling :-( > This is just a guess, but at the time he wrote Clojure, those type systems most likely were Java-style (Java, C++, C#) and Haskell SML and OCaml pre-date some of the languages in that list, and certainly pre-date clojure. The "positional semantics" section -- and that whole class of arguments -- never made any sense to me. All languages have hash maps, so this is about program design rather than language design. Or perhaps, at most, an argument for having nice syntactic sugar for hash maps. In any case, I'm not sure what this has to do with fundamental language design issues. The "can Haskell..." stuff has a similar smell to it. The answer is always "yes, Haskell (and everyone else) have hash maps and HOFs." At best, it's an argument that those languages should provide a bit of extra syntax around the "everything is a map" programming style. Which, I won't disagree with :) > In the kinds of systems Rich is talking about, any data could possibly be missing... At the limit, you would need to make everything Maybe Which is why ML-family languages have both exceptions and algebraic data types. The discussion of abstraction is just confusing. The author seems to define "abstraction" as "literally any list of information". And I guess it's true that pathologically bad abstractions do exist, but... what point is being made here? I don't get it. The "screwing around in the type system syndrome" thing actually makes sense, but you can see the same thing in dynamic languages (e.g., with meta-object protocols or macros). There's something more fundamental here, and it's more about human psychology than language design. I have to agree with keymone, though, that the really interesting thing about clojure is not its design but rather clojure.spec. Sure, you lose a lot of static guarantees, and along with them some of the maintainability/correctness that come along with statically typed languages. But perhaps recovering static checks, and tooling based on static checks, is best done on a library-by-library basis via compositional specification checkers specialized to the particular library. Rather than by a single general-purpose type theory that's rich enough for the "real problems in the messy world" type of programming. And the article kinda starts hinting at this toward the end. But I think keymone really hits the nail on the head when it comes to what you should take away from learning/working in clojure.

platz 9y ago
> The "can Haskell..." stuff has a similar smell to it. The answer is always "yes, Haskell (and everyone else) have hash maps and HOFs." +1 ! If necessary you don't need to use and ADT+pattern matching on JSON. You just work with the hashmap directly.
- keymone 9y ago
  What is the type signature for json hashmap in Haskell and how using it is different from using a dynamically typed language?
  - chowells 9y ago
    The easiest way to use JSON as dynamically typed data in Haskell is with the lens[1] and lens-aeson[2] packages. The type signatures those use are astounding, and not trivial to understand. But the code that results is very simple while remaining strongly typed. It ends up being not that different in style from something like hpricot in ruby. [1] https://hackage.haskell.org/package/lens https://hackage.haskell.org/package/lens [2] https://hackage.haskell.org/package/lens-aeson https://hackage.haskell.org/package/lens-aeson
  - platz 9y ago
    A json object has the type signature: type Object = HashMap Text Value which is A JSON "object" (key/value map). The keys of the hashmap are Text and the leaves are "Value" which contain more JSON here are different well-formed json values that both resolve to the same type, A.Object (either you get a parse error String for not-well-formed json, or an A.Object) >>> A.eitherDecode "{ \"name\": \"Joe\", \"age\": 12 }" :: Either String A.Object Right (fromList [("age",Number 12.0),("name",String "Joe")]) >>> A.eitherDecode "{ \"name\": \"Joe\", \"age\": {\"foo\": \"12\"} }" :: Either String A.Object Right (fromList [("age",Object (fromList [("foo",String "12")])),("name",String "Joe")]) Then you can access values in the HashMap by key just like a hashmap in any other language. Or, as noted by chowells, you can use lens-aeson which can be thought of as a DSL to perform queries in a dynamic fashion: retrieve value of "foo" in "age" >>> s = "{ \"name\": \"Joe\", \"age\": {\"foo\": \"12\"} }" :: String >>> s ^? key "age" . key "foo" Just (String "12")

Verdex_3 9y ago

The thing about static typing is that there's a lot of research behind it and it's getting better every day. Eventually it will get to the point where it's nearly almost the same as dynamically typed systems, but with type checking (but today is definitely not that day). Checkout liquid types [1]. It's a way to get type inference with nearly dependent types. Cool stuff. Dynamically typed languages, on the other hand, don't really have that much more research that can even be done with them. Can't do any more research on the type system because there isn't much of one. Really the only thing you can do is introduce language features that are difficult to type in a static system, but at that point you're just giving more theory CS phd students targets of things to find a novel way to type. That being said, the problem with static type systems is that there is a lot of details that you need to figure out to A) be able to use it and B) be able to avoid the edge cases. You'll eventually need to learn about type theory ... which isn't just one thing. Agda and Idris have incompatible definitions of equality and that has an impact. Are your dependent types intensional or extensional? It matters. And that's just the theory side. Two different type systems with the same theory might have different implementation details that impact the programmer. Are you using ML? Is that an applicative functor or a generative functor? Hey, you're using first class modules, cool. Btw you can't use that with applicative functors, don't ask why it has something to do with complicated type theory stuff that took people years to figure out. Using haskell? Is it GHC or is it some alternative ... because that impacts some type class definitions that are possible. Eventually the static types are going to win because we'll slowly figure out how to type everything (well, nearly everything) and we'll slowly figure out how to package that power in a way that everybody can understand. However, in the mean time there is a very real cost to having to learn any given static type system that doesn't exist if you live in a dynamically typed system. Additionally, if you do understand some type theory you can bring over the lessons learned to your dynamic system. You won't get type checks at compile time, but you will get a more disciplined way to produce code. [1] - http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=029D52B462162562BA423FE3B7A3A37B?doi=10.1.1.205.2089&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=029...

throwawayjava 9y ago
I'm not sure I agree that "eventually the static types are going to win". The problem is that a lot of program specifications are possible and even economical to write down, but not at all interesting from a research perspective. I do agree that "eventually statically checked specifications are going to win", but I'm not sold that those specifications will take the form of (something easily recognizable as) a type theory. (However, neither outcome would surprise me).

GreaterFool 9y ago

This post is seriously misguided. > The tools Haskell gives you are great at some things, but dealing with arbitrarily nested ADTs is not one of them. There's nothing more natural in Haskell than recursion and processing of ADTs. There are dozens incredibly well-research patterns for processing just about anything under the sun. > What we wound up doing was nesting pattern matching to get at the value we wanted. The deeper the JSON nesting, the deeper our pattern matching. In my experience that works great for moderately complicated and ugly JSON messages. Tried that in Haskell, OCaml and Rust. Rust was most clunky due to the way things are represented in serde (I expect that's more performant though) but still worked nicely. Alternatively, lenses would allow for incredibly easy access to just about anywhere in any JSON document. Want to hit multiple nested targets in weird locations? No problem! > But imagine if more and more of your code is dealing with JSON. It would be nice if there were some easier way. Sadly the author skipped explaining that mythical "easier way".

thedufer 9y ago
> There's nothing more natural in Haskell than recursion and processing of ADTs. There are dozens incredibly well-research patterns for processing just about anything under the sun. MLs are widely cited as some of the best languages for implementing compilers in, and large chunks of a compiler consist of transforming various ASTs. An AST being a particularly complex recursive ADT, it seems strange to claim that's a weak point of statically-typed languages.
- emeraldd 9y ago
  The weak point he's highlighting isn't in processing the ADT itself. The problem is that there's a loss of semantic meaning about the information stored in the ADT. i.e. The ADT itself cannot dictate that the semantic structure of the information it stores is correct even though it may represent a well formed "Document"
  - GreaterFool 9y ago
    Clearly the best way to store a document is a blob of text!

m12k 9y ago

> I sometimes wish I could tighten down some Clojure code with static type guarantees. These are in small, remote portions of the code that have intricate algorithms. Static types would be very useful there. But that's the exception. In general, I like the flexible information model approach of Clojure better than the statically-typed approach of Haskell. I feel the opposite way. I find a dynamic approach useful in some places, but in most places I miss having static typing to help catch errors faster and give my IDE better auto-completions and make exploring new APIs faster without constantly needing to look things up. And rather than small intricate algorithms, I find the most important place for static typing to be when making big refactorings that span the whole codebase. I think my ideal language would have static typing by default but you could disable it in places.

kochthesecond 9y ago
My sentiment as well. Local segments with dynamic typing could be nice, but especially along api borders I want static typing. In most cases static type inference would be enough, I generally don't feel the need for dynamic typing then.
- emidln 9y ago
  I've been writing Clojure for several years with ^:always-validate'd Schemas at the API boundaries in for library boundaries and compojure-api enforcing the Schemas for input passed in via http or queues (via constructing a ring map out of an input queue and turning a ring response map into a response on a different queue). My tooling (emacs/Spacemacs) has good support for introspection/autocompletion/automatic doc popups/testing and I also get cheap to free generative testing via test.check. The water is nice, you should jump on in.
- mamcx 9y ago
  My sweet spot is local type inference (inside functions, methods) and explicit type annotations (for types, parameters, etc), and a way to have a dynamic type with low ceremony, like just sugar over a hasmap....
weavie 9y ago

lkrubner 9y ago

Here is a long excerpt from Professor Mark Taver (inventor of the Qi/Shen language), which I think sums up both sides of the argument nicely: -------------------------------- (quote from someone named Racketnoob) “I have the strange feeling that types hamper a programmer’s creativity.” The above sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages — that they are losing something, a degree of freedom that the writer identifies as hampering creativity. Is this true? I will argue, to a degree — yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel’s incompleteness proof, is that the human ability to recognize truth transcends our ability to capture it formally. In computing terms our ability to recognize something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work. That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding. The invitation of adding types was thus taken up by myself, and the journey to making this program type secure in Shen emphasizes the conclusion in this paragraph.http://www.shenlanguage.org/library/shenpaper.pdf http://www.shenlanguage.org/library/shenpaper.pdf

emidln 9y ago
The allure of Shen is that it offers a type system that is, roughly speaking, very similar to what you get with clojure.spec. You construct "predicates", what Shen calls sequents, which hold about your data. Shen goes a step further than clojure.spec in that it offers a way to prove that those predicates hold locally to each function and globally through your program. I wonder if it might be possible to feed predicates from clojure.spec to the inference engine/type checker from the Shen java port to gain static type checking. I wish I had more time to work on this kind of fundamental research, but alas I'm merely a working programmer schlepping data to and fro.

wellpast 9y ago

This post seems to miss the fact that in Rich's talk he rails on ADTs even more than he does on static typing. Rich's biggest complaint is that our tools should be a la carte not forced down our throat at every turn. Type verification (static or not) should be a tool, not a religion. (In this way, Rich renders the perennial static vs. dynamic debate stupid: it's a false dichotomy that most statically typed languages needlessly force us into.) In Rich's talk, the bigger target of his attack is ADTs -- that is, processing information in any way that doesn't make properties first-class. (It's easy to mix up his argument against ADTs and static types, probably because ADTs are kind of like the go-to idioms for people programming in statically typed languages.) I think one of Rich's one-trick ponies (i.e., one of his goals) is to remove the impedance between thinking and coding. We humans don't naturally think in terms of ADTs (e.g., when you open a dictionary, you see vocabulary/words, not categorical types/ADTs.) Computers only ask us to be precise and ADTs are unnecessary to achieve precision -- properties ("words") capture all of the precision needed to solve our information-processing problems. All Rich is doing is trying to remove that impedance between thinking and coding. Static types are also unnatural and unnecessary to the precise expression/coding of solutions to our "situated" programming problems. I don't think any static typing enthusiast would disagree. What the static typer would say, though, is that they've done something clever: they're adding the extra impedance of type verification to achieve a higher level of problem-solving throughput. (Because their static types reduce other impedances: bugs, refactoring ease, etc.) Are the static typers right? Rich seems to imply no. (Because even though he says typing should be a la carte, you can clearly see in the talk that he has his predilection.) The fight here is usually left to our intuitions and habit, but my guess is that someone smarter than me could model this programmer-productivity problem as an optimization formula, showing how over time software-construction slows down due to certain constant impedances like juggling static types and certain accumulative impedances like coupling and code quality in a large code base. My guess is that this formula would show that in low-quality code bases with lots of coupling, the static typing tax would win. But that in higher-quality codebases the static typing tax wouldn't pay for itself. This jives with my instincts of course but you also find that the better programmers (the ones that know how not to couple shit) favor dynamic typing while those that regardless of experience haven't learned how to keep coupling at bay prefer static types.

9y ago

taeric 9y ago

The thing that baffles me on this is the idea that static typing is limited to something only the compiler can do. If instead it was merely a form of static analysis, then it could easily be seen as something that can be added. Which, in many languages, it can be. The forms of analysis the advanced tools can give for C codebases is quite impressive. All without having to rewrite the system with more precise types. Similarly with LISP. It is widely lauded as a very popular dynamic language. However, there is nothing stopping you from statically analyzing it. Obviously some practices make this more difficult, but sometimes just having an escape hatch for the developer is enough. Just as obviously, these practices that truly make it hard to analyze statically aren't used that often. That is, a decent sized program will almost certainly use the features in a few spots. But only a few and the majority of the code can still be analyzed easily statically.

always_good 9y ago
> there is nothing stopping you from statically analyzing it Well, sure there is. Someone has to decide it's worthwhile to build it, then they have to build it, and polish it to a point where it's usable which generally means a community has to form around that tool. Years of work. Doesn't surprise me that people think it's more worthwhile to just use a statically-typed language.
- taeric 9y ago
  That isn't stopping you from doing it. That is just making it more difficult. But, and this is my point, this was effort that had to happen in creating the static languages, too. Just now we locked out the benefits to existing problems to problems that are rewritten in the new languages. Contrast this with hardening existing codebases by running enhanced tooling against them.
jahewson 9y ago
The analysis tools for C codebases are quite impressive mostly because it’s a statically typed language which is amenable to such analysis.

todd8 9y ago

I've always felt comfortable programming in Lisp or Python, and I don't seem to miss strong typing very much. While programming Java though, with it's extensive library of functions, the more intelligent autocompletion provided by my IDE is very welcome. So I see both sides of the points being made here, but I do have a question for those HN readers that are closer to research in program correctness than I am. Why are types beleived to be so useful in insuring that programs express the intent of the programmer? It seems to me, that types are useful for useful for expressing the boundaries of components, but they seem rather awkward constructs to be wrestled with to express the invariants and predicates about the state of the program that I invariably end up using in my head to insure that my code is correct. For example, one might simply want to insure that three variables, say x, y and z, satisfy the relation (x <= y && y <= z) while inside a loop. The x, y and z might be integers or account-numbers or zip-codes or anything else with the <= predicate. What I want is not to twist the type system around to say that just while in this loop the type guarantees that (x <= y && y <= z). What I want in a programming language is to be able to express this as a claim I'm making about the program at this point and to have help from an interactive theorem prover that it is so. I'd expect some sort of dialog with my tooling that would point out where I needed to make changes to guarentee this or to indicate that it is a claim stronger than needed for the program to run correctly (and satisfy it's specifications). Type systems just don't seem very natural for this; I would think we would use something like Dijkstra's weakest-preconditions or temporal logic over program states. I really am asking for help in understanding where research on programming correctness is currently headed. (You don't have to explain it like I'm a fifth grader, I've been programming for 50 years, many in grad school.)

christophilus 9y ago
Clojure's spec basically provides that, but it does so at run-time while in development mode. I think Idris may have some similar capability there at compile-time. I suspect the wrangling involved to get a static type checker to precisely describe this would probably not often be worth the effort.