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
- Henry Baker's home page
- Chapter 6 - Linear Lambda Calculus - handouts from Frank Pfennig's course on Linear Logic
- Interpreter of Linear Lambda Calculus in Haskell - by Oleg Kiselyov
- School of Haskell Implementation of Oleg's LLC Interpreter
- A type system for bounded space and functional in-place update
- Linear types and non-size-increasing polynomial time computation
- Linear Type Proposal for Haskell
- A Taste of Linear Logic