Picture of automobile manufacturing plant

Driving innovations in manufacturing: Open Access research from DMEM

Strathprints makes available Open Access scholarly outputs by Strathclyde's Department of Design, Manufacture & Engineering Management (DMEM).

Centred on the vision of 'Delivering Total Engineering', DMEM is a centre for excellence in the processes, systems and technologies needed to support and enable engineering from concept to remanufacture. From user-centred design to sustainable design, from manufacturing operations to remanufacturing, from advanced materials research to systems engineering.

Explore Open Access research by DMEM...

Outrageous but meaningful coincidences : dependent type-safe syntax and evaluation

Mcbride, Conor (2010) Outrageous but meaningful coincidences : dependent type-safe syntax and evaluation. In: Proceedings of the 6th ACM SIGPLAN workshop on Generic programming. ACM, New York, NY, New York, pp. 1-12. ISBN 9781450302517

Full text not available in this repository. Request a copy from the Strathclyde author

Abstract

Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coincidence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontrivial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article constructs a type-safe representation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The KIPLING interpreter example is not merely de rigeur - it is key to the construction. At the heart of the technique is that key component of generic programming, the universe.