Embedding session types in Haskell

Sam Lindley, J. Garrett Morris

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Citations (Scopus)

Abstract

We present a novel embedding of session-typed concurrency in Haskell. We extend an existing HOAS embedding of linear λ-calculus with a set of core session-typed primitives, using indexed type families to express the constraints of the session typing discipline. We give two interpretations of our embedding, one in terms of GHC’s built-in concurrency and another in terms of purely functional continuations. Our safety guarantees, including deadlock freedom, are assured statically and introduce no additional runtime overhead.

Original languageEnglish
Title of host publicationHaskell 2016: Proceedings of the 9th International Symposium on Haskell
EditorsGeoffrey Mainland
PublisherAssociation for Computing Machinery
Pages133-145
Number of pages13
ISBN (Print)9781450344340
DOIs
Publication statusPublished - Sep 2016
Event9th International Symposium on Haskell 2016 - Nara, Japan
Duration: 22 Sep 201623 Sep 2016

Conference

Conference9th International Symposium on Haskell 2016
CountryJapan
CityNara
Period22/09/1623/09/16

Keywords

  • Embedded languages
  • Linear types
  • Session types

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Computer Vision and Pattern Recognition
  • Computer Science Applications
  • Software
  • Human-Computer Interaction

Cite this