Staging with Class: A Specification for Typed Template Haskell • Ningning Xie • YOW! 2022

This presentation was recorded at YOW! 2022. #GOTOcon #YOW https://yowcon.com Ningning Xie - Research Associate at Department of Computer Science and Technology University of Cambridge @ningningxie3528 RESOURCES https://twitter.com/xnningxie https://xnning.github.io ABSTRACT Multi-stage programming using typed code quotation is an established technique for writing optimizing code generators with strong type-safety guarantees. Unfortunately, quotation in #Haskell interacts poorly with type classes, making it difficult to write robust multi-stage programs. In this talk, I will present my recent work which studies this unsound interaction and proposes a resolution, staged type class constraints, which is formalized in a source calculus that elaborates into an explicit core calculus. I will show type soundness of both calculi, establishing that well-typed, well-staged source programs always elaborate to well-typed, well-staged core programs, and prove beta and eta rules for code quotations. The design allows programmers to incorporate type classes into multi-stage programs with confidence. Although motivated by Haskell, it is also suitable as a foundation for other languages that support both overloading and quotation. [...] TIMECODES 0:00 Introduction 2:32 Quotations and splices 3:24 Multi-stage programming: example 5:20 Code generation 8:30 Multi-stage programming and type classes 10:53 Multi-stage programming: well-typedness 12:56 Well-stagedness: the level of an expression 14:02 Well-stagedness: the level restriction 15:50 Is the problem with qpower well-stageness? 17:50 Well-staged type classes 18:45 Key idea: staged type class constraints 21:04 Level-indexed constraint resolution 22:32 How to evaluate staged programs? 23:27 Level-indexed Evaluation 24:21 Key idea: splice environments 26:57 Type-directed elaboration 27:53 Integration into #GHC RECOMMENDED BOOKS Vitaly Bragilevsky • Haskell in Depth • https://amzn.to/3EXpmbe Rebecca Skinner • Effective Haskell • https://amzn.to/3VgUKsh Graham Hutton • Programming in Haskell • https://amzn.to/3Fi8rBC John Whitington • Haskell from the Very Beginning • https://amzn.to/3VmX68R https://twitter.com/GOTOcon https://www.linkedin.com/company/goto- https://www.facebook.com/GOTOConferences #SoftwareEngineering #Programming #FunctionalProgramming #Tech #SoftwareDevelopment #SoftwareTechnology #-NingningXie #YOWcon Looking for a unique learning experience? Attend the next GOTO conference near you! Get your ticket at https://gotopia.tech Sign up for updates and specials at https://gotopia.tech/newsletter SUBSCRIBE TO OUR CHANNEL - new videos posted almost daily. https://www.youtube.com/user/GotoConferences/?sub_confirmation=1