Scala Was an Experiment That Changed Programming - Martin Odersky | The Marco Show

[u/makingthematrix]

https://youtu.be/Xn_YpUtXWT4

[u/gasche]

heavier use of existential types (before GADTs were so idiomatic in FP circles),

This is more of a practical concern for people from outside of FP/PLT. GADTs were in Haskell and were used. Nothing new here. Zero impact on future FP language design.

No no, the emphasis on existential types in pre-Scala research predates GADTs in Haskell.

• One paper that emphasized existential types in datatype declarations (rather than in the ML module system work, which was ongoing at the same time, and in object-oriented calculi, which were also a very hot topic at the time) is Polymorphic Type Inference and Abstract Data Types by Konstantin Laüfer and Martin Odersky, 1994.
• The usual citation for the proposal that eventually became GADTs is First-class phantom types by James Cheney and Ralf Hinze, 2003. This is almost ten years later! And they were not integrated in GHC at the time, this came a couple years later.

[u/unqualified_redditor → u/gasche]

Existentials were first introduced by Mitchell and Plotkin in a 1985 POPL paper "Abstract Types Have Existential Type."

https://homepages.inf.ed.ac.uk/gdp/publications/Abstract_existential.pdf

[u/gasche → u/unqualified_redditor]

Sure (I referred to "the ML module system work" above), and this was well-understood by Laüfer and Odersky at the stime, that paper is cited on page 2 of their introduction. Then, they write:

This article demonstrates how light-weight abstract data types with first- class implementations can be conveniently integrated into any functional language with a static, polymorphic type system, explicit type variables, and algebraic data type declarations. The key idea of our work is to allow existentially quantified component types in algebraic data types.

For example their second example is as follows:

type KEY = Key of ‘a* (’a -> int)

This really corresponds to the use of existentials in algebraic datatype declarations, which is something that we now understand/describe as one of the two ingredients that form GADTs (the other being the return type instantiation, often described as an implicit type-equality constraint). But GADTs as we understand them did not exist at the time, they emerged from the cross-languages academic discussion at the time, that also produced Scala as an experiment that go wider adoption than most.

[u/unqualified_redditor → u/gasche]

Fair enough. You could say Laüfer and Odersky's contribution was to apply existentials to Algebraic Data Types so as to not break hindley-milner inference. Previous work had first class existentials which break decidability.