TY - JOUR
T1 - Eff directly in OCaml
AU - Kiselyov, Oleg
AU - Sivaramakrishnan, K. C.
N1 - Funding Information:
We are very grateful to Andrej Bauer for introducing us to Eff, for patiently explaining Eff features and design decisions, and for writing some of the sample Eff code in §2.1. We thank Kenichi Asai, Yukiyoshi Kameyama and Achim Jung for helpful discussions. Extensive comments and suggestions by anonymous reviewers are greatly appreciated. This work was partially supported by JSPS KAKENHI Grant Number 17K00091.
Publisher Copyright:
© 2018 OPEN PUBLISHING ASSOCIATION. All rights reserved.
PY - 2018/12/31
Y1 - 2018/12/31
N2 - The language Eff is an OCaml-like language serving as a prototype implementation of the theory of algebraic effects, intended for experimentation with algebraic effects on a large scale. We present the embedding of Eff into OCaml, using the library of delimited continuations or the multicore OCaml branch. We demonstrate the correctness of the embedding denotationally, relying on the tagless-final–style interpreter-based denotational semantics, including the novel, direct denotational semantics of multi-prompt delimited control. The embedding is systematic, lightweight, performant and supports even higher-order, ‘dynamic’ effects with their polymorphism. OCaml thus may be regarded as another implementation of Eff, broadening the scope and appeal of that language.
AB - The language Eff is an OCaml-like language serving as a prototype implementation of the theory of algebraic effects, intended for experimentation with algebraic effects on a large scale. We present the embedding of Eff into OCaml, using the library of delimited continuations or the multicore OCaml branch. We demonstrate the correctness of the embedding denotationally, relying on the tagless-final–style interpreter-based denotational semantics, including the novel, direct denotational semantics of multi-prompt delimited control. The embedding is systematic, lightweight, performant and supports even higher-order, ‘dynamic’ effects with their polymorphism. OCaml thus may be regarded as another implementation of Eff, broadening the scope and appeal of that language.
UR - http://www.scopus.com/inward/record.url?scp=85060076709&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85060076709&partnerID=8YFLogxK
U2 - 10.4204/EPTCS.285.2
DO - 10.4204/EPTCS.285.2
M3 - Conference article
AN - SCOPUS:85060076709
VL - 285
SP - 23
EP - 58
JO - Electronic Proceedings in Theoretical Computer Science, EPTCS
JF - Electronic Proceedings in Theoretical Computer Science, EPTCS
SN - 2075-2180
T2 - 2016 ML Family Workshop / OCaml Users and Developers Workshops, ML/OCAML 2016
Y2 - 22 September 2016 through 23 September 2016
ER -