yagi

yagi is an experimental, dependently-typed programming language, still in the "primordial ooze" phase of development. The project consists of three parts:

• yagi-lang defines the yagi syntax, parser, and typechecker
• yagi-lsp-server is a language server for yagi built with the lsp package
• yagi-lsp-client is vscode extension which communicates with the yagi language server to show parsing and type information

Attributions

At the moment, significant portions of the code are directly adapted from the following excellent projects.

• For the intial typechecker, I translated some of the OCaml code from Andrej Bauer's series "How to Implement Dependent Type Theory" into Haskell.

• The yagi parser is built with megaparsec. I am using a custom Stream instance to attach position information to each node of the tree.

• The structure of the yagi language server is mostly copied from dhall-lsp-server. I learned a lot reading through the source code of the Dhall language server (also using lsp) and parser (also based on megaparsec).

• The yagi language client was written using vscode-haskell as a reference. See also the language server extension guide.

The haskell-language-server source has also been a valuable reference.

Features

Implemented

• pi-types
• universes
• type annotations

Todo

• normalization by evaluation
• sigma-types
• pattern matching
• tactics
• typeclasses
• do-notation
• inductive types

Stretch Goals

• ornaments
• built-in induction principles and recursion schemes
• stream fusion