Safe zero-cost coercions for Haskell

Generative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for...

Full description

Saved in:
Bibliographic Details
Published in:Journal of functional programming 2016-01, Vol.26, Article e15
Main Authors: BREITNER, JOACHIM, EISENBERG, RICHARD A., PEYTON JONES, SIMON, WEIRICH, STEPHANIE
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Generative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.
ISSN:0956-7968
1469-7653
DOI:10.1017/S0956796816000150