#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
Type Theory Forall
00:00
Exploring Quotation and Quasi-Quotation in Programming Languages
The chapter discusses the significance of bidirectional type checking, delving into the concepts of quotation and quasi-quotation in programming languages like Lisp and Idris. It highlights their importance in treating programs as data, implementing interpreters, and creating embedded languages for specific tasks like signal processing. The chapter also explores the nuances of syntax transformation, code transformation, pattern matching, and the implementation challenges related to handling quotation.
Transcript
Play full episode
