3 ms·
While there's been impressive practical advances recently, the theory dates back to the mid-90s.
by morelisp 3y ago
While there's been impressive practical advances recently, the theory dates back to the mid-90s.
- nrabulinski 3y agoAdvanced type theory dates back to the 90s too, and yet only now we see it being utilized in mainstream languages more and more
- morelisp 3y agoI 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.
- Loq 3y agoUnlike Graal/Truffle, PyPy was done by a very small team.
- Loq 3y agoDependent 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.
- Loq 3y agoCould 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.