Inferring Type Isomorphisms Generically

Abstract. Datatypes which differ inessentially in their names and structure are said to be isomorphic; for example, a ternary product is isomorphic to a nested pair of binary products. In some canonical cases, the conversion function is uniquely determined solely by the two types involved. In this article we describe and implement a program in Generic Haskell which automatically infers this function by normalizing types w.r.t. an algebraic theory of canonical isomorphisms. A simple generalization of this technique also allows to infer some non-invertible coercions such as projections, injections and ad hoc coercions between base types. We explain how this technique has been used to drastically improve the usability of a Haskell–XML Schema data binding, and suggest how it might be applied to improve other type-safe language embeddings.

• Type: Conference
• Year: 2004
• Where: MPC
• Authors: Frank Atanassow, Johan Jeuring
• Keywords: Ad Hoc Coercions, Canonical Cases, Mathematics, MPC 2004, Type-safe Language Embeddings