TY - GEN

T1 - Extensional universal types for call-by-value

AU - Asada, Kazuyuki

N1 - Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.

PY - 2008

Y1 - 2008

N2 - We propose -calculus, which is a second-order polymorphic call-by-value calculus with extensional universal types. Unlike product types or function types in call-by-value, extensional universal types are genuinely right adjoint to the weakening, i.e., β-equality and η-equality hold for not only values but all terms. We give monadic style categorical semantics, so that the results can be applied also to languages like Haskell. To demonstrate validity of the calculus, we construct concrete models for the calculus in a generic manner, exploiting "relevant" parametricity. On such models, we can obtain a reasonable class of monads consistent with extensional universal types. This class admits polynomial-like constructions, and includes non-termination, exception, global state, input/output, and list-non-determinism.

AB - We propose -calculus, which is a second-order polymorphic call-by-value calculus with extensional universal types. Unlike product types or function types in call-by-value, extensional universal types are genuinely right adjoint to the weakening, i.e., β-equality and η-equality hold for not only values but all terms. We give monadic style categorical semantics, so that the results can be applied also to languages like Haskell. To demonstrate validity of the calculus, we construct concrete models for the calculus in a generic manner, exploiting "relevant" parametricity. On such models, we can obtain a reasonable class of monads consistent with extensional universal types. This class admits polynomial-like constructions, and includes non-termination, exception, global state, input/output, and list-non-determinism.

UR - http://www.scopus.com/inward/record.url?scp=58549119552&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=58549119552&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-89330-1_9

DO - 10.1007/978-3-540-89330-1_9

M3 - Conference contribution

AN - SCOPUS:58549119552

SN - 3540893296

SN - 9783540893295

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 122

EP - 137

BT - Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings

PB - Springer Verlag

T2 - 6th Asian Symposium on Programming Languages and Systems, APLAS 2008

Y2 - 9 December 2008 through 11 December 2008

ER -