At the risk of horn auto-tooting and potential shameful self-promotion, I will link to my own Cognicast appearance. Topics include Clojure, Lisp, Haskell, Type theory, LispCast, and this very Gazette. Mutual recursion!
I really liked this interview. I was surprised to hear about expecting a clean, fundamental core static language to rise in the future.
It makes me reflect back on when Rich presented his rationale to LispNYC. I wasn’t there, unfortunately, but it’s one of my favorite recording about Clojure.
What I’m getting at is, should you be able to articulate some of your objectives or rationale, this could be the seed of something great!
Do you happen to know where to get that talk? I don’t think I’ve heard it and a lot of people refer to it.
But to answer your interest, I think it would be great if I could program using formal models. Lots of this is just ideas; I am no authority on the matter. I will probably put my foot in my mouth.
What is the relationship between the type system and the choice of types? I often felt that Haskell’s selection of types was not very powerful. You got some power from the formality of them, but I never felt as powerful as I feel with map with seq abstraction in Clojure. Obviously, there are explorations happening there in the typed world and as these develop, they could be integrated in.
I am really interested in Type 2 bootstrapped languages (small core, rest written in itself, like Lisp). Is this possible with a Hindley-Milner type system? This might involve reifying types to exist at runtime, or perhaps have a separate “type inference time” where typing code can run, just like Lisp macros have a special time to run in.
Static typing on a dynamically typed language (Curry-style). I guess that’s called Gradual Typing but everything I’ve seen with gradual typing has been trying to partially type untypeable code. What about a totally typeable subset of a language (according to some type system). You would write your code in a dynamic way first, then turn on the inference and it would help you restrict your code to the formal version allowed by the types. Again, this may exist. I don’t keep up-to-date. I like the idea of multiple type systems, but that seems like a pipe dream.
The stuff that people are doing with GHC, that it is very high-level code compiled to beat C in many cases is amazing and it’s only getting more capable. Haskell started with very humble type inference capabilities and research has added more and more.
What may or may not be obvious is that I want a Typed Lisp. Not just s-expressions and macros, but something that embraces much more of what’s cool about Lisp. Lisp is dynamic (not dynamic types, but the language is largely available at runtime); it is bootsrapped from a small fixpoint; it is homoiconic (macros); it has powerful data structure abstractions; and it has lexical closures. Haskell is ok in terms of data structures. It has closures. It does have a macro system called Template Haskell, but because it’s statically compiled it does not the same. Would love to see a language with the other two.
Eric, you’re aware of the Shen language, are you not? I’m pretty sure I remember you writing about how inspiring it was for you, but this post of yours raised doubts in me.
I’m aware of Shen. It’s interesting. But why would you doubt?
I wondered how Shen is not, for you, what you’re seeking.
Ah, ok, good question.
I’ve always had Shen on my list of stuff to look at when you get the inclination. It’s interesting and I’d like to learn more about it, but I just can’t evaluate it. If it got more people using it, that would bump it up a lot on the list. But because you bring it up, I just might have to take another look.
Have you explored Shen?
I read (in 2009) the Qi II book detailing its implementation and usage. That was a very, very entertaining Type 2 bootstrapping reading. Since it became Shen (even though Shen is even more interesting than Qi was), I’ve looked at it from afar, having settled on Clojure for my pragmatic needs. The author has since rewritten his book for Shen, providing almost the same level of detail as to the language’s implementation.
Clojure really hits a sweet spot due to its host interop emphasis. Shen, on the other hand, makes me feel the community would eventually end up rewriting the whole world (like most new languages). For that reason, I’d rather thrive in Clojure until they’re done doing a substantial amount of that rewriting. Who knows what can happen in the span of, say, 25 years, both in Clojure’s court and in Shen’s court?