July 15, 2014
Summary: Static vs dynamic typing debates often flounder because the debators see from two different perspectives without knowing it. Learning to identify the two perspectives can calm the discussion. The tension between the two perspectives has led to Gradual Typing and other technologies.
Many discussions about type systems around the internet fail to be interesting because one or both parties are not versed in type theory. There's a less common (yet related) reason, which I have begun to notice more and more: people who are not familiar with the difference between Church Types and Curry Types. These are also known, respectively, as Intrinsic Types and Extrinsic types. Because the participants are not aware of the two perspectives, they blame the other one for ignorance, when in fact they just have a different perspective.
Church Types are what Haskell has. Church types are named for Alonzo Church, the inventor of the lambda calculus. In a Church-style system, types are an intrinsic part of the semantics of the language. The language would be different without the types--it may even be meaningless. With an intrinsic type system, the meaning of the program is different from the runtime behavior of the program. One way to think of this is that so much of the meaning of the program occurs at compile time that you can begin to think of the program having properties you can reason about even if you never run the program.
The other kind of types are Curry types (aka extrinsic types). They are named for Haskell Curry, the man the Haskell language is named after. Curry-style types is when a system of types is applied that is not part of the semantics of the language. This is what Clojure has in core.typed. The meaning of a Clojure program is not dependent on it passing the type checker--it can be run without it. The type checker simply alerts you to type errors in your code. Note that you could consider your type checker to be your own head, which, as flawed as it may be, is what most Clojure programmers use. The types could be anywhere outside of the language.
Each perspective is valuable and bears its own fruit. Intrinsic types are great because you are guaranteed to have a mathematically-sound safety net at all times. You always have something you can reason about. Such is not guaranteed for extrinsic type checkers. They may not be able to reason about your code at all.
Extrinsic types are useful because you can apply multiple type systems to your code--or even write something that you don't know how to prove is sound. There are more benefits on both sides, but you get the idea.
We now have a new perspective which is slightly "higher" than either of them. We can now see that both perspectives exist and talk about them as such. What can we see/say now that we couldn't before?
A famous article by Robert Harper exemplifies the Church perspective very well. It argues that untyped programs are a subset of typed programs. They are programs that have a single type and all values are of that one type. So instead of being liberating, dynamic languages restrict you to one type. Notice the assumption that languages have a type system by default which is typical of the Church-style perspective. We can now say "This reasoning is correct given that perspective."
On the other side, you'll often see a dynamic typist say the exact opposite: that well-typed programs are a subset of dynamically typed programs. In other words, well-typed programs are just dynamic programs with fewer errors. Curry-style to the core: static type errors are something that is added onto the semantics of the language. We can now see that they are right, from their perspective.
Here's a diagram:
Notice how they're isomorphic? That means something, I just don't know what :)
My ambitious hope is that this perspective will quiet a lot of the fighting as people recognize that they are just perpetuating a rift in the field of mathematics that happened a long time ago. The perspectives are irreconcilable now, but that could change. A paper called Church and Curry: Combining Intrinsic and Extrinsic Typing builds a language with both kinds of types. And Gradual Typing and Blame Calculus are investigating the intersection of static and dynamic typing. Let's stop fighting, make some cool tools and use them well.
For more inspiration, history, interviews, and trends of interest to Clojure programmers, get the free Clojure Gazette.
Learn More
Clojure pulls in ideas from many different languages and paradigms, and also from the broader world, including music and philosophy. The Clojure Gazette shares that vision and weaves a rich tapestry of ideas from the daily flow of library releases to the deep historical roots of computer science.
You might also like
January 13, 2014
All sarcasm aside, the above diagram has a kernel of truth. The important thing to note is that the intersection between "Proponents of dynamic typing" and "People familiar with type theory" is very small.
In an effort to increase the size of that intersection, I decided to familiarize myself with a little more type theory. I developed an implementation of Hindley-Milner which operates on a simple Lisp-like λ-calculus with let polymorphism. Everything you need for Hindley-Milner Algorithm W.
Background
Hindley-Milner is a type system that is used by ML and Haskell. Algorithm W is a fast algorithm for inferencing Hindley-Milner which is syntax-directed (meaning it is based on the type of expression) and recursively defined. In this way, it is similar to Lisp's eval.
Implementation
I based my implementation on a paper called Algorithm W Step by Step which implemented it in Haskell. My implementation started very similar to that implementation and diverged as I refactored it into a more Clojure-esque style.
This implementation uses no in-place mutation, instead using a "substitution style" which is slightly harder to read. It is, however, easier to write and prove correct.
In addition to the type inferencer, I wrote an interpreter for the same language, just because. My original intent was to expose (to myself) the similarities between syntax-driven type inference and eval. There might be some, but the full clarity I desire is yet many refactorings away. Note that the interpreter and type inferencer are completely independent, except that both apply to the same set of expressions.
I added a couple of minor luxuries to the language having to do with currying. Writing fully parentheisized function applications for curried functions is a pain, as is writing a hand-curried function with multiple arguments. I added two syntax transformations which transform them into a more Lispy style. For example:
(fn [a b c d e f] 1) => (fn a (fn b (fn c (fn d (fn e (fn f 1))))))
and
(+ 1 2) => ((+ 1) 2)
I'm pretty sure the syntactic transformation is completely safe. All of my tests still type check.
The final luxury is that it is a lazily-evaluated language. That's not strictly necessary, but it is strictly cool. It builds up thunks (Clojure delays and promises) and a trampoline is used to get the values out. This lets me define if as a function. The only special forms are let and fn.
Where to find it
You can find the code in the ericnormand/hindley-milner Github repo. I don't promise that it has no bugs. But it does have a small and growing test suite. Pull requests are welcome and I will continue to expand and refactor it.
What I learned
Type unification is why the error messages of most type inferencers are so bad. Unification by default only has local knowledge and is commutative (unify a b == unify b a). No preference is given to either argument. A lot of work must have gone into making the error messages of Haskell as good as they are.
Let polymorphism is useful and I'm glad that Haskell has it.
Hindley-Milner is powerful, but it does not by itself work magic on a languageq. A language still requires a lot of good design and a well-chosen set of types.
Your turn
I think you should implement Hindley-Milner in the language of your choice for a small toy λ-calculus. There is a lot to learn from it, even if you never program using a Hindley-Milner language. At the very least, you'll know what the fuss is about.
If you think it would be helpful, have a look at my implementation. Like I said, pull requests are welcome.
For more inspiration, history, interviews, and trends of interest to Clojure programmers, get the free Clojure Gazette.
Learn More
Clojure pulls in ideas from many different languages and paradigms, and also from the broader world, including music and philosophy. The Clojure Gazette shares that vision and weaves a rich tapestry of ideas from the daily flow of library releases to the deep historical roots of computer science.
You might also like
November 02, 2013
It is better to have 100 functions operate on one data structure than 10 functions on 10 data structures. -- Alan Perlis
In his essay titled "Dynamic languages are static languages", Robert Harper states:
the so-called untyped (that is "dynamically typed") languages are, in fact, unityped. Rather than have a variety of types from which to choose, there is but one!
The notion that a language with no types also has one type is absurd, so we must proceed and allow the perspective that a language with dynamic typing actually has a single static type. The argument is very rhetorical, but it does seem to be a valuable perspective. However, I disagree with the final conclusion:
And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice!
I believe that a well-chosen type is freeing.
In Smalltalk, "everything is an object". This statement is one of the first things you might hear about the language--from people who use it and like it. What is that statement but a declaration of having one type? That one type, with its single operation (send message), is what made Smalltalk so powerful.
Smalltalk's power comes from adhering to a small, firm discipline that others also adhere to. Much like the laws of a government might be binding in a certain sense, in another they give rise to the freedom and privilege citizens enjoy in society. The prohibition of murder allows us the freedom to move about without fear of death. The rules governing market transactions ensure a minimum of fairness. Everyone benefits.
In the same way, Smalltalk's message passing presents a very small point of agreement in order to participate in the bounty of the runtime. Powerful tools, services, and metaprogramming facilities were available for the small price of conforming to a very simple type.
Far from being restrictive, a single type is freeing. The rhetoric of "bondage" does not hold, since there is an existential proof of a single type being the source of freedom and power. I wonder if a paucity of perspectives is part of the reason such an obvious flaw can arise in an intelligent essay. There are no sides in the search for better tools. We will want to combine the powerful elements from as many different perspectives as possible.
You might also like
April 15, 2015
Nathan Sorenson's talk at Clojure/West is about type systems for DSLs.
Background
Clojure is a dynamically typed language. The types are encoded in the classes of objects. However, when we develop a DSL, we are designing a new language and are free to build in a static type system for that DSL. Nathan Sorenson's talk addresses some of the hardest but most important work in developing a type system: the error messages and interoperability. And it seems practical: he'll be developing a query DSL for Datomic.
If you're new to macros, you may want to read the macro chapter from Clojure for the Brave and True. If you're really interested in Type Theory, you're in for a treat with this recording of Robert Harper.
GitHub - Twitter
This post is one of a series called Pre-West Prep, which is also published by email. It's all about getting ready for the upcoming Clojure/West, organized by Cognitect. Conferences are ongoing conversations and explorations. Speakers discuss trends, best practices, and the future by drawing on the rich context built up in past conferences and other media.
That rich context is what Pre-West Prep is about. I want to enhance everyone's experience at the conference by surfacing that context. With just a little homework, we can be better prepared to understand and enjoy the talks and the hallway conversations.
Clojure/West is a conference organized and hosted by Cognitect. This information is in no way official. It is not sponsored by nor affiliated with Clojure/West or Cognitect. It is simply me (and helpers) curating and organizing public information about the conference.
You might also like
October 08, 2013
Way back in May 2012, Ambrose was beginning work on Typed Clojure for Google Summer of Code. I interviewed him to get an idea of what kind of type system we could expect. Since he's now running a very successful crowd funding campaign, I thought I'd bring up this blast from the past.
You might also like
October 08, 2013
Michael Fogus is right (as usual) about this one. Someone with Odersky's stature should not fear lack of humilty but instead lack of confidence.
You might also like
