Open elpinal opened 3 years ago
I've decided to include "Modular Type Classes" (Dreyer et al. 2006, 2007). It has a formal definition (internal type theory, elaboration and type inference): the internal type theory is a variant of one presented in Dreyer's thesis; the elaboration is HS2000-style translation; the type inference algorithm is an extension of Algorithm W, which is sound with respect to the elaboration (but incomplete). While most work related to type classes is done during the elaboration, meaning that the type theory is not so novel, it syntactically distinguishes projectible modules and non-projectible ones, but has no effect system, meaning that the theory is a bit different from Dreyer's thesis. So it contributes to a new theory. Next, the type theory exploits dependent records rather than dependent pairs, to represent structures: most papers following DCH2003 used dependent pairs, so the theory has some significance. Moreover, the type inference algorithm poses the DB2007 problem. Lastly, this paper confirms the usefulness of HS2000-style elaboration.
Singleton kinds
I've added the following papers.
What about Aspinall's papers?
Definition
Should I include the Definitions?
Books
What about ATTAPL (Chapters 8 and 9) and PFPL (Part XVII)?
Modular implicits
I'm not willing to include it, but I might change my mind in the future.
Module Generation without Regret / Program Generation for ML Modules / Staging beyond terms: prospects and challenges
I'm not willing to include them.
Pending