3 ms·
Advanced type theory dates back to the 90s too, and yet only now we see it being utilized in mainstream languages more and more
by nrabulinski 3y ago
Advanced 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.