Language.LinearLC
Contents
Description
Typed tagless-final interpreters for Linear Lambda Calculus de Bruijn indices
Linear lambda-calculus: each bound variable is referenced exactly once.
Application: natural language semantics: (see for example, works by Michael Moortgat) In particular, linear lambda calculi are extensively used in Abstract Categorial Grammars.
The following code would look better in ML: we can declare types F and U in a signature. They will be assumed distinct. Yet an implementation of the signature may conflate the F and U types; therefore, we can use the interpreter for the ordinary lambda calculus. Alas, this approach doesn't work for Haskell: If we use associated types to model type-class local types F and U, the type checker does not consider them necessarily distinct and generates equality constraint. That breaks the abstraction! Terms like tl2 below would not be rejected.
http://okmij.org/ftp/tagless-final/course/course.html#linear
Documentation
Constructors
| F a |
class LSymantics repr whereSource
This semantics assumes that all values (that is, substitutable things) are closed terms. This is the case in CBV or CBN calculi, which never evaluate under lambda. Therefore, we do not qualify the types of values by the env Otherwise, we have to qualify each type such as Int or a with its env. For the unextended linear lambda calculus below, we don't need to make this restriction as substitution of linear terms into linear terms doesn't violate the linearity. But that property is not stated syntactically below. Stating it syntactically does seem possible, but the code becomes quite more complex.
Methods
int :: Int -> repr hi hi IntSource
add :: repr hi h Int -> repr h ho Int -> repr hi ho IntSource
z :: repr (F a, h) (U, h) aSource
s :: repr hi ho a -> repr (any, hi) (any, ho) aSource
app :: repr hi h (a -> b) -> repr h ho a -> repr hi ho bSource
Instances
class LinearL repr hi ho whereSource
The reason we separate out lam is to expose the type variables
hi and ho in the class head. A particular instance might be able to attach
constraints to hi and ho. The instance for the R interpreter
indeed attaches the HiHo constraint.
tl2 = lam (add z z)
tlk = lam (lam z)
Typed and tagless evaluator object term ==> metalanguage value
Instances
| GZ R | |
| LSymantics R | |
| HiHo hi ho => GenL R hi ho | Now, non-linear terms like tl2 and the K combinator become expressible The following does not type-check, although it is `morally correct' Syntactically, the term is non-linear! The linear calculus without extensions did not have the problem of being too conservative: a function cannot avoid using its argument. So, a term that is syntactically linear is semantically linear, and vice versa. It is only when we added general lambdas that the calculus became conservative: a function like the K combinator can disregard its argument expression. So, a term that is syntactically non-linear may still end up using each argument expression once. In general, we have to evaluate it to see it. tg6 = lam ((tgk `app` z) `app` (add (int 1) z)) the following are OK because we never evaluate under lambda All values are always closed terms. Therefore, even though a non-linear function may replicate its arguments, it replicates values -- never variables We extend the interpreters |
| HiHo hi ho => LinearL R hi ho |
Interpreting lam is quite more different Why? Why the simple approach does not work? We need to produce ho when the lambda-form is produced, not when it is applied. But ho of the lambda-form includes the ho for the body of lambda. The latter is the result of evaluating the body; but we get to evaluate the body of the lambda only when the lambda-form is applied. But we need that ho now. Fortunately, types are enough to produce ho. That's the purpose for the type class HiHo.
tl2o_eval = eval tl2o
Another interpreter Literally the same as Symantics.S Although I later decided to print linear lambdas as !x -> ...
tl2o_view = view tl2o
Exercise: add an affine lambda
Extension: the ordinary lam
Constructors
| G a |
class GenL repr hi ho whereSource
Instances
| GenL S hi ho | |
| HiHo hi ho => GenL R hi ho | Now, non-linear terms like tl2 and the K combinator become expressible The following does not type-check, although it is `morally correct' Syntactically, the term is non-linear! The linear calculus without extensions did not have the problem of being too conservative: a function cannot avoid using its argument. So, a term that is syntactically linear is semantically linear, and vice versa. It is only when we added general lambdas that the calculus became conservative: a function like the K combinator can disregard its argument expression. So, a term that is syntactically non-linear may still end up using each argument expression once. In general, we have to evaluate it to see it. tg6 = lam ((tgk `app` z) `app` (add (int 1) z)) the following are OK because we never evaluate under lambda All values are always closed terms. Therefore, even though a non-linear function may replicate its arguments, it replicates values -- never variables We extend the interpreters |