In general org files in the top level are named by topic and offer code and commentary in a presentation or top to bottom reading style. Fuller examples and derivations are to be found the examples project. Other projects around effects are intended for more engineering focussed exploration of libraries and frameworks.
An opiniated tour of the territory I’ve covered so far (or in the process of). It might be nice to use this as a starting point for discussion on the direction and relevance of various topics.
- B3 Intro to categories and algebra of types
What’s a monoid, fucntor, natural transformation? How do they play out in Haskell? ,onoidial and functorial categories.
- I1 Effects up to Free monads
How effects are modelled in pure languages; T-programs; Kleisli and monads; Free construction and why we care; Issues and directions for effects frameworks; eDSLs as a paradigm; Categories for the working programmer. (1Hr)
- I2 Data types a la carte etc.
Type level programming in Haskell; Nominal vs. structural types; Where are the types?; The expression problem; deep and shallow; Free monads again. (1Hr)
- I3 Finally tagless upto expression problem
What if I can’t/won’t do fancy type wrangling. How has the expression problem been solved in Haskell98? (45 mins)
- B4 Compiling to Categories - Conal Elliott
Lambda Jam 2017 Demonational Design YouTube channel
Conal Elliott’s work on transforming the typed lambda calculus (Haskell) by eliminating lambda (and thus being able to overload it) into Cartesian Closed Categories and then re-interpreting the CCC into hardware, gpu etc. etc.
- I5 Algebraic and denotational design (TBS)
Following Conal Elliott and Sandy Maguire and taking denotational semantics seriously. What are the implications for correct software and the engineering discipline?
- I6 More tagless; even final! (TBS)
More masterful tagless and final embeddings of sophisticated DSLs from Oleg.
- B1 Programming language theory - 101 (Self Study)
Lambda calculus up to simply typed LC; evaluation strategies etc.; Introduction to Wadler’s PLT course in Agda (upto Part 2).
- B2 The Lambda Cube (TBS)
The landscape of typing theories up to calculus of constructions; what are the choices and trade offs of the typing regime?
- I4 Dependent types etc. (In Preparation)
Per-Martin Löf Type Theory and Intuitionistic logic, propositions as types and programs as proof; Proof relevance, equality type; Issues in logic; Agda, Idris.
- A2. Homotopy Type Theory (TBS)
Higher dimensional types, cubical type theory and the Univalence axiom.