[plt-scheme] Statically typed Lisp-like language?

On Jan 1, 2008, at 10:36 AM, Shriram Krishnamurthi wrote:

> There have been plenty of statically-typed Lisp systems.  The earliest
> I know of, at least one of any quality or significance, is that by
> Robert Cartwright:
>
> http://stinet.dtic.mil/oai/oai? 
> verb=getRecord&metadataPrefix=html&identifier=ADA045722
>
> In the early 1990s, there was a long line of research at Rice
> (initiated again by Cartwright and his students, and subsequently
> pursued by Felleisen and his students) on typed Lisps -- the students
> in question are Fagan, Wright and Flanagan.  Wright's thesis has the
> most insight into what it takes to create a meaningful type system for
> a language like Lisp.
>
> This work still continues today, personified by Tobin-Hochstadt and
> Matthews, working with Felleisen and Findler.

There are two distinct traditions of typed Lisps:

1. explicitly typed Lisps, and yes, Cartwright initiated this branch  
in the early 1970s.

2. before that, Boyer and Moore initiated what people who now call a  
system based on type inference. Anything you could prove about a  
program was/is a type. This is the 1970s perspective.

This second community split into two sub-communities: type inference  
people and verification people. The former tend to understand the  
world according to the modern frame of reference; in my experience  
talking to the latter kind of people is often like talking to the  
wall (unless they are thm provers who originated in the PL community).

In the late 1980s, the Scheme community developed the notion of soft  
typing: type inference (or recovery) from existing Scheme programs  
plus the notion that even if  the program isn't typable according to  
your type system, you run it. That is, you repair the program (just  
like in parsing) and you continue type checking/elaborating. The Rice  
people had four efforts in this direction:

  -- Fagan, supervised by Cartwright; inference based on Hindley  
Milner, using an algebra of extensible records instead of arrow types
  -- Wright, jointly supervised by Cartwright and myself; ditto but  
for a full-fledged Scheme (Chez) not some mini Scheme
  -- Flanagan, I was the supervisor; based on set-based analysis and  
incorporating a "witness trace" facility (drawing a flow graph)
  -- Meunier, I supervised this, too; based on SBA plus module  
boundaries

Aiken and co at IBM Almaden, then Aiken at Berkeley alone: developed  
a set-based analysis for FL, Backus's Lisp-style combinator language;  
that was after Fagan and contemporary to Wright.

Henglein at DIKU translated Scheme into ML using brute-force  
projection and injection, then minimizing those. I had proposed the  
first step to Fagan before he discovered Didier Remy's work on  
extensible records and took off in that direction.

Parallel to Flanagan, Wadler picked up Wright's work and produced  
some soft typer for Erlang. Someone else in Sweden (of Greek origin)  
continued this effort. I don't believe they extended Wright's framework.

An MIT master student did something that I can't decipher for Python.  
I don't think there is any theory behind that or any principles.  
That's 2003 or 4.

;; ---

Sam and I picked up explicit typing again. I know that some  
verification people tried to assign CL a type system (UT Austin, six  
seven years ago). They are thm provers and just don't know enough PL.  
So I suspect we're the first ones since Corky Cartwright's 1974 effort.

Matthews and Findler is NOT at all a typed Scheme/Lisp effort. It is  
a theoretical framework for integrating distinct languages with  
protection of individual global invariants. They expounded this idea  
with a pairing of typed and untyped lambda calculi. It is much more  
general work and equally applies to ByName and ByValue, and other  
such things. Sam and I did exploit an idea from this work for the  
integration of Typed Scheme and PLT Scheme. Our type system is  
independent of the above, except Cartwright's 1974 system.

Following the example of the XML community (that is, Essence of ML)  
from the early 90s, we consider type inference a mechanism in the IDE  
for recovering types from partially type source, i.e., a translation  
of source to explicitly typed Scheme.

Shriram and Guillaume Marceau have investigated a similar route,  
based on Wright's system. As far as I know there are no pubs.

-- Matthias