Linear Lambda Calculus in Agda

Posted on 2018-07-12 by Oleg Grenrus linear, agda

Haskell by day, Agda by Night.

In comparison with other implementation found by googling this approach feels simpler.

Philip Wadler wrote a paper A taste of linear logic (1993), if you want to learn what this is about.

You can compare the code below with Oleg Kiselyov's LinearLC.hs, or with Embedding a Full Linear Lambda Calculus in Haskell by Jeff Polakow (Available via OpenTOC) and Embedding session types in Haskell by Sam Lindley and J. Garrett Morris (Available via OpenTOC). (Note: my encoding isn't HOAS, but uses de Bruijn indices; encodings above are HOAS, but also use de Bruijn indices to track linearity).

This time it's only code, your comments welcome: reply to my tweet, email me or find me on IRC (phadej on Freenode).

-- An encoding of Linear Lambda Calculus
--
-- The idea is from Conor McBride's /I Got Plenty o’ Nuttin’/
-- The variables stay in the context,
-- but "consuming" them uses their multiplicity.
module LLC where

open import Data.Nat
open import Data.List

-- Types
data Ty : Set where
  A   : Ty  -- "atomic" propositions
  __ : Ty  Ty  Ty
  __ : Ty  Ty  Ty

infixr 0 __
infixr 1 __

-- None-One-Tons Rig
data R : Set where
  none : R
  one  : R
--  tons : R -- Add if !_ type is introduced.
             -- Left as an exercise

-- Context
Ctx = List Ty

-- Multiplicities of the context
data M : Ctx  Set where
   []  : M []
   __ : R  {t : Ty}  {ts : Ctx}  M ts  M (t ∷ ts) 

infixr 5 __

-- Variable of type t
data Var (t : Ty) : (Γ : Ctx)  M Γ  M Γ  Set where
  -- variable consumes multiplicity
  zero  :  {Γ m}
     Var t (t ∷ Γ) (one ∷ m) (none ∷ m)
  -- somewhere else in the context
  succ  :  {t′ Γ m n p}
     Var t Γ n p
     Var t (t′ ∷ Γ) (m ∷ n) (m ∷ p)

data Term : (Γ : Ctx)  M Γ  M Γ  Ty  Set where
  var :  {a Γ m n}
     Var a Γ m n
     Term Γ m n a

  -- linear implication
  app :  {a b Γ m n p}
     Term Γ m n (a ⊸ b)
     Term Γ n p a
     Term Γ m p b
  lam :  {a b Γ m n}
     Term (a ∷ Γ) (one ∷ m) (none ∷ n) b
     Term Γ m n (a ⊸ b)

  -- tensor (pair)
  tensI :  {a b Γ m n p}
     Term Γ m n a
     Term Γ n p b
     Term Γ m p (a ⊗ b)
  tensE :  {a b c Γ m n p}
     Term Γ m n (a ⊗ b)
     Term (a ∷ b ∷ Γ) (one ∷ one ∷ n) (none ∷ none ∷ p) c
     Term Γ m p c

-- Variable helpers
var0 :  {a Γ m}  Term (a ∷ Γ) (one ∷ m) (none ∷ m) a
var0 = var zero

var1 :  {a x Γ m xᵣ}
      Term
       (x ∷ a ∷ Γ)
       (xᵣ ∷ one ∷ m)
       (xᵣ ∷ none ∷ m)
       a
var1 = var (succ zero)

var2 :  {a x y Γ m xᵣ yᵣ}
      Term
       (x ∷ y ∷ a ∷ Γ)
       (xᵣ ∷ yᵣ ∷ one ∷ m)
       (xᵣ ∷ yᵣ ∷ none ∷ m)
       a
var2 = var (succ (succ zero))

var3 :  {a x y z Γ m xᵣ yᵣ zᵣ}
      Term (x ∷ y ∷ z ∷ a ∷ Γ)
       (xᵣ ∷ yᵣ ∷ zᵣ ∷ one ∷ m)
       (xᵣ ∷ yᵣ ∷ zᵣ ∷ none ∷ m)
       a
var3 = var (succ (succ (succ zero)))

--  Examples

ClosedTerm = Term [] [] []

-- (A ⊸ B ⊸ C) ⊸ (B ⊸ A ⊸ C)
-- or using naturals for atomic propositions:
-- (0 ⊸ 1 ⊸ 2) ⊸ (1 ⊸ 0 ⊸ 2)
--
-- λ f x y ⊸ f y x
exFlip : ClosedTerm ((A 0 ⊸ A 1 ⊸ A 2)(A 1 ⊸ A 0 ⊸ A 2))
exFlip = lam (lam (lam (app (app var2 var0) var1)))

-- λ f x y ⊸ f (x , y)
exCurry : ClosedTerm ((A 0 ⊗ A 1 ⊸ A 2)(A 0 ⊸ A 1 ⊸ A 2))
exCurry = lam (lam (lam (app var2 (tensI var1 var0))))

-- λ f p ⊸ let (x , y) = p in f x y
exUncurry : ClosedTerm ((A 0 ⊸ A 1 ⊸ A 2) ⊸ A 0 ⊗ A 1 ⊸ A 2)
exUncurry = lam (lam (tensE var0 (app (app var3 var0) var1)))

-- type error example:
--
-- We cannot write
-- λ f x ⊸ f x x
-- (but we can in STLC: λ f x → f x x)
exJoin : ClosedTerm ((A 0 ⊸ A 0 ⊸ A 1) ⊸ A 0 ⊸ A 1)
exJoin = lam (lam (app (app var1 var0) {!!}))
-- Goal:
--
-- Term
--   (A 0 ∷ (A 0 ⊸ A 0 ⊸ A 1) ∷ [])
--   (none ∷ none ∷ [])
--   (none ∷ none ∷ [])
--   (A 0)
Site proudly generated by Hakyll