FP /

Agda mode for Yi

What is Yi

Yi is a text editor written in Haskell and extensible in Haskell. It provides a flexible, powerful and correct editor core scriptable in Haskell.

Yi already has a Haskell mode, emacs key bindings which can be used as a basis for this project.

What is Agda

Agda is a dependently typed programming language with good support for programming with inductively defined families of types.

Agda is also implemented in Haskell, so scripting should be natural. Agda currently has an emacs mode which also can be used as a basis for this project.

Goals of the project

  • Adding support for interactive programming / proving in Yi
  • Provide this as a Cabal package on Hackage

The long term goal is to provide a package that provides an Agda development environment.

Probable steps on the way:

  • learn about the framework (Yi and Agda)
  • set up a trivial cabal package (keep extending it below)
  • write a coarse-grained parser for Agda syntax using the Yi parsing library
  • add support for interaction points
  • add bindings for
    • type-checking / loading
    • show syntax highlighting
    • show context, type, evaluate to normal form
    • refining interaction points
    • generate case skeleton
    • ...
Functional programming, Programming (Languages or Paradigms), Software Architecture, (Types for Programs and Proofs is recommended)
Jean-Philippe Bernardy and Patrik Jansson
Number of people

Learning outcomes:

  • good understanding of advanced software architecture
  • experience with software deployment (packaging etc.)
  • software engineering within functional programming
  • experience with software technology: combinator parsing, proof assistants