Taf - A plan for a statically-typed Lisp
manuel.github.com
manuel.github.com
Also, you should have a look at Andrew Wright's work on Soft Scheme, which also used row polymorphism to statically analyze and check Scheme programs.
You can even turn off the static type checking while keeping the type annotations. Not to mention that the type system is incredibly powerful and expressive.
It's literally the best of both worlds.
However, Siek's Gradual Typing does handle mix-type expressions at finer-grain.
If you're interested in helping out, would love to chat. We're on #dylan on freenode.
Would anything of value of Lisp be lost beyond the typical trade-offs you see mentioned in every static vs dynamic debate, such as up-front ease of development?
Typed Racket lets you easily migrate portions (or the entirety) of a dynamically typed codebase into an equivalent statically-typed version. You get the best of both - easy prototyping with dynamic typing, robustness and scalability of static typing, and then the flexibility of applying those choices to parts of your codebase while keeping everything completely interoperable.
In terms of what you'd lose--eval() for one. It's only been relatively recently that decent type inference has been integrated with interactive execution (GHCi), but I think it's possible (though GHCi is still more limited and cumbersome than full batch GHC).
GHCi is a bytecode interpreter for Haskell, it supports the full Haskell+GHC type system -- and has very little to do with eval() or your comment.
There's no excuse anymore to be ignorant of "modern" static typing - a quarter of a century is long enough.
As one sample point, I have a PhD from a top-10 US institution. Partially in compilers. I'm motivated everyday to learn about programming. I hack on interpreters in my spare time. A lot. I am utterly 'ignorant of modern static typing'. Setting aside modesty, I'll submit that it isn't my fault.
And you can always get a copy of TAPL,
Types and Programming Languages
Benjamin C. Pierce
February 1, 2002
ISBN-10: 0262162091
And there's a typo above, Nilsson should be "Nielson", as in:
"Flemming Nielson and Hanne Riis Nielson.
Two-Level Functional Languages.
Cambridge University Press, 1992.
A Modal Analysis of Staged Computation
Rowan Davies and Frank Pfenning, 1996I kid, but only somewhat. Relevancy (even if just perceived) and accessibility matter.
Presumably, if you're doing type theory, you know it cold. If you're doing crypto or machine learning or computability or databases or (god forbid) are just a working schmo programmer, do you?
It's a big world out there. Can't learn everything, although it's fun to try.
LEAP: A language with eval and polymorphism http://scholar.google.com/scholar?cluster=698636143255963875...
Pfenning follows that up with more advances, leading up to Staged Computation; various techniques at the intersection of reflection, partial-evaluation and typing.
The most recent studies on EVAL in the context of statically-typed languages make use of GADTs.
And Lisps being so powerful you can actually use the language itself to add type safety to it and there's no need for a lot of code (typed Clojure --although not perfect yet-- is quite small, for example).
The great thing is that you also don't need to do it yourself because there are people working on the issue.
With the Lisp "revival" and especially all the coders re-discovering Lisp nowadays I expect to see more and more research in that area and it's pretty exciting.
We'll soon get Emacs (or IDEs) warning us in realtime about type errors ; )
The basic idea is to first expand the whole program (really the whole module) and then to type check the fully expanded code, which doesn't have macros.
When a programmer is forced to think about a type before he already decided what it could be is a limiting factor. All scripting languages are based on this idea.
And, of course, having lists of elements of just the same type and different sets of functions for different types of, say, lists is an ugly thing.
The current mass-hysteria about necessity of static typing is due some sort of Bandwagon effect.
I think it is much better to learn the elegant approach of authors of Scheme and other Lisps to hide necessary hardware types inside a runtime and to allow programmers and themselves to think in terms of a problem domain.
So, statically typed Lisp is something like four-wheel bicycle. It is very "safe" and "stable" but for some reasons no one wants it.
Both of these are not the case with row polymorphism.
I think this is a wonderful initiative. I originally tried to do this a few years ago, but gave up after having considered the implementation too involved (I was using LLVM at the time and was effectively writing a compiler). I still think an optionally typed LISP compiler would be a great idea if somebody is willing to do it.
EDIT: grammar.
Static typing eliminates an entire class of bugs. It's not like any of us need it, it's just a powerful tool. It might be a nice option in a Lisp if it could be done elegantly.
For some protection from being called with wrong arguments there are assertions.
Those who believe that a sophisticated type-system is a protection from idiots, rather than unnecessary burden, seems like come from a corporate Java world, where they believe that something decent could be created by a crowd of mediocre coders piling up "safe" or even "protected" crap.
And of course, Unit tests and CI are our friends.)
I guess it just doesn't seem like a burden to me; most of it is just preventing passing a variable as something it is not or double-checking that you've handled all the cases for Maybes and Eithers. It's all stuff I'd like to be doing anyway.
I don't understand why tail recursion isn't a bigger deal to people.
Paragraph 4 of http://en.wikipedia.org/wiki/Common_Lisp for a vague citation.