Platonic C# - Managing Referential Transparency through Unique Types

The idea of Platonic C# is to enforce referential transparency within the context of C#, by enforcing a set of rules around defaulting to immutability of data structures and requiring uniqueness of instances of mutable types.

(Comment on this)

Computer History Museum releases PostScript source

The Computer History Museum, in conjunction with Adobe, has released the PostScript source code. Here is the release, with some helpful historical context and several photos:

The story of PostScript has many different facets. It is a story about profound changes in human literacy as well as a story of trade secrets within source code. It is a story about the importance of teams, and of geometry. And it is a story of the motivations and educations of engineer-entrepreneurs.

The Computer History Museum is excited to publicly release, for the first time, the source code for the breakthrough printing technology, PostScript. We thank Adobe, Inc. for their permission and support, and John Warnock for championing this release.

(Comment on this)

The Verse Calculus: a Core Calculus for Functional Logic Programming
The Verse Calculus: a Core Calculus for Functional Logic Programming

https://simon.peytonjones.org/assets/pdfs/verse-conf.pdf

• LENNART AUGUSTSSON, Epic Games, Sweden
• JOACHIM BREITNER
• KOEN CLAESSEN, Epic Games, Sweden
• RANJIT JHALA, Epic Games, USA
• SIMON PEYTON JONES, Epic Games, United Kingdom
• OLIN SHIVERS, Epic Games, USA/li>
• TIM SWEENEY, Epic Games, USA

Functional logic languages have a rich literature, but it is tricky to give them a satisfying semantics. In this
paper we describe the Verse calculus, VC, a new core calculus for functional logical programming. Our main
contribution is to equip VC with a small-step rewrite semantics, so that we can reason about a VC program
in the same way as one does with lambda calculus; that is, by applying successive rewrites to it.

This draft paper describes our current thinking about Verse. It is very much a work in progress, not a finished
product. The broad outlines of the design are stable. However, the details of the rewrite rules may well change; we
think that the current rules are not confluent, in tiresome ways. (If you are knowledgeable about confluence proofs,
please talk to us!)We are eager to enagage in a dialogue with the community. Please do write to us.

(Comment on this)

LtU is now running in a new, more stable environment

LtU has experienced a long period of downtime recently. Its software infrastructure was outdated enough that it became difficult to maintain when problems arose. It has now been migrated to a brand new environment. It should be much more stable from now on.

(Comment on this)

Graydon Hoare: 21 compilers and 3 orders of magnitude in 60 minutes

In 2019, Graydon Hoare gave a talk to undergraduates (PDF of slides) trying to communicate a sense of what compilers looked like from the perspective of people who did it for a living.

I've been aware of this talk for over a year and meant to submit a story here, but was overcome by the sheer number of excellent observations. I'll just summarise the groups he uses:

• The giants: by which he means the big compilers that are built the old-fashioned way that throw massive resources at attaining efficiency
• The variants, which use tricks to avoid being so massive:
  1. Fewer optimisations: be traditional, but be selective and only the optimisations that really pay off
  2. Use compiler-friendly languages, by which he is really taking about languages that are good for implementing compilers, like Lisp and ML
  3. Theory-driven meta-languages, esp. how something like yacc allows a traditional Dragon-book style compiler to be written more easily
  4. Base compiler on a carefully designed IR that is either easy to compile or reasonable to bytecode-interpret
  5. Exercise discretion to have the object code be a mix of compiled and interpreted
  6. Use sophisticated partial evaluation
  7. Forget tradition and implement everything directly by hand

I really recommend spending time working through these slides. While much of the material I was familiar with, enough was new, and I really appreciated the well-made points, shout-outs to projects that deserve more visibility, such as Nanopass compilers and CakeML, and the presentation of the Futamura projections, a famously tricky concept, at the undergraduate level.

(Comment on this)

Latent Effects for Reusable Language Components

Latent Effects for Reusable Language Components, by Birthe van den Berg, Tom Schrijvers, Casper Bach Poulsen, Nicolas Wu:

The development of programming languages can be quite complicated and costly. Hence, much effort has been devoted to the modular definition of language features that can be reused in various combinations to define new languages and experiment with their semantics. A notable outcome of these efforts is the algebra-based “datatypes "a la carte" (DTC) approach. When combined with algebraic effects, DTC can model a wide range of common language features. Unfortunately, the
current state of the art does not cover modular definitions of advanced control-flow mechanisms that defer execution to an appropriate point, such as call-by-name and call-by-need evaluation, as well as (multi-)staging. This paper defines latent effects, a generic class of such control-flow mechanisms. We demonstrate how function abstractions, lazy computations and a MetaML-like staging can all be expressed in a modular fashion using latent effects, and how they can be combined in various ways to obtain complex semantics. We provide a full Haskell implementation of our effects and handlers with a range of examples.

Looks like a nice generalization of the basic approach taken by algebraic effects to more subtle contexts. Algebraic effects have been discussed here on LtU many times. I think this description from section 2.3 is a pretty good overview of their approach:

LE&H is based on a different, more sophisticated structure than AE&H’s free monad. This structure supports non-atomic operations (e.g., function abstraction, thunking, quoting) that contain or delimit computations whose execution may be deferred. Also, the layered handling is different. The idea is still the same, to replace bit by bit the structure of the tree by its meaning. Yet, while AE&H grows the meaning around the shrinking tree, LE&H grows little “pockets of meaning” around the individual nodes remaining in the tree, and not just around the root. The latter supports deferred effects because later handlers can still re-arrange the semantic pockets created by earlier handlers.

(Comment on this)

Introducing PathQuery, Google's Graph Query Language

Introducing PathQuery, Google's Graph Query Language

We introduce PathQuery, a graph query language developed to scale with Google's query and data volumes as well as its internal developer community. PathQuery supports flexible and declarative semantics. We have found that this enables query developers to think in a naturally "graphy" design space and to avoid the additional cognitive effort of coordinating numerous joins and subqueries often required to express an equivalent query in a relational space. Despite its traversal-oriented syntactic style, PathQuery has a foundation on a custom variant of relational algebra -- the exposition of which we presently defer -- allowing for the application of both common and novel optimizations. We believe that PathQuery has withstood a "test of time" at Google, under both large scale and low latency requirements. We thus share herein a language design that admits a rigorous declarative semantics, has scaled well in practice, and provides a natural syntax for graph traversals while also admitting complex graph patterns.

Things that are somewhat interesting to me, from an engineering standpoint:

1. PathQuery has a module/compilation system, enabling re-use of PathQuery modules across projects. (Someone had mentioned that Google has around 40,000 PathQuery modules already, internally...)
2. PathQuery supports native functions so that some query pieces can be evaluated procedurally (peephole optimization)
3. Use of relational algebra to enable a lot of known optimizations, plus future optimizations

Also, from a socio-linguistic perspective, Graph Languages are effectively the new Object-Relational Mapping layer, but they solve an interesting organizational problem of allowing multiple teams to code in different languages, without needing to re-write / re-implement entities and mapping configurations in each language. It's the Old New Thing again...

(Comment on this)

Google announces Logica: organizing your data queries, making them universally reusable and fun

You can read more about it at the Google Open Source blog post, Logica: organizing your data queries, making them universally reusable and fun.

They advocate for datalog-like language they developed internally at Google.

The reason?

Good programming is about creating small, understandable, reusable pieces of logic that can be tested, given names, and organized into packages which can later be used to construct more useful pieces of logic. SQL resists this workflow. Although you can encapsulate certain repeated computations into views and functions, the syntax and support for these can vary among implementations, the notions of packages and imports are generally nonexistent, and higher-level constructions (e.g. passing a function to a function) are impossible.

(Comment on this)

Coq will be renamed

From the Coq-club:

The Coq development team acknowledges the recent discussions (started on the Coq-Club mailing list) around Coq's logo and name.

We wish to thank everyone that participated in these discussions. Testimonies from people who experienced harassment or awkward situations, reports about students (notably women) who ended up not learning / using Coq because of its name, were all very important so that the community could fully recognize the impact of the current name and its slang meaning in English, especially with respect to gender-diversity in the Coq community.

For these reasons, the Coq development team is open to a renaming.

Suggestions for alternative names go here.

(Comment on this)

LAMBDA: The ultimate Excel worksheet function

Post by Andy Gordon and Simon Peyton Jones on LAMBDA giving Excel users the ability to define functions.

Ever since it was released in the 1980s, Microsoft Excel has changed how people organize, analyze, and visualize their data, providing a basis for decision-making for the millions of people who use it each day. It’s also the world’s most widely used programming language. Excel formulas are written by an order of magnitude more users than all the C, C++, C#, Java, and Python programmers in the world combined. Despite its success, considered as a programming language Excel has fundamental weaknesses. Over the years, two particular shortcomings have stood out: (1) the Excel formula language really only supported scalar values—numbers, strings, and Booleans—and (2) it didn’t let users define new functions.

Until now.

(Comment on this)

Google Brain's Jax and Flax

Google's AI division, Google Brain, has two main products for deep learning: TensorFlow and Jax. While TensorFlow is best known, Jax can be thought of as a higher-level language for specifying deep learning algorithms while automatically eliding code that doesn't need to run as part of the model.

Jax evolved from Autograd, and is a combination of Autograd and XLA. Autograd "can automatically differentiate native Python and Numpy code. It can handle a large subset of Python's features, including loops, ifs, recursion and closures, and it can even take derivatives of derivatives of derivatives. It supports reverse-mode differentiation (a.k.a. backpropagation), which means it can efficiently take gradients of scalar-valued functions with respect to array-valued arguments, as well as forward-mode differentiation, and the two can be composed arbitrarily. The main intended application of Autograd is gradient-based optimization."

Flax is then built on top of Jax, and allows for easier customization of existing models.

What do you see as the future of domain specific languages for AI?

(Comment on this)

Tackling the Awkward Squad for Reactive Programming

https://2020.ecoop.org/details/ecoop-2020-papers/19/Tackling-the-Awkward-Squad-for-Reactive-Programming-The-Actor-Reactor-Model

Sam Van den Vonder, Thierry Renaux, Bjarno Oeyen, Joeri De Koster, Wolfgang De Meuter

Reactive programming is a programming paradigm whereby programs are internally represented by a dependency graph, which is used to automatically (re)compute parts of a program whenever its input changes. In practice reactive programming can only be used for some parts of an application: a reactive program is usually embedded in an application that is still written in ordinary imperative languages such as JavaScript or Scala. In this paper we investigate this embedding and we distill “the awkward squad for reactive programming” as 3 concerns that are essential for real-world software development, but that do not fit within reactive programming. They are related to long lasting computations, side-effects, and the coordination between imperative and reactive code. To solve these issues we design a new programming model called the Actor-Reactor Model in which programs are split up in a number of actors and reactors. Actors and reactors enforce a strict separation of imperative and reactive code, and they can be composed via a number of composition operators that make use of data streams. We demonstrate the model via our own implementation in a language called Stella.

(Comment on this)

Built to Last

Mar Hicks. Built to Last. Logic. Issue 11, "Care".

It was this austerity-driven lack of investment in people—rather than the handy fiction, peddled by state governments, that programmers with obsolete skills retired—that removed COBOL programmers years before this recent crisis. The reality is that there are plenty of new COBOL programmers out there who could do the job. In fact, the majority of people in the COBOL programmers’ Facebook group are twenty-five to thirty-five-years-old, and the number of people being trained to program and maintain COBOL systems globally is only growing. Many people who work with COBOL graduated in the 1990s or 2000s and have spent most of their twenty-first century careers maintaining and programming COBOL systems...

In this sense, COBOL and its scapegoating show us an important aspect of high tech that few in Silicon Valley, or in government, seem to understand. Older systems have value, and constantly building new technological systems for short-term profit at the expense of existing infrastructure is not progress. In fact, it is among the most regressive paths a society can take.

Recently, work on the history of technology has been becoming increasingly more sophisticated and moved beyond telling the story of impressive technology to trying to unravel the social, political, and economic forces that affected the development, deployment, and use of a wide range of technologies and technological systems. Luckily, this trend is beginning to manifest itself in studies of the history of programming languages. While not replacing the need for careful, deeply informed, studies of the internal intellectual forces affecting the development of programming languages, these studies add a sorely needed aspect to the stories we tell.

(Comment on this)

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy, Lionel Parreaux, ICFP 2020.

MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand.

There's also an introductory blog post and an online demo.

Stephen Dolan's Algebraic Subtyping (discussion) unexpectedly provided a solution to the problem of combining type inference and subtyping, but used somewhat heavy and unusual machinery. Now Lionel Parreaux shows that the system can be implemented in a very straightforward and pleasing way. Here's to hoping that it makes it into real languages!

(Comment on this)

Applications of Blockchain to Programming Language Theory

Let's talk about Blockchain. Goal is to use this forum topic to highlight its usefulness to programming language theory and practice. If you're familiar with existing research efforts, please share them here. In addition, feel free to generate ideas for how Blockchain could improve languages and developer productivity.

As one tasty example: Blockchain helps to formalize thinking about mutual knowledge and common knowledge, and potentially think about sharing intergalactic computing power through vast distributed computing fabrics. If we can design contracts in such a way that maximizes the usage of mutual knowledge while minimizing common knowledge to situations where you have to "prove your collateral", third-party transactions could eliminate a lot of back office burden. But, there might be benefits in other areas of computer science from such research, as well.

Some language researchers, like Mark S. Miller, have always dreamed of Agoric and the Decades-Long Quest for Secure Smart Contracts.

Some may also be aware that verification of smart contracts is an important research area, because of the notorious theft of purse via logic bug in an Ethereum smart contract.

(Comment on this)

Turnstile+: Dependent Type Systems as Macros

In 2017, a team from Northeastern University released Turnstile, a framework for implementing propositionally typed languages in Racket; cf. naasking's story Type Systems as Macros. The system was really nice because it allowed type systems to be expressed in a manner similar to the way theoretical PL researchers would in a paper, and because it hooked into Racket's clean compiler backend.

Now Stephen Chang, one of that team, together with new coauthors Michael Ballantyne, Usamilo Turner and William Bowman, have released a rewrite that they call Turnstile+, together with a POPL article, Dependent Type Systems as Macros. From that article's introduction:

Turnstile+ represents a major research leap over its predecessor. Specifically, we solve the major challenges necessary to implement dependent types and their accompanying DSLs and extensions (which Turnstile could not support), while retaining the original abilities of Turnstile. For example, one considerable obstacle was the separation between the macro expansion phase and a program’s runtime phase. Since dependently typed languages may evaluate expressions while type checking, checking dependent types with macros requires new macrology design patterns and abstractions for interleaving expansion, type checking, and evaluation. The following summarizes our key innovations.

• Turnstile+ demands a radically different API for implementing a language’s types. It must be straightforward yet expressive enough to represent a range of constructs from base types, to binding forms like Π-types, to datatype definition forms for indexed inductive type families.
• Turnstile+ includes an API for defining type-level computation, which we dub normalization by macro expansion. A programmer writes a reduction rule using syntax resembling familiar on-paper notation, and Turnstile+ generates a macro definition that performs the reduction during macro expansion. This allows easily implementing modular type-level evaluation.
• Turnstile+’s new type API adds a generic type operation interface, enabling modular implementation of features such as error messages, pattern matching, and resugaring. This is particularly important for implementing tools like tactic systems that inspect intermediate type-checking steps and construct partial terms.
• Turnstile+’s core type checking infrastructure requires an overhaul, specifically with first-class type environments, in order to accommodate features like dependent binding structures of the shape[x:τ]...,i.e., telescopes [de Bruijn 1991; McBride 2000].
• Relatedly, Turnstile+’s inference-rule syntax is extended so that operations over telescopes, or premises with references to telescopes, operate as folds instead of as maps </p>

The code is available at https://github.com/stchang/macrotypes.

(Comment on this)

Histogram: You have to know the past to understand the present by Tomas Petricek

Histogram: You have to know the past to understand the present by Tomas Petricek, University of Kent

Programs are created through a variety of interactions. A programmer might write some code, run it interactively to check whether it works, use copy and paste, apply a refactoring or choose an item from an auto-complete list. Programming research often forgets about these and represents programs as the resulting text. Consequently, thinking about such interactions is often out of scope. This essay shifts focus from programs to a more interesting question of programming.

We represent programs as lists of interactions such as triggering an auto-complete and choosing an option, declaring a value, introducing a variable or evaluating a piece of code. We explore a number of consequences of this way of thinking about programs. First, if we create functions by writing concrete code using a sample input and applying a refactoring, we do not lose the sample input and can use it later for debugging. Second, if we treat executing code interactively as an interaction and store the results, we can later use this information to give more precise suggestions in auto-complete. Third, by moving away from a textual representation, we can display the same program as text, but also in a view inspired by spreadsheets. Fourth, we can let programmers create programs by directly interacting with live previews as those interactions can be recorded and as a part of program history.

We discuss the key ideas through examples in a simple programming environment for data exploration. Our focus in this essay is more on principles than on providing fine tuned user experience. We keep our environment more explicit, especially when this reveals what is happening behind the scenes. We aim to show that seeing programs as lists of interactions is a powerful change of perspective that can help us build better programming systems with novel features that make programming easier and more accessible. The data exploration environment in this interactive essay may not yet be that, but it gives a glimpse of the future.

(Comment on this)

Applied Category Theory - The Emerging Science of Compositionality

An enjoyable 25-minute introductory talk: YOW! Lambda Jam 2019 - Ken Scambler - Applied Category Theory (slides)

What do programming, quantum physics, chemistry, neuroscience, systems biology, natural language parsing, causality, network theory, game theory, dynamical systems and database theory have in common?

As functional programmers, we know how useful category theory can be for our work - or perhaps how abstruse and distant it can seem. What is less well known is that applying category theory to the real world is an exciting field of study that has really taken off in just the last few years. It turns out that we share something big with other fields and industries - we want to make big things out of little things without everything going to hell! The key is compositionality, the central idea of category theory.

Previously: Seven Sketches in Compositionality: An Invitation to Applied Category Theory.

(via Brian McKenna)

(Comment on this)

Tensor Considered Harmful

Tensor Considered Harmful, by Alexander Rush

TL;DR: Despite its ubiquity in deep learning, Tensor is broken. It forces bad habits such as exposing private dimensions, broadcasting based on absolute position, and keeping type information in documentation. This post presents a proof-of-concept of an alternative approach, named tensors, with named dimensions. This change eliminates the need for indexing, dim arguments, einsum- style unpacking, and documentation-based coding. The prototype PyTorch library accompanying this blog post is available as namedtensor.

Thanks to Edward Z. Yang for pointing me to this "Considered Harmful" position paper.

(Comment on this)

Seven Sketches in Compositionality: An Invitation to Applied Category Theory
Seven Sketches in Compositionality: An Invitation to Applied Category Theory

2018 by Brendan Fong and David I. Spivak

Category theory is becoming a central hub for all of pure mathematics. It is unmatched in its ability to organize and layer abstractions, to find commonalities between structures of all sorts, and to facilitate communication between different mathematical communities. But it has also been branching out into science, informatics, and industry. We believe that it has the potential to be a major cohesive force in the world, building rigorous bridges between disparate worlds, both theoretical and practical. The motto at MIT is mens et manus, Latin for mind and hand. We believe that category theory—and pure math in general—has stayed in the realm of mind for too long; it is ripe to be brought to hand.

A very approachable but useful introduction to category theory. It avoids the Scylla and Charybdis of becoming incomprehensible after page 2 (as many academic texts do), and barely scratching the surface (as many popular texts do).

(Comment on this)