Paul Downen ; Zena M. Ariola - Compiling With Classical Connectives

lmcs:5663 - Logical Methods in Computer Science, August 28, 2020, Volume 16, Issue 3 -
Compiling With Classical ConnectivesArticle

Authors: Paul Downen ; Zena M. Ariola

    The study of polarity in computation has revealed that an "ideal" programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But this binary choice leaves out call-by-need which is used in practice to implement lazy-by-default languages like Haskell. We show how the notion of polarity can be extended beyond the value/name dichotomy to include call-by-need by adding a mechanism for sharing which is enough to compile a Haskell-like functional language with user-defined types. The key to capturing sharing in this mixed-evaluation setting is to generalize the usual notion of polarity "shifts:" rather than just two shifts (between positive and negative) we have a family of four dual shifts. We expand on this idea of logical duality---"and" is dual to "or;" proof is dual to refutation---for the purpose of compiling a variety of types. Based on a general notion of data and codata, we show how classical connectives can be used to encode a wide range of built-in and user-defined types. In contrast with an intuitionistic logic corresponding to pure functional programming, these classical connectives bring more of the pleasant symmetries of classical logic to the computationally-relevant, constructive setting. In particular, an involutive pair of negations bridges the gulf between the wide-spread notions of parametric polymorphism and abstract data types in programming languages. To complete the study of duality in compilation, we also consider the dual to call-by-need evaluation, which shares the computation within the control flow of a program instead of computation within the information flow.

    Volume: Volume 16, Issue 3
    Published on: August 28, 2020
    Accepted on: June 20, 2020
    Submitted on: August 1, 2019
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages
      Source : OpenAIRE Graph
    • SHF: Small: SEQUBE: A Sequent Calculus Foundation for High- Level and Intermediate Programming Languages; Funder: National Science Foundation; Code: 1423617
    • SHF: SMALL: Intermediate Languages for Safe and Efficient Compilation; Funder: National Science Foundation; Code: 1719158

    Consultation statistics

    This page has been seen 1571 times.
    This article's PDF has been downloaded 518 times.