A systems programmer who uses a statically typed functional language like OCaml, Scala, or Haskell can be forgiven for doubting the importance of the latest addition to the type system of their language of choice. Certainly, that was what we thought about the arrival of Generalized Algebraic Data Types, or GADTs, to OCaml. The motivating examples for GADTs all seem to be about tagless interpreters and typeful representations of ADTs, all of which sound like the kind of thing you get when you let compiler writers design your language.
In this case, however, we were wrong. After some experience with GADTs, we came to realize that they're of central importance for writing high performance code, in particular by giving the programmer better control over how data is represented in memory. This talk will focus on one example: the use of GADTs to provide convenient and efficient representations for dealing with network packets in a zero-copy, zero-allocation way.
Yaron Minsky got his BA in Mathematics from Princeton and his PhD in Computer Science from Cornell, where he studied distributed systems. He joined Jane Street in 2003, where he started out doing quantitative research on trading strategies, going on to found the firm's quantitative research group. He introduced OCaml to the company and eventually managed the transition to using OCaml for all of its core infrastructure, turning Jane Street into the world's largest industrial user of OCaml. In the meantime, he's been involved in many different aspects of Jane Street's technology stack, including trading and risk systems, developer tools, and user-interface toolkits.
Faculty Host: Jan Hoffman