Hindley-Milner in Clojure

http://www.lispcast.com/Hindley-Milner-in-Clojure

by ericn • 13 years ago

142 77 13 years ago

I find it curious that the venn diagram seems to indicate that a sizable subset of people who are familiar with type theory don't advocate either static typing or dynamic typing.

zephjc• 13 years ago

I think that was the joke :)

kleiba• 13 years ago

I think the joke is rather the small overlap between people who advocate dynamic typing and people who know type theory.

aidenn02• 13 years ago

I would suspect that a large fraction of them are mathematicians and not particularly interested in how people program.

octo_t• 13 years ago

I love type theory, but I think a language like Sage[1] is probably the most interesting way forward.

[1] http://sage.soe.ucsc.edu/

StefanKarpinski• 13 years ago

That's a somewhat unfortunate name to choose for a new language given the existence of this well-established system:

http://www.sagemath.org/

sfvisser3• 13 years ago

Why the 'but'? There seems to be quite some type theory involved in Sage.

ufo7• 13 years ago

I really like the idea behind Sage but I found it kind of funny that in their test cases all the ".out" files are empty because none of the programs actually do any IO. No hello-world for you :P

tel3• 13 years ago

How do you feel about dependently typed systems?

brudgers• 13 years ago

CS departments are where people exposed to Type Theory tend to be exposed to it. The sorts of languages that tend to be taken seriously in such departments [yes, I know there are exceptions] tend to be statically typed. Java and C++ just have more gravitas than Ruby and JavaScript and Lisps are for hippies.

TeeWEE• 13 years ago

I'm familiar with type theorie but i'm not a proponent of either of them. Sometimes its better to use static typing and sometimes its better to use dynamic typing. Howeover most of the times I would prefer static typing.

I think in this subset you're mentioning?

technomancy• 13 years ago

I wouldn't say I'm intimately familiar with type theory, but I'm certainly old slash grumpy enough to not be an "advocate" of anything except learning both and thinking for yourself about the problem at hand.

exDM693• 13 years ago

Here's the Hindley-Milner implementation (in Haskell) from a toy compiler project of mine. It was really enlightening to write it and surprisingly simple.

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.

sfvisser3• 13 years ago

Nice job! Seems you could have put the TypeEnv in a ReaderT as well, might make things slightly easier.

the1• 13 years ago

literate programming https://github.com/saml/lipl/blob/master/src/TCheck.lhs

moomin2• 13 years ago

As an aside, if you just want curried functions in Clojure, try poppea.

https://github.com/JulianBirch/poppea

derengel• 13 years ago

Noob question, doesn't partial provides curried functions?

brandonbloom• 13 years ago

Partial application and curried functions are subtly different.

Consider a "+" operator that does currying:

    ((+ 5) 10)

If the plus operator is not currying, that's either an arity or type error. You're either not supplying enough arguments to +, or you're trying to do this:

    (5 10)

Partial application can be explicit, without currying:

    ((partial + 5) 10)

lmkg• 13 years ago

A 'true' curried function in clojure doesn't need partial because it overloads on the arity of the function. It automatically partializes itself if it's called with too few arguments.

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

Basically with a currying function, (f x y) and ((f x) y) are equivalent calls, without the need for partial.

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.

chongli6• 13 years ago

Dynamic typing is just a special case of static typing where there is only one type!

sfvisser3• 13 years ago

Even when this is true, this special case of static typing gives you exactly none of the advantages of general static typing.

chongli6• 13 years ago

Yes, of course. I'm a big proponent of static typing, or (as Bob Harper likes to call it) typing! This is in contrast with unityped languages.

bcoates• 13 years ago

An idealized dynamic strong typed language can actually give you the guarantee that all statically valid programs give you well-defined runtime behavior. This is a huge advantage over weakly typed languages that you also get out of the idealized static typed language.

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.

dmytrish• 13 years ago

That's not quite true: there are many types, but the type checking is delayed into run time. Though your point of view may be also correct with respect to definitions (if you assume that types exist only during compile time).

chongli6• 13 years ago

That's not quite true: there are many types, but the type checking is delayed into run time.

Runtime checks are not type checks[0], they are class checks.

[0]. https://existentialtype.wordpress.com/?s=dynamic+typing

Dewie• 13 years ago

No. That sounds more like an untyped language.

ufo7• 13 years ago

While this is technically correct (the best kind of correct) it also trivializes the argument and somewhat misses the point. For example, in a dynamic language all the values are belong to a single type and carry a tag at runtime to identify their category. Static languages also do that but on more restricted scope - you aren't allowed to accidentally mix strings and integers in Haskell but you can accidentally mix empty/non-empty lists (getting a runtime exception on `head`) or zero/nonzero numbers (breaking division). You can sort of fix this if you go up to dependent types but then the type system gets much more complicated and its not always easy to statically create the proofs for everything so you start to see the appeal of dynamically checking some of the stuff.

chongli6• 13 years ago

Haskell but you can accidentally mix empty/non-empty lists (getting a runtime exception on `head`) or zero/nonzero numbers (breaking division).

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.

nabla92• 13 years ago

Why not both?

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.

emiljbs• 13 years ago

I agree. Good dynamic languages (Common Lisp, Smalltalk, Factor) has a lot going for them but static typing is also really nice. A mix between the two (preferably something that starts out as a dynamic lang and slowly moves towards being static) would be great (Common Lisp kinda does this with optional static typing).

aidenn02• 13 years ago

CL's type system has a few warts to really do static typing well.

For a language that truly hass optional static types see Shen[1]

[1] http://shenlanguage.org/

ufo7• 13 years ago

The actual reason for why not both is that its actually very hard to do and is still kind of an open problem. Some things are easy to do statically but hard to check dynamically (for example, parametric polymorphism or type-based overloading and name resolution) and some things are easy to check dynamically but hard to specify using static types (for example, array bounds checking).

nabla92• 13 years ago

You can do those things that are easy to do statically at development/testing time and those thing that are easy to do dynamically in runtime.

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.

coolsunglasses5• 13 years ago

(for example, array bounds checking)

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 ^_^

michaelochurch4• 13 years ago

I'm familiar with type theory and (often) a proponent of dynamic typing.

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?

augustl• 13 years ago

Interesting insights. Would love to read more aobut this. Usually the arguments are "I'm a bad programmer like everyone else so I need verification" or "the world is dynamic".

runT1ME• 13 years ago

The good arguments for static typing are much different than "I'm a bad programmer".

Google "Theorems for free". One of the most life-altering CS papers I've read. :-)

hesselink• 13 years ago

I've heard this argument a lot, and I disagree. If your software is changing a lot, that is where types really shine. Refactoring is a breeze when you have types: you just change the code you want to improve, and all use sites are pointed to by the compiler. This is taken from daily experience: I work on a code base that is about 25K lines of Haskell and 35K lines of Javascript. Refactoring the Haskell is a pleasure. Refactoring the Javascript is something we dread, and always introduces bugs, some of which might linger for up to a year.

Glide• 13 years ago

I've actually had this experience a couple of times on a project like upgrading a library from one release to another when APIs were updated. The compiler would often "show the way" by highlighting every mistake between version x and y.

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.

tel3• 13 years ago

I think on top of this the self-documenting properties of a nice statically typed system push back the onset of code ossification quite a lot. I always trust my type documentation while I tend to be a skeptic of documentation that's more than a few months old unless it's being actively refactored regularly.

zenbowman• 13 years ago

Exactly. A strong type system enables more rapid iteration than a weak one, just like writing unit tests. I was a fan of dynamic languages until I used Haskell and Scala, and saw how powerful types could be when they allowed you to express intention rather than getting in your way.

Now I relegate dynamic languages to writing single file scripts or less.

girvo• 13 years ago

I agree. I define empty interfaces and the types to go with them for prototyping, and it makes building my prototype so much quicker. And with a better final product, too. So IMO static (or optional/gradual) typing can even be better in that way, but only if you think in types rather than hacking away til it works.

coolsunglasses5• 13 years ago

Hum, no.

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.

michaelochurch4• 13 years ago

Have you looked into Prismatic's Schema?

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

elwell• 13 years ago

Douglas Crockford is a proponent of dynamic typing. (At least from what I read in the beginning of "JavaScript: The Good Parts)

Semiapies• 13 years ago

What's the relevance of that point? He doesn't appear to be mentioned in the post.

kd0amg2• 13 years ago

I think you should implement Hindley-Milner in the language of your choice for a small toy λ-calculus.

Did this a little while ago (as a stepping stone to building an inference system for a more complicated calculus).

https://gist.github.com/jrslepak/6158954

hardboiled• 13 years ago

Disagree about the idea that those who are unfamiliar with type theory prefer dynamic typing.

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.

rtfeldman• 13 years ago

The most useful takeaway from that graph is the insight into how many type theory aficionados look at the world.

kd0amg2• 13 years ago

FWIW, I don't think the diagram is claiming that people who are unfamiliar with type theory tend to prefer dynamic typing, rather that people who prefer dynamic typing tend to be unfamiliar with type theory.

the_af• 13 years ago

I'm not disagreeing with you (that a lot of people go with what's trendy or what they already know), but I wouldn't put Gilad Bracha in the list of knowledgeable people. I've seen the talk you are linking to and it's not very impressive... he sounds mostly whiny to me. In his own blog, when he writes about about functional programming or type theory, he gets called out by the people who really know about it.

codygman• 13 years ago

I would agree, I don't see why Gilad Bracha is on that list.

coolsunglasses5• 13 years ago

Gilad Bracha has no idea what the hell he's talking about.

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.

__--__2• 13 years ago

All this talk about formal type theory, but where are the references to the relevant studies? Where's the data? The few studies[1][2][3][4] I've found are inconclusive one way or the other and none of them focus on error rates. I found another conversation about how to go about studying error rate in dynamically vs statically typed languages, but all I really found was this article studying the affect of hair style on language design[5].

[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

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

jgg• 13 years ago

Are you trolling? I seriously can't tell...

exDM693• 13 years ago

I glanced over the studies you linked to and in all of them, the languages used as examples of static typing are Java, C and C++. There's no mention of type inference or any languages that have a more advanced static typing scheme like ML or Haskell. A lot of it seemed to be a "Java vs. Ruby fight" with a slight bias towards the latter in the authors.

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.

__--__2• 13 years ago

I agree completely, that's why I used the word "inconclusive." Still, it's the only real data we have on static vs dynamic typing. Until we get better data, everything is just opinion and preference. Well informed opinions, in the case of those familiar with type theory (which I am not), but opinion nonetheless.

Hindley-Milner in Clojure

Related Stories