"Qi makes use of the logical notation of sequent calculus to define types. This type notation, under Qi's interpretation, is actually a Turing complete language in its own right. This notation allows Qi to assign extensible type systems to Common Lisp libraries and is thought of as an extremely powerful feature of the language."
http://en.wikipedia.org/wiki/Qi_(programming_language)
What also interests me is that, unlike Java or Scala, adding types is optional, so the types can be layered in. I prefer that style, because when I face a new problem that I have never faced before, I feel that adding type information suggests I know something that I don't actually know. I prefer to add types to a function, once I've come to understand what role a function should play in regards to the problem I'm trying to solve. In that way, the type information also communicates what I have learned about the problem I am trying to solve, versus the areas of my problem that I am still ignorant about, and whose code I can leave untyped while I figure things out.
I am also intrigued by what fogus has written:
"Qi (and its successor Shen) really push the limits of what we might call a Fluchtpunkt Lisp. I suspect it requires a categorization of its own. A few years ago I was looking for a Lisp to dive into and my searching uncovered two extremely interesting options: Clojure and Qi. I eventually went with Clojure, but in the intervening time I’ve managed to spend quality time with Qi and I love what I’ve seen so far. Qi’s confluence of features, including an optional type system (actually, its type system might be more accurately classified as “skinnable”), pattern matching,3 and an embedded logic engine based on Prolog, make it a very compelling choice indeed."
http://blog.fogus.me/2011/05/03/the-german-school-of-lisp-2/
Just recently, here on Hacker News, we had posted an example of a step-by-step explanation of adding types to a working Shen app:
http://www.shenlanguage.org/library/shenpaper.pdf
Someone in the comments on Hacker News highlighted this comment, by the original author of the untyped app:
"No, I didn't think about writing typed version of this program. You know, I'm not "disciplined" kind of person so type discipline is (for now) pretty foreign to me. :) I have the strange feeling that types hampers programmer's creativity."
Mark Taver responded with his own thoughts, which I thought were interesting:
"The underlined 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 [9] [11], is that the human ability to recognise truth transcends our ability to capture it formally. In computing terms our ability to recognise 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."