Thursday, January 18, 2018

Linear Logic, Linear Lisp, Linear Types and Concatenative Languages

I have been revisiting an old gem of a paper by Henry Baker, dating back to 1991, called Lively Linear Lisp -- 'Look Ma, No Garbage!'. This paper came back up on my radar when I realized that the converting from the Lambda Calculus to Cat was closely related to converting to a linear Lambda calculus.

Linear lisp is effectively a version of lisp where each variable is used exactly once. There is a correspondence between the Linear Lisp described by Baker, and Linear Lambda Calculus, and Linear Logic.

My recent realization is that a stack language seems to be effectively a linear language which maps more closely to linear Lambda Calculus that vanilla Lambda Calculus.

Baker points this out in another paper Linear Logic and Permutation Stacks--The Forth Shall Be First. He shows a natural equivalence between a "linear" programming language and a stack machine in which the top items can undergo arbitrary permutations.

After reading Baker's papers, take a look at an informal (but still rigorous) article by Brent Kerby called the Theory of Concatenative Combinators. In it he describes an encoding of the Lambda Calculus in a concatenative language and an algorithm for converting from this encoding to an actual point-free concatenative language.

Linear types are more well known in the area of programming languages. They are a way of enforcing linear properties of certain values in a programming language. Basically a subset of the language is partially linear.

What I am investigating now, is whether the type system of Cat is a linear type system, and if so does it explain why I have been able to devise a higher-order polymorphic type inference algorithm for it, while doing so for the Lambda Calculus remains hard.

Footnote

If you are unfamiliar with Concatenative languages and want a formal introduction I suggest A Foundation for Typed Concatenative Languages, a Master's Thesis by Robert Kleffner

Additional Reading