Richard is a Principal Researcher at Tweag I/O. His research centers around how we can use static type systems to power high-assurance programming and avoid programmer mistakes, all without sacrificing ease-of-use or runtime efficiency.
His language of focus is the pure functional language Haskell. Richard is a core contributor to GHC and serves on the GHC Steering Committee. He lives in suburban Philadelphia with his wife and daughter.
There are a surprising number of ways to parametrize a Haskell function.
Since its inception, Haskell has allowed parameters to be dependent (or not), visible (or not), and relevant (or not). Starting with GHC 9.0, to be released this fall, we add linear (or not) to this list. Haskell restricts these choices to be correlated; for example, a parameter cannot currently be both dependent and relevant. Having dependent types mostly just means relaxing this restriction.
This talk will walk through these different flavors of parameters, with examples taken from Haskell and Idris. (No Idris experience necessary.)