I submitted a paper entitled Fake it until they make it: Implementing Substructural Type-Systems for EDSLs using Dependent Types to Type-Driven Development ‘18
I have decided to uploaded the abstract here so that my attempt is a least indexable by the great machine spirit in the web—Hallowed be thy API. Given time I will also upload a copy of the paper to ArXiV.
The paper’s abstract was:
Many substructural type-systems are presented for general purpose languages, reasoning about structural rules referencing memory access, and variable usage. When looking to design Embedded Domain Specific Languages (EDSLs) we utilise the host language’s functionality to reason about, and provide, domain specific properties. If the host language does support substructural typing, the substructural rules are specific to the general purpose host language. We build upon existing work that utilises parameterised monads and dependent types when implementing substructural type-systems for EDSLs where the host language does not support omain specific, nor customisation of, substructural type-systems. We extend this work to use De Bruijn indices as proofs of existence that a language’s substructural properties hold. Further, we present two exemplar languages that illustrate the technique’s core principles and how dependent types provide correctness guarantees that our EDSL programs are well-typed.