Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Brief Overview of the Pawns Programming Language

Lee Naish

TL;DR

Pawns tackles the challenge of safely merging pure functional programming with destructive updates and shared mutable state through explicit sharing information and compiler-enforced purity. It introduces mechanisms like dereference-based refs, ! annotations, and pre/postconditions to track updates and sharing, enabling encapsulation of effects inside pure interfaces. The paper presents pure BST construction, destructive-update examples, and a comprehensive sharing-analysis framework, along with a C-FFI path and a renaming facility to manage polymorphism. While still a prototype, Pawns demonstrates how high-level declarative code can co-exist with low-level memory updates without unsafe operations, potentially improving performance for algorithms relying on shared data structures.

Abstract

Pawns is a programming language under development which supports pure functional programming (including algebraic data types, higher order programming and parametric polymorphism) and imperative programming (including pointers, destructive update of shared data structures and global variables), integrated so each can call the other and with purity checked by the compiler. For pure functional code the programmer need not understand the representation of the data structures. For imperative code the representation must be understood and all effects and dependencies must be documented in the code. For example, if a function may update one of its arguments, this must be declared in the function type signature and noted where the function is called. A single update operation may affect several variables due to sharing of representations (pointer aliasing). Pawns code requires all affected variables to be annotated wherever they may be updated and information about sharing to be declared. Annotations are also required where IO or other global variables are used and this must be declared in type signatures as well. Sharing analysis, performed by the compiler, is the key to many aspects of Pawns. It enables us to check that all effects are made obvious in the source code, effects can be encapsulated inside a pure interface and effects can be used safely in the presence of polymorphism.

A Brief Overview of the Pawns Programming Language

TL;DR

Pawns tackles the challenge of safely merging pure functional programming with destructive updates and shared mutable state through explicit sharing information and compiler-enforced purity. It introduces mechanisms like dereference-based refs, ! annotations, and pre/postconditions to track updates and sharing, enabling encapsulation of effects inside pure interfaces. The paper presents pure BST construction, destructive-update examples, and a comprehensive sharing-analysis framework, along with a C-FFI path and a renaming facility to manage polymorphism. While still a prototype, Pawns demonstrates how high-level declarative code can co-exist with low-level memory updates without unsafe operations, potentially improving performance for algorithms relying on shared data structures.

Abstract

Pawns is a programming language under development which supports pure functional programming (including algebraic data types, higher order programming and parametric polymorphism) and imperative programming (including pointers, destructive update of shared data structures and global variables), integrated so each can call the other and with purity checked by the compiler. For pure functional code the programmer need not understand the representation of the data structures. For imperative code the representation must be understood and all effects and dependencies must be documented in the code. For example, if a function may update one of its arguments, this must be declared in the function type signature and noted where the function is called. A single update operation may affect several variables due to sharing of representations (pointer aliasing). Pawns code requires all affected variables to be annotated wherever they may be updated and information about sharing to be declared. Annotations are also required where IO or other global variables are used and this must be declared in type signatures as well. Sharing analysis, performed by the compiler, is the key to many aspects of Pawns. It enables us to check that all effects are made obvious in the source code, effects can be encapsulated inside a pure interface and effects can be used safely in the presence of polymorphism.
Paper Structure (13 sections, 10 figures)

This paper contains 13 sections, 10 figures.

Table of Contents

  1. Introduction
  2. Pure functional programming example - BST creation
  3. Representation and destructive update of values
  4. Destructive update examples
  5. Purity and abstraction
  6. Sharing analysis
  7. IO and state variables
  8. Polymorphism and renaming
  9. Complications
  10. Polymorphism and type safety
  11. Higher order programming
  12. Foreign language interface
  13. Conclusion

Figures (10)

  • Figure 1: BST creation using pure code
  • Figure 2: Destructive update via a ref
  • Figure 3: BST insertion using pure code with pointers
  • Figure 4: BST creation using destructive update
  • Figure 5: Cord operations using destructive update
  • ...and 5 more figures