liboleg-2010.1.10.0: An evolving collection of Oleg Kiselyov's Haskell modules

Language.LinearLC

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.

Synopsis

• newtype F a = F a
• data U = Used
• class LSymantics repr where
• int :: Int -> repr hi hi Int
• add :: repr hi h Int -> repr h ho Int -> repr hi ho Int
• z :: repr (F a, h) (U, h) a
• s :: repr hi ho a -> repr (any, hi) (any, ho) a
• app :: repr hi h (a -> b) -> repr h ho a -> repr hi ho b
• class LinearL repr hi ho where
• lam :: repr (F a, hi) (U, ho) b -> repr hi ho (a -> b)
• newtype R hi ho a = R {
• unR :: hi -> (a, ho)
}
• class HiHo hi ho where
• newtype S hi ho a = S {}
• view :: S () () a -> String
• newtype G a = G a
• class GenL repr hi ho where
• glam :: repr (G a, hi) (G a, ho) b -> repr hi ho (a -> b)
• class GZ repr where
• gz :: repr (G a, hi) (G a, hi) a

# Documentation

newtype F a Source

Constructors

 F a

Instances

 HiHo hi ho => HiHo (F a, hi) (U, ho) HiHo hi ho => HiHo (F a, hi) (F a, ho)

data U Source

Constructors

 Used

Instances

 HiHo hi ho => HiHo (F a, hi) (U, ho)

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

 LSymantics S LSymantics R

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.

Methods

lam :: repr (F a, hi) (U, ho) b -> repr hi ho (a -> b)Source

Instances

 LinearL S hi ho HiHo hi ho => LinearL R hi ho

# tlk = lam (lam z)

newtype R hi ho a Source

Typed and tagless evaluator object term ==> metalanguage value

Constructors

 R FieldsunR :: hi -> (a, ho)

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

class HiHo hi ho whereSource

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.

Methods

hiho :: hi -> hoSource

Instances

 HiHo () () HiHo hi ho => HiHo (G a, hi) (G a, ho) HiHo hi ho => HiHo (F a, hi) (U, ho) HiHo hi ho => HiHo (F a, hi) (F a, ho)

# tl2o_eval = eval tl2o

newtype S hi ho a Source

Another interpreter Literally the same as Symantics.S Although I later decided to print linear lambdas as !x -> ...

Constructors

 S FieldsunS :: [String] -> String

Instances

 GZ S LSymantics S GenL S hi ho LinearL S hi ho

# Exercise: add an affine lambda

newtype G a Source

Extension: the ordinary lam

Constructors

 G a

Instances

 HiHo hi ho => HiHo (G a, hi) (G a, ho)

class GenL repr hi ho whereSource

Methods

glam :: repr (G a, hi) (G a, ho) b -> repr hi ho (a -> b)Source

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

class GZ repr whereSource

Methods

gz :: repr (G a, hi) (G a, hi) aSource

Instances

 GZ S GZ R