EffW is an implementation of Algorithm W (see Luis Damas’s PhD thesis) in terms of algebraic effects and handlers.

EffW.hs

The first implementation of Algorithm W using Algebraic Effects.

• Haskell implementation by Conor McBride
• implements parameterised algebraic effects as Kripke resumptions that keep track of meta variables
  • see Sigal’s et al HOPE 2024 talk for more information
• uses the locally constrained Dictionary trick to get GHC to automatically generate segments for resumptions

EffW in Agda

The first attempt at a typechecker for Gilear:

• in Agda by @wenkokke, @cyberglot and @takanuva
• generation of paths out of Kripke resumption segments are done by hand
• abandoned half-way for Haskell version (below)
• to be moved to Faeth and refactored

EffW in Haskell [again]

Gilear typechecker implementation:

• in Haskell by @wenkokke, @cyberglot and @takanuva
• generation of paths out of Kripke resumption segments are done by hand (as opposed to the Dict trick)
  • note: the necessity modality creeps up