Hacker News Reader

Comment by morelisp | Hacker News Reader

While there's been impressive practical advances recently, the theory dates back to the mid-90s.

Advanced type theory dates back to the 90s too, and yet only now we see it being utilized in mainstream languages more and more

I guess this depends on what you define as "advanced". Many languages still struggle with dependent types and these date back even to the 80s, but I would not say they are "advancing computer science." I agree with the original article that liquid types represent a real recent CS advance (but aren't in any mainstream general-purpose languages yet).

Partial evaluation and meta-tracing, though, were more or less fully understood theoretically by ~2000. What was missing was the enormous amount of tooling and compiler design work needed to support them e.g. Graal, and that in turn preceded by enough work on Java / the JVM to make a project like Graal viable.

Unlike Graal/Truffle, PyPy was done by a very small team.

Dependent types: de Brujin (1967)

Curry-Howard: Curry (1934, 1958), Howard (1968)

MLTT: Martin-Lof (1972)

Polymorphic lambda-calculus: Girard (1972/3), Reynolds (1974)

Effect systems: Gifford/Lucassen (1986)

Calculus of constructions: Coquand/Huet (1988)

HKTs: Girard (1971)

Type classes: Kaes (1988)

Dates are imprecise and from memory.

Could you give me references for this theory of meta-tracing in the 1990s? It seems to me that PyPy was the first to, systematically and in a lightweight way, solve the problem of normal JITs optimising the wrong loop, when JITing interpreter loops.

Reply on news.ycombinator.com