next-700-module-systems
next-700-module-systems copied to clipboard
alhassy
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
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
alhassy