TY - JOUR
T1 - Generating code with polymorphic let a ballad of value restriction, copying and sharing
AU - Kiselyov, Oleg
N1 - Funding Information:
I thank Jacques Garrigue and Atsushi Igarashi for many helpful discussions. Comments and suggestions by Yukiyoshi Kameyama and anonymous reviewers are gratefully appreciated. This work was partially supported by JSPS KAKENHI Grant Numbers 22300005, 25540001, 15H02681.
Publisher Copyright:
© 2017, Open Publishing Association. All rights reserved.
PY - 2017/2/7
Y1 - 2017/2/7
N2 - Getting polymorphism and effects such as mutation to live together in the same language is a tale worth telling, under the recurring refrain of copying vs. sharing. We add new stanzas to the tale, about the ordeal to generate code with polymorphism and effects, and be sure it type-checks. Generating well-typed-by-construction polymorphic let-expressions is impossible in the Hindley-Milner type system: even the author believed that. The polymorphic-let generator turns out to exist. We present its derivation and the application for the lightweight implementation of quotation via a novel and unexpectedly simple source-to-source transformation to code-generating combinators. However, generating let-expressions with polymorphic functions demands more than even the relaxed value restriction can deliver. We need a new deal for let-polymorphism in ML. We conjecture the weaker restriction and implement it in a practically-useful code-generation library. Its formal justification is formulated as the research program.
AB - Getting polymorphism and effects such as mutation to live together in the same language is a tale worth telling, under the recurring refrain of copying vs. sharing. We add new stanzas to the tale, about the ordeal to generate code with polymorphism and effects, and be sure it type-checks. Generating well-typed-by-construction polymorphic let-expressions is impossible in the Hindley-Milner type system: even the author believed that. The polymorphic-let generator turns out to exist. We present its derivation and the application for the lightweight implementation of quotation via a novel and unexpectedly simple source-to-source transformation to code-generating combinators. However, generating let-expressions with polymorphic functions demands more than even the relaxed value restriction can deliver. We need a new deal for let-polymorphism in ML. We conjecture the weaker restriction and implement it in a practically-useful code-generation library. Its formal justification is formulated as the research program.
UR - http://www.scopus.com/inward/record.url?scp=85018903133&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85018903133&partnerID=8YFLogxK
U2 - 10.4204/EPTCS.241.1
DO - 10.4204/EPTCS.241.1
M3 - Conference article
AN - SCOPUS:85018903133
SN - 2075-2180
VL - 241
SP - 1
EP - 22
JO - Electronic Proceedings in Theoretical Computer Science, EPTCS
JF - Electronic Proceedings in Theoretical Computer Science, EPTCS
T2 - 2015 ML Family / OCaml Users and Developers Workshops, ML 2015
Y2 - 3 September 2015 through 4 September 2015
ER -