Safe zero-cost coercions for Haskell

DOI10.1017/S0956796816000150MaRDI QIDQ5371973zbMATH OpenOpenAlexFDO

Authors Joachim Breitner, Richard A. Eisenberg, Stephanie Weirich, Simon Peyton-Jones

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796816000150

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Safe zero-cost coercions for Haskell
• Type-safe cast (functional pearl)
• Generative type abstraction and type-level computation
• Types for Proofs and Programs
• Coercions in a polymorphic type system

Cites work

• \textsc{OutsideIn(X)}: modular type inference with local assumptions
• A church-style intermediate language for ML\(^{\text{F}}\)
• Associated type synonyms
• Associated types with class
• Closed type families with overlapping equations
• Derivable type classes
• GADTs Meet Subtyping
• Generative type abstraction and type-level computation
• On the power of coercion abstraction
• Ott: Effective tool support for the working semanticist
• Safe zero-cost coercions for Haskell
• Typed compilation of inclusive subtyping

Cited in

(4)

• Safe zero-cost coercions for Haskell
• Type-safe cast (functional pearl)
• Efficient lambda encodings for Mendler-style coinductive types in Cedille
• Monotone recursive types and recursive data representations in Cedille

Describes a project that uses

Uses Software

• Ott
• ML
• Haskell
• OCaml
• GHC

This page was built for publication: Safe zero-cost coercions for Haskell

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5371973)