2 10 Elaborator Reflection: Extending Idris in Idris

Elaborator Reflection: Extending Idris in Idris

There are two things that you might mean here: how Idris is translated to the core language, or how that machinery is exposed to Idris code for metaprogramming. Neither is really covered, but you can learn about the former from Edwin's JFP paper, and the latter from either our ICFP paper, my PhD, or by watching the talk. There's also built-in API docs for every symbol exposed from the library that you can browse from the Idris REPL, but that doesn't give much of an overview of the whole system.

I switch between different packages, depending on the type of presentation and the audience. However, I increasingly find that I use Racket's slideshow package for most talks. It has lots of the advantages of Beamer, like the ability to keep slides in Git, the ability to script complicated visual aids, and with a library, the ability to display LaTeX math. At the same time, it has fewer of the built-in assumptions that can make Beamer slides so text-heavy and bureaucratic. Also, it can do things that Beamer just can't, like animations and interactivity. For my ICFP talk last year, I even implemented an interactive Idris component, including an editor with semantic highlighting and a work…