Created
October 18, 2014 07:45
-
-
Save silky/9dece881155df191f4a4 to your computer and use it in GitHub Desktop.
linear type things, from - http://okmij.org/ftp/tagless-final/course/LinearLC.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE NoMonomorphismRestriction #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
-- * 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. | |
module LinearLC where | |
newtype F a = F a -- actual variable | |
data U = Used | |
-- 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. | |
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 | |
-- 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. | |
class LinearL repr hi ho where | |
lam :: repr (F a,hi) (U,ho) b -> repr hi ho (a->b) | |
-- * Sample terms and their inferred types | |
tl1 = add (int 1) (int 2) | |
-- tl1 :: (LSymantics repr) => repr hi hi Int | |
-- * tl2 = lam (add z z) | |
-- This term is not linear | |
-- Couldn't match expected type `U' against inferred type `F a' | |
-- Expected type: repr (U, hi) (U, ho) Int | |
-- Inferred type: repr (F a, h) (U, h) a | |
-- In the second argument of `add', namely `z' | |
-- In the first argument of `lam', namely `(add z z)' | |
tl2o = lam (add z (s z)) | |
-- tl2o :: (LSymantics repr) => repr (F Int, h) (U, h) (Int -> Int) | |
-- The term is open. It can still be written | |
-- * tlk = lam (lam z) | |
-- The outer lam's argument is not consumed | |
-- Couldn't match expected type `F a' against inferred type `U' | |
-- Expected type: repr (F a1, (F a, hi)) (U, (U, ho)) b | |
-- Inferred type: repr (F a1, (U, hi)) (U, (U, hi)) a1 | |
-- In the first argument of `lam', namely `z' | |
-- In the first argument of `lam', namely `(lam z)' | |
tl3 = lam (add (app z (int 1)) (int 2)) | |
-- tl3 :: (LSymantics repr) => repr hi hi ((Int -> Int) -> Int) | |
tl4 = lam (lam (add z (s z))) | |
-- tl4 :: (LSymantics repr) => repr hi hi (Int -> Int -> Int) | |
tl5 = lam (app (lam z) z) | |
-- tl5 :: (LSymantics repr) => repr hi hi (a -> a) | |
tl7 = lam (z `app` lam z) | |
-- * // | |
-- * Typed and tagless evaluator | |
-- * object term ==> metalanguage value | |
newtype R hi ho a = R{unR :: hi -> (a,ho)} | |
instance LSymantics R where | |
int x = R $ \hi -> (x,hi) | |
add e1 e2 = R $ \hi -> | |
let (v1,h) = unR e1 hi | |
(v2,ho) = unR e2 h | |
in (v1+v2,ho) | |
z = R $ \(F x,h) -> (x,(Used,h)) | |
s v = R $ \(any,hi) -> | |
let (x,ho) = unR v hi | |
in (x,(any,ho)) | |
app e1 e2 = R $ \hi -> | |
let (v1,h) = unR e1 hi | |
(v2,ho) = unR e2 h | |
in (v1 v2,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. | |
class HiHo hi ho where | |
hiho :: hi -> ho | |
instance HiHo () () where | |
hiho = id | |
instance HiHo hi ho => HiHo (F a,hi) (F a,ho) where | |
hiho (x,hi) = (x,hiho hi) | |
instance HiHo hi ho => HiHo (U,hi) (U,ho) where | |
hiho (x,hi) = (x,hiho hi) | |
instance HiHo hi ho => HiHo (F a,hi) (U,ho) where | |
hiho (x,hi) = (Used,hiho hi) | |
instance HiHo hi ho => LinearL R hi ho where | |
lam e = R $ \hi -> (f hi, hiho hi) | |
where f hi x = let (v,_) = unR e (F x,hi) | |
in v | |
-- The implementation of lam shows that the value of lam, which is | |
-- f hi, is the closure of the (input) environment in which | |
-- lam was produced. | |
eval e = fst $ unR e () -- Eval in the empty environment | |
tl1_eval = eval tl1 | |
-- 3 | |
-- * tl2o_eval = eval tl2o | |
-- Cannot evaluate an open term | |
-- Couldn't match expected type `()' | |
-- against inferred type `(F Int, h)' | |
-- Expected type: R () b a | |
-- Inferred type: R (F Int, h) (U, h) (Int -> Int) | |
-- In the first argument of `eval', namely `tl2o' | |
-- tl3 = lam (add (app z (int 1)) (int 2)) | |
tl3_eval = eval tl3 | |
-- tl3_eval :: (Int -> Int) -> Int | |
tl3_eval' = tl3_eval succ | |
-- 4 | |
tl4_eval = eval tl4 | |
-- tl4_eval :: Int -> Int -> Int | |
tl4_eval' = tl4_eval 19 35 | |
-- 54 | |
tl5_eval = eval tl5 | |
-- tl5_eval :: a -> a | |
tl5_eval' = tl5_eval True | |
-- True | |
tl7_eval = eval tl7 | |
-- tl7_eval :: ((b1 -> b1) -> b) -> b | |
tl7_eval' = tl7_eval ($ 1) | |
-- 1 | |
-- * // | |
-- Another interpreter | |
-- * Literally the same as Symantics.S | |
-- Although I later decided to print linear lambdas as \!x -> ... | |
newtype S hi ho a = S{unS :: [String] -> String} | |
instance LSymantics S where | |
int x = S $ const $ show x | |
add e1 e2 = S $ \h -> | |
"(" ++ unS e1 h ++ "+" ++ unS e2 h ++ ")" | |
z = S $ \(x:_) -> x | |
s v = S $ \(_:h) -> unS v h | |
app e1 e2 = S $ \h -> | |
"(" ++ unS e1 h ++ " " ++ unS e2 h ++ ")" | |
instance LinearL S hi ho where | |
lam e = S $ \h -> | |
let x = "x" ++ show (length h) | |
in "(\\!" ++ x ++ " -> " ++ unS e (x:h) ++ ")" | |
view :: S () () a -> String | |
view e = unS e [] | |
tl1_view = view tl1 | |
-- "(1+2)" | |
-- * tl2o_view = view tl2o | |
-- Open terms can't be viewed | |
tl3_view = view tl3 | |
-- "(\\!x0 -> ((x0 1)+2))" | |
tl4_view = view tl4 | |
-- "(\\!x0 -> (\\!x1 -> (x1+x0)))" | |
tl5_view = view tl5 | |
-- "(\\!x0 -> ((\\!x1 -> x1) x0))" | |
tl7_view = view tl7 | |
-- "(\\!x0 -> (x0 (\\!x1 -> x1)))" | |
-- * Exercise: add an affine lambda | |
-- * // | |
-- * Extension: the ordinary lam | |
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 | |
-- Now, non-linear terms like tl2 and the K combinator | |
-- become expressible | |
tg2 = glam (add gz gz) | |
-- tg2 :: (GZ repr, LSymantics repr, GenL repr hi hi) => | |
-- repr hi hi (Int -> Int) | |
-- The K combinator is expressible in two ways | |
tgk = glam (glam gz) | |
-- tgk :: (GZ repr, GenL repr (G a1, hi) (G a1, hi), GenL repr hi hi) => | |
-- repr hi hi (a1 -> a -> a) | |
tgk' = glam (lam z) | |
-- tgk' :: (LSymantics repr, | |
-- LinearL repr (G a1, hi) (G a1, hi), | |
-- GenL repr hi hi) => | |
-- repr hi hi (a1 -> a -> a) | |
-- Mixing linear and non-linear lambdas | |
tg4 = glam (lam (add (s gz) (add z (s gz)))) | |
-- tg4 :: (GZ repr, | |
-- LSymantics repr, | |
-- LinearL repr (G Int, hi) (G Int, hi), | |
-- GenL repr hi hi) => | |
-- repr hi hi (Int -> Int -> Int) | |
tg5 = glam (app (lam z) gz) | |
-- 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)) | |
tg71 = glam (app gz (lam z)) | |
-- tg71:: repr hi hi (((a -> a) -> b) -> b) | |
-- 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 | |
tg72 = lam (glam (app gz (s z))) | |
-- tg72:: repr hi hi (a -> (a -> b) -> b) | |
tg73 = glam (lam (app (s gz) z)) | |
-- repr hi hi ((a -> b) -> a -> b) | |
tg74 = lam (lam (app (s z) z)) | |
-- repr hi hi ((a -> b) -> a -> b) | |
-- * // | |
-- * We extend the interpreters | |
instance HiHo hi ho => GenL R hi ho where | |
glam e = R $ \hi -> (f hi, hiho hi) | |
where f hi x = let (v,_) = unR e (G x,hi) | |
in v | |
instance GZ R where | |
gz = R $ \(G x,h) -> (x,(G x,h)) | |
instance HiHo hi ho => HiHo (G a,hi) (G a,ho) where | |
hiho (x,hi) = (x,hiho hi) | |
tg2_eval = eval tg2 27 | |
-- 54 | |
tgk_eval = eval tgk "abc" "cde" | |
tgk'_eval = eval tgk' "abc" "cde" | |
tg4_eval = eval tg4 20 2 | |
-- 42 | |
tg5_eval = eval tg5 True | |
-- True | |
tg72_eval = eval tg72 4 succ | |
--5 | |
tg73_eval = eval tg73 succ 4 | |
-- 5 | |
tg74_eval = eval tg74 succ 4 | |
-- 5 | |
-- * // | |
-- * We extend the S interpreter | |
instance GZ S where | |
gz = S $ \(x:_) -> x | |
instance GenL S hi ho where | |
glam e = S $ \h -> | |
let x = "y" ++ show (length h) | |
in "(\\" ++ x ++ " -> " ++ unS e (x:h) ++ ")" | |
tg2_view = view tg2 | |
-- "(\\y0 -> (y0+y0))" | |
tgk_view = view tgk | |
-- "(\\y0 -> (\\y1 -> y1))" | |
tgk'_view = view tgk' | |
-- "(\\y0 -> (\\!x1 -> x1))" | |
tg4_view = view tg4 | |
-- "(\\y0 -> (\\!x1 -> (y0+(x1+y0))))" | |
tg5_view = view tg5 | |
-- "(\\y0 -> ((\\!x1 -> x1) y0))" | |
main = do | |
print tl1_eval | |
print tl3_eval' | |
print tl4_eval' | |
print tl5_eval' | |
print tl7_eval' | |
print tl1_view | |
print tl3_view | |
print tl4_view | |
print tl5_view | |
print tl7_view | |
print tg2_eval | |
print tgk_eval | |
print tgk'_eval | |
print tg4_eval | |
print tg5_eval | |
print tg2_view | |
print tgk_view | |
print tgk'_view | |
print tg4_view | |
print tg5_view |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment