Invisible arguments: language design (discussion)
Any language with a sufficiently advanced type system will have a need to support invisible arguments. These arguments might be erased at runtime or not, but they are not written by programmers (by default) in their source code. Examples include type parameters and type-class dictionaries. The design space around invisible arguments is large: How syntactically do we denote the visibility of an argument in a type? Are programmers allowed to pass an invisible argument visibly? When defining a function with invisible parameters, how can the body of the function access those parameters? Does order matter? Do names matter? What happens when the presence of some of the invisible arguments are actually inferred? How do we deal with different mechanisms for inferring concrete arguments at call sites (e.g. unification vs. constraint solving)? Come join the conversation with some questions of your own, and perhaps even some answers.
Principal Researcher at Tweag. I believe that clever application of theory can eliminate a great deal of programmer errors – specifically, I think fancy types and functional programming are the future. I completed my PhD in 2016 at University of Pennsylvania working under Stephanie Weirich; my dissertation topic was the integration of dependent types into the Haskell programming language. I am a core contributor to the Glasgow Haskell Compiler (GHC) and Chair of the Board of Directors at the Haskell Foundation.
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00
|Make Three To Throw Away: Frontiers in Homotopical Proof AssistantsRemote|
Jonathan Sterling Aarhus University
|The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoqRemote|
|Elaborator reflection APIs (discussion)Remote|
Jesper Cockx TU Delft
|Invisible arguments: language design (discussion)In-Person|
Richard A. Eisenberg Tweag