This is one really tough problem. I wonder how many desirable properties would have to be specified in the type extensions. Substructural types and purity are in her examples, but then, how'd you encode something like a dependent type?
Dependent types break things, yeah. One thing I wish she'd mentioned as well is that QTT (qualitative type theory) is a superset of linear types, so languages should probably be extended with that
_Obviously_ the solution is to give every language linear types and make every language referentially transparent while also marking total functions as distinct from partial functions. \s
To be fair she's not advocating giving every language linear types, only adding linear type checks with interop when you want to interop with a language that supports linear types.
To be clear we've literally hit a point where people have written compilers to translate from one language to the other. The labor of writing an entire new compiler is probably greater than an overzealous affine type checker.
The thing is that once you’ve added the ability to express linear types in the type system and ensure that you don’t violate the constraints of linear types you’ve done most of the work involved in implementing linear types.
"Different languages are best suited for different tasks." This is reasonable. But consider that many languages (Python, Javascript, C, C++, etc) are being used for tasks they are hardly suited for. On a large scale. So, while the statement is fundamentally true, people are very, very tolerant and there must be a design space for a single language which targets and is sufficiently suitable for a wide range of applications. Even then, this is a good talk and important work, thanks for sharing!
This speaker knows her her stuff.
This is one really tough problem. I wonder how many desirable properties would have to be specified in the type extensions. Substructural types and purity are in her examples, but then, how'd you encode something like a dependent type?
Dependent types break things, yeah. One thing I wish she'd mentioned as well is that QTT (qualitative type theory) is a superset of linear types, so languages should probably be extended with that
_Obviously_ the solution is to give every language linear types and make every language referentially transparent while also marking total functions as distinct from partial functions.
\s
To be fair she's not advocating giving every language linear types, only adding linear type checks with interop when you want to interop with a language that supports linear types.
To be clear we've literally hit a point where people have written compilers to translate from one language to the other. The labor of writing an entire new compiler is probably greater than an overzealous affine type checker.
The thing is that once you’ve added the ability to express linear types in the type system and ensure that you don’t violate the constraints of linear types you’ve done most of the work involved in implementing linear types.
What stops linking types from being used for non-FFI use cases? At that point you've just added linear/pure types to OCaml, FFI or not.
"Different languages are best suited for different tasks." This is reasonable. But consider that many languages (Python, Javascript, C, C++, etc) are being used for tasks they are hardly suited for. On a large scale. So, while the statement is fundamentally true, people are very, very tolerant and there must be a design space for a single language which targets and is sufficiently suitable for a wide range of applications. Even then, this is a good talk and important work, thanks for sharing!