We’ve got some pretty sharp minds in type theory wandering around this channel. I’m more and more convinced that static types are powerful, and that a language without them is going to be missing on a dimension of expressiveness. But I use Typescript at work, and its gradual typing system is pretty sweet. From a type theorist’s perspective (I know oh so little about type theory, so be gentle with me), does gradual typing get a seat at the table, or do type theorists look at gradually typed languages like functional programmers look at Javascript: sure, some of the same primitives are there, but you’re severely handicapping yourself in expressiveness and power.
👍 1
j
Jonathan Schuster
06/21/2019, 1:12 AM
It's a very active area of research, but the short answer is that (in my experience) type theorists do pay it serious attention. This paper from one of my former labmates goes into it, and following forward and backward references from there should give you more info: http://www.ccs.neu.edu/home/amal/papers/gtt.pdf
👍 1
Jonathan Schuster
06/21/2019, 1:13 AM
Max would probably be happy to talk more about it on Twitter too: @maxsnew
g
Garth Goldwater
06/21/2019, 4:10 AM
I think you can look at projects like hazel with typed holes as being an outgrowth of absolutely taking the ideas of gradual types systems seriously—sometimes youre in the middle of figuring out what your program should do and youre not ready to type it yet and that's ok—and the best type theorists in PLT IMO are saying "all code is ok—how can we get the compiler to help you here?"
The way you get “a seat at the table” in type theory is to present a type system that offers some formal guarantees. I don’t know if Typescript itself qualifies, but there is quite a line of work on gradual typing that does offer formal guarantees (cf. the papers posted above), for example if, even though the types are currently unknown, it’s not impossible that they could be correct when realized in practice. Gradual typing was the subject of the keynote at the 2018 ICFP (Int’l Conference on Functional Programming), so it has enough respect amongst some influential members of the academic community (but see the cute aside at 26:30 in the video)!