The Next 700 Module Systems

Extending Dependently-Typed Languages to Implement Module System Features In The Core Language

This repository contains the research proposal for my doctoral studies at McMaster University under the supervision of Jacques Carette and Wolfram Kahl.

What are and what should be the module systems of DTLs? DTLs remove distinctions between packaging systems and so using pedestrian modules systems is not necessarily the best route.

• A requirements driven approach to coherent modularisarion constructs in Dependently-typed languages.

• Main Question: What are the module systems for Dependently-Typed Languages?

• Goal: Extend Agda to be powerful enough to implement the module system features, in the core language, that people want to do.

  In user facing libraries, redundancies are desirable since they may utilise a a variety of aliases for what user want, this is useful flexibility.

  • However, in the source file, each item should only exist once.
  • The front-end redundancy should be produced by machine generation,

rather than by hand.

◈ Website ◈

A super simple description of this work, for the layman, can be found here.

Prototype and a Preprint

◈ Prototype ◈ MathScheme: 200+ Math Theories in (Clickable) Agda ◈ A Language Feature to Unbundle Data at Will ◈ Slides ◈ Youtube

The Context Library ---An Agda Counterpart of the PackageFormer Prototype

◈ [PhD Thesis](./thesis.pdf) ; [Youtube](https://youtu.be/hTQG2QbBPhA) ◈ [Slides](./phd-defence.pdf) ◈ AIM 2020: [Youtube](https://youtu.be/lSIFM5lhnWc); [Slides](./diy/agda-implementors-meeting-2020.html)

Proposal

◈ PDF ◈ HTML ◈ Slides ◈ translate code ◈ monoid code ◆ Demo

Related

◈ Metaprogramming Agda --- IFIP Program Generation Talk