Thu 11 Jan 2018 16:15 - 16:40 at Bunker Hill - Language Design Chair(s): Zachary Tatlock

Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts, implicitly. Scala offers implicit parameters which are used pervasively, but which cannot be abstracted over.

This paper describes a generalization of implicit parameters to implicit function types, a powerful way to abstract over the context in which some piece of code is run. We provide a formalization based on bidirectional type-checking that closely follows the semantics implemented by the Scala compiler.

To demonstrate their range of abstraction capabilities, we present several applications that make use of implicit function types. We show how to encode the builder pattern, tagless interpreters, reader and free monads and we assess the performance of the monadic structures presented.

Thu 11 Jan
Times are displayed in time zone: Tijuana, Baja California change

15:50 - 16:40: Language DesignResearch Papers at Bunker Hill
Chair(s): Zachary TatlockUniversity of Washington, Seattle
15:50 - 16:15
Research Papers
Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Japan, Zhenjiang HuNational Institute of Informatics
Link to publication DOI Pre-print Media Attached File Attached
16:15 - 16:40
Research Papers
Martin OderskyEPFL, Switzerland, Olivier BlanvillainEPFL, Fengyun LiuEPFL, Switzerland, Aggelos BiboudisEcole Polytechnique Federale de Lausanne, Heather MillerEcole Polytechnique Federale de Lausanne, Sandro StuckiEPFL