https://github.com/rikusalminen/funfun/blob/master/FunFun/Ty...
This was also the first time I used monad transformers and almost the first non-IO monad application (I've used ST and Parsec before) I have dealt with. If you compare my code with the book source (Peter Hancock's type checker in Peyton-Jones' "Implementation of Functional Programming Languages", link in source code comment), my version using monads is a lot simpler to follow than the original, written in a pre-Haskell functional programming language called Miranda with no monads.
The type checker is a "pure function", it has inputs and outputs but no side-effects but in the code you need to 1) generate unique "names" 2) bail out early on type errors. I solved this problem using Error and State monads. The Miranda code used an infinite list of numbers for unique names and cumbersome tricks to handle type errors.
I think in this subset you're mentioning?
Typing preferences are usually due to trends in language usage having little to do with knowledge.
Plenty of java programmers use static typing without ever having to understand type theory.
But looking to history of language designers/implementers
Dan Friedman
Gilad Bracha http://www.infoq.com/presentations/functional-pros-cons
Guy Steele
Rich Hickey
All of these guys have worked on static languages, have a keener understanding of type theory than most, and yet they seem to promote dynamic languages at least when it comes to their pet languages.
Rich hasn't worked on static languages and I'm not familiar with him having done anything in type theory. He wanted a nicer, practical Lisp first and foremost. A helpful compiler wasn't high on his list of priorities.
Guy Steele's most recent work has involved functional, statically typed programming languages: http://en.wikipedia.org/wiki/Fortress_(programming_language)
One of Friedman's most recent books http://www.ccs.neu.edu/home/matthias/BTML/ was on ML which is a statically typed, functional programming language.
The smart people that weren't using static types back in the 70s and 80s weren't using them because the statically typed languages available back then were fuckin' awful except for ML and Miranda.
We can do a lot better as programmers these days. Stop giving yourself an excuse to not learn new things.
ghc compiler in Haskell has -fdefer-type-errors flag. SBCL Common Lisp implementation has option to turn type warnings into errors. Extending -fdefer-type-errors function and creating better type checker for dynamic languages could achieve best of both worlds.
Some things like overloading based on return values don't work dynamically, but you could either choose to not have them or resolve them in development time. I would like to see languages where dynamic vs. static is continuum and programmers can determine how much they need want case by case basis.
It's relatively easy to do this statically compared to bringing the benefits of Haskell to a unityped language. We just don't program in languages designed around dependent types typically.
Dependent types aren't hard.
Agda, Idris, Coq for any who are curious as to what that looks like.
Total functional programming is cool ^_^
For a language that truly hass optional static types see Shen[1]
This is due to Haskell's support for partial functions. It does induce some weakness in the type system but it brings the benefit of making the language Turing-complete. As for these specific examples, they would be solved if the libraries in question were rewritten.
The issue is, outside of languages with very baroque type systems or monstrosities like Java's sandbox, static typing often winds up decaying into weak typing, which offer much weaker behavior guarantees than real-world dynamic languages.
Runtime checks are not type checks[0], they are class checks.
[0]. https://existentialtype.wordpress.com/?s=dynamic+typing
[1] http://pleiad.dcc.uchile.cl/papers/2012/kleinschmagerAl-icpc... - maintainability
[2] http://dl.acm.org/citation.cfm?id=2047861&CFID=399382397&CFT... - development time
[3] https://courses.cs.washington.edu/courses/cse590n/10au/hanen... - development time, take 2
[4] http://pleiad.dcc.uchile.cl/papers/2012/mayerAl-oopsla2012.p... - usability
To joke and exaggerate a little, those studies seem to be done by people who belong to the "proponents of dynamic typing" and not "familiar with type theory" bin of people in the Venn diagram in the OP.
Did this a little while ago (as a stepping stone to building an inference system for a more complicated calculus).
E.g. you have a function f that takes two arguments, x and y. If the function is truly curried, then (f x y) is a full function call of f that returns a value, while (f x) returns a function of one argument, as if you had used partial. You could create a (two-argument) currying helper-function with the following:
(defn curry-2 [f]
(fn ([x] (partial f x))
([x y] (f x y))))
The reason this isn't more pervasive is because it doesn't play well with optional parameters, &rest parameters, arity overloading, or other ways in which the number of arguments to a function might vary (Haskell permits currying by not allowing variable param lists). Clojure has a couple of library functions that use this pattern (notably, the reducer library), but it's not ubiquitous.
Consider a "+" operator that does currying:
((+ 5) 10)
(5 10)
((partial + 5) 10)It depends on what you're doing. If you're building cathedrals-- high-quality, performance-critical software that can never fail-- then static typing is a great tool, because it can do things that are very hard to do with unit testing, and you only pay the costs once in compilation. There are plenty of use cases in which I'd want to be using a statically typed language like OCaml (or, possibly, Rust).
If you're out in the bazaar-- say, building a web app that will have to contend with constant API changes and shifting needs, or building distributed systems designed to last decades without total failure (that may, like the Ship of Theseus, have all parts replaced) despite constant environmental change-- then dynamic typing often wins.
What I like about Clojure is that, being such a powerful language, you can get contracts and types and schemas but aren't bound to them. I like static typing in many ways, but Scala left me asking the question, any time someone insists that static typing is necessary: which static type system?
I would go so far as to say one of the most evil things a person can do when designing an API for statically typed languages is using the equivalent of System.Object unnecessarily.
Now I relegate dynamic languages to writing single file scripts or less.
I use Clojure at work and the single biggest drain on my productivity is a lack of a sensible, static type system. Yearn for Haskell big time.
I'd use Rust if I had to really get down and dirty, otherwise Haskell would be my first choice. OCaml isn't that great at all in practice.
I fully agree that if you're working on a large project, you'll need something that is "type-like" in terms of enforcing interface integrity. Where there's an open question is how necessary compile-time typing is for most problems. (Few would disagree with the claim that types are a good thing.)
Clojure (esp. without types) seems to favor smaller projects (libraries over frameworks) and modularity in the extreme, almost implicitly. When you get "into the large" and need checks like types or contracts, there are various libraries that are available.
I like Haskell a lot, but my experience going between the dynamic and static styles of programming and languages (these things are as much about coding style as the language itself, which is why Scala can be beautiful or horrid depending on how it is used) is that the grass often seems greener on the other side. Haskell's great in many ways, and designed by some of the most brilliant computer scientists and logicians alive right now, but it's not without some painful warts (although my knowledge is 3-4 years out of date).
Google "Theorems for free". One of the most life-altering CS papers I've read. :-)