Embedding session types in Haskell

Sam Lindley; J. Garrett  Morris

doi:10.1145/2976002.2976018

Embedding session types in Haskell

Sam Lindley, J. Garrett Morris

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English
Title of host publication	Haskell 2016 Proceedings of the 9th International Symposium on Haskell
Publisher	ACM
Pages	133-145
Number of pages	13
ISBN (Electronic)	978-1-4503-4434-0
DOIs	https://doi.org/10.1145/2976002.2976018
Publication status	Published - 8 Sep 2016
Event	2016 Proceedings of the 9th International Symposium on Haskell - Nara, Japan Duration: 18 Sep 2016 → 24 Sep 2016 https://conf.researchr.org/home/icfp-2016/

Publication series

Name	ACM SIGPLAN Notices
Publisher	ACM
Number	12
Volume	51
ISSN (Print)	0362-1340
ISSN (Electronic)	1558-1160

Conference

Conference	2016 Proceedings of the 9th International Symposium on Haskell
Abbreviated title	ICFP'16
Country/Territory	Japan
City	Nara
Period	18/09/16 → 24/09/16
Internet address	https://conf.researchr.org/home/icfp-2016/

Access to Document

10.1145/2976002.2976018

gvhsAccepted author manuscript, 356 KB

http://dl.acm.org/citation.cfm?id=2976018

From Data Types to Session Types - A Basis for Concurrency and Distribution
Wadler, P.
EPSRC
20/05/13 → 19/11/20
Project: Research

Cite this

@inproceedings{d19cc4059940448aa617fb6adad4e3fc,

title = "Embedding session types in Haskell",

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{\textquoteright}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.",

author = "Sam Lindley and Morris, {J. Garrett}",

year = "2016",

month = sep,

day = "8",

doi = "10.1145/2976002.2976018",

language = "English",

series = "ACM SIGPLAN Notices",

publisher = "ACM",

number = "12",

pages = "133--145",

booktitle = "Haskell 2016 Proceedings of the 9th International Symposium on Haskell",

note = "2016 Proceedings of the 9th International Symposium on Haskell, ICFP'16 ; Conference date: 18-09-2016 Through 24-09-2016",

url = "https://conf.researchr.org/home/icfp-2016/",

}

TY - GEN

T1 - Embedding session types in Haskell

AU - Lindley, Sam

AU - Morris, J. Garrett

PY - 2016/9/8

Y1 - 2016/9/8

N2 - 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.

AB - 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.

U2 - 10.1145/2976002.2976018

DO - 10.1145/2976002.2976018

M3 - Conference contribution

T3 - ACM SIGPLAN Notices

SP - 133

EP - 145

BT - Haskell 2016 Proceedings of the 9th International Symposium on Haskell

PB - ACM

T2 - 2016 Proceedings of the 9th International Symposium on Haskell

Y2 - 18 September 2016 through 24 September 2016

ER -

Embedding session types in Haskell

Abstract

Publication series

Conference

Access to Document

Projects

From Data Types to Session Types - A Basis for Concurrency and Distribution

Cite this