Notes on subtle papers

[elpinal]

Singleton kinds

I've added the following papers.

• Deciding type equivalence in a language with singleton kinds (POPL, January 2000) https://doi.org/10.1145/325694.325724
  • Deciding Type Equivalence in a Language with Singleton Kinds (techreport, September 1999, CMU-CS-99-155) http://reports-archive.adm.cs.cmu.edu/anon/1999/abstracts/99-155.html
• Sound and Complete Elimination of Singleton Kinds (Types in Compilation, September 2000) https://www.springer.com/gp/book/9783540421962
  • Sound and Complete Elimination of Singleton Kinds (techreport, January 2000, CMU-CS-00-104) http://reports-archive.adm.cs.cmu.edu/anon/2000/abstracts/00-104.html
• Singleton Kinds and Singleton Types (Ph.D. Thesis, August 2000, CMU-CS-00-153) http://reports-archive.adm.cs.cmu.edu/anon/2000/abstracts/00-153.html
• Implementing the TILT Internal Language (techreport, December 2000, CMU-CS-00-180) http://reports-archive.adm.cs.cmu.edu/anon/2000/abstracts/00-180.html
• Extensional equivalence and singleton types (Transactions on Computational Logic, 2006) https://doi.org/10.1145/1183278.1183281
• Sound and complete elimination of singleton kinds (Transactions on Computational Logic, 2007) https://doi.org/10.1145/1227839.1227840
• A syntactic account of singleton types via hereditary substitution (LFMTP 2009) https://doi.org/10.1145/1577824.1577829

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

• Type sharing constraints and undecidability (Narbel 2007)
• Non-reformist reform for Haskell Modularity (Kilpatrick 2019)
• Modules and Persistence in Standard ML (Harper 1986)
• A Secure Compiler for ML Modules (Larmuseau et al. 2015)
• Call-by-Value Semantics for Mutually Recursive First-Class Modules (Rohloff and Lorenzen 2012)
• The Next 700 Module Systems (Al-hassy 2019)
• An implementation of an advanced module system in Caml Light (Pottier 1995)
• Rossberg's old papers
• Dule
• A theory of mixin modules: algebraic laws and reduction semantics (Ancona and Zucca 2002)
• Rigid Mixin Modules (Hirschowitz 2004)
• Program Units as Higher-Order Modules (Flatt and Felleisen 1998)
• Thesis Proposal: Effective Type Theory for Modularity (Dreyer 2002): Unpublished manuscript, November 2002
• Efficient recursion in the presence of effects (Dreyer et al. 2003)
• Type-Safe Linking with Recursive DLLs and Shared Libraries (Duggan 2002)
• An implementation of Standard ML modules (MacQueen 1988)
• Higher-order Functors and Principal Signatures in Standard ML (Birkedal 1993)

[elpinal]

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.