Search for: All records

Recursion and induction are mature, well-understood topics in programming. Yet their duals, co-recursion and co-induction, are still exotic and underdeveloped programming features. We aim to put them on equal footing by giving a foundation for co-recursion based on computation, analogous to the original computational foundation of recursion. At the lower level, we show how the connection between the two can be strengthened through their implementation details in an abstract machine. At the higher level, we develop a syntactic equational theory for inductive and co-inductive reasoning based on control flow. We also observe the impact of evaluation strategy: call-by-name has efficient recursion and strong co-inductive reasoning, but call-by-value has efficient co-recursion and strong inductive reasoning. 

A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is a pain for compilers tasked with producing efficient code that manipulates concrete values. This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself. 

Computer scientists are well-versed in dealing with data structures. The same cannot be said about their dual: codata. Even though codata is pervasive in category theory, universal algebra, and logic, the use of codata for programming has been mainly relegated to representing infinite objects and processes. Our goal is to demonstrate the benefits of codata as a general-purpose programming abstraction independent of any specific language: eager or lazy, statically or dynamically typed, and functional or object-oriented. While codata is not featured in many programming languages today, we show how codata can be easily adopted and implemented by offering simple inter-compilation techniques between data and codata. We believe codata is a common ground between the functional and object-oriented paradigms; ultimately, we hope to utilize the Curry-Howard isomorphism to further bridge the gap. 

Abstract We present a model of computation that heavily emphasizes the concept of duality and the interaction between opposites–production interacts with consumption. The symmetry of this framework naturally explains more complicated features of programming languages through relatively familiar concepts. For example, binding a value to a variable is dual to manipulating the flow of control in a program. By looking at the computational interpretation of the sequent calculus, we find a language that lets us speak about duality, control flow, and evaluation order in programs as first-class concepts. We begin by reviewing Gentzen's LK sequent calculus and show how the Curry–Howard isomorphism still applies to give us a different basis for expressing computation. We then illustrate how the fundamental dilemma of computation in the sequent calculus gives rise to a duality between evaluation strategies : strict languages are dual to lazy languages. Finally, we discuss how the concept of focusing , developed in the setting of proof search, is related to the idea of type safety for computation expressed in the sequent calculus. In this regard, we compare and contrast two different methods of focusing that have appeared in the literature, static and dynamic focusing, and illustrate how they are two means to the same end.