Skip to content

PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

License

Notifications You must be signed in to change notification settings

alhassy/next-700-module-systems

Repository files navigation

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

PrototypeMathScheme: 200+ Math Theories in (Clickable) AgdaA Language Feature to Unbundle Data at WillSlidesYoutube

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

PDFHTMLSlidestranslate codemonoid codeDemo

Related

Metaprogramming Agda --- IFIP Program Generation Talk