Algebraic Macros is a project to add meta-programming via algebraic effects and handlers to dependently typed languages. It is developed by April Gonçalves and Robert Atkey, along with collaborators.

The idea was first introduced by Robert Atkey in a series of talks entitled “An Algebraic Approach to Typechecking and Elaboration”.

Agda version

• on codeberg: Fancy Algebraic Effects for Types and Humans (Faeth)
• What is in Faeth ?
  • Faeth is a study on algebraic macros for typechecking and elaboration for type systems, with special focus on developing meta-programming for dependently typed programming languages.
• Roadmap
  • Basic implementation of algebraic macros for different, simple type theories. done
  • Algebraic macros for System F$\omega$, including proofs for effect equations. paused
  • Refactoring from Eff W’s Agda version. paused
  • Binders & Elaboration: what, how and why? wip

Prototype language

• on codeberg: Greatest Imaginable Language According to Rumour (Gilear)
• Gilear is “playground” programming language, to experiment with dependent types, CPS compilation, meta-programming and incremental editor updates. wip
  • built in collaboration with Wen Kokke (parsing, editor support; main dev) and Paulo Torrens (compilation, IR, CPS transformations)
• Roadmap
  • Incremental parsing via tree-sitter. done
  • Basic VSCode editor support. done
  • Basic compiler pipeline. done
  • Two-Level Type Theory implementation into Dependent CPS Calculus. wip

We are studying whether the Effing W approach could be applied to Gilear and Faeth.