Syntax.agda

open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
open import Data.Fin.Base as Fin using (Fin; zero; suc)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)

module Syntax where

module Lambda where
  -- The variable keyword lets you introduce conventions
  -- E.g. if n is mentioned anywhere without being bound it refers to a ℕ
  variable
    n : ℕ


  -- Example syntax for the lambda calculus
  -- The Expr type is indexed by the number of free variables
  -- E.g. Expr n is an expression that can refer to n free variables
  data Expr : ℕ → Set where

    -- In an expression Expr n, var can refer to n many variables
    -- Fin n is a type with n distinct elements
    ‵_ : Fin n → Expr n

    -- Function abstraction, where we introduce a new binder
    -- Let us say the expression λx.e is of type Expr n
    -- The lambda abstraction λx. introduces a new variable
    -- The inner expression e is therefore of type Expr (suc n)
    ‵λ : Expr (suc n) → Expr n

    -- Function application, where we apply one expression to another
    _‵∙_ : Expr n → Expr n → Expr n


  -- Types for the lambda calculus
  -- ‵⊤ is an arbitrary base type, ‵⇒ is the function type
  data Type : Set where
    ‵⊤ : Type
    _‵⇒_ : Type → Type → Type


  -- A typing context Γ of type Ctx n is an association of de Bruijn indices with types
  Ctx : ℕ → Set
  Ctx = Vec Type

  variable
    s t : Type
    f e : Expr n
    Γ : Ctx n
    i : Fin n

  -- A selection of type Γ ∋ i ∶ t models the fact that in Γ the variable with index i has type t
  data _∋_∶_ : Ctx n → Fin n → Type → Set where
    zero : (t ∷ Γ) ∋ zero    ∶ t
    suc  :      Γ  ∋      i  ∶ t
        → (s ∷ Γ) ∋ (suc i) ∶ t

  -- A well typedness predicate
  -- A typing derivation of type Γ ⊢ e models the fact that e is well typed under context Γ
  -- Notice that the context has to be as big as the number of free variables in the expression
  -- I.e. for every free variable the expression might refer to, we have a type
  infix 4 _⊢_∶_
  data _⊢_∶_ : Ctx n → Expr n → Type → Set where
    var : Γ ∋   i ∶ t
        → Γ ⊢ ‵ i ∶ t

    abs : s ∷ Γ ⊢    e ∶ t
        →     Γ ⊢ ‵λ e ∶ s ‵⇒ t

    app : Γ ⊢ f      ∶ s ‵⇒ t
        → Γ ⊢ e      ∶ s
        → Γ ⊢ f ‵∙ e ∶ t


-- The idea is to do something similar but for the linear π-calculus.
-- The syntax is modelled similarly, though of course different constructors must be used
-- (process termination, scope restriction, send, receive, parallel composition).
-- Additionally, because we want to support at least composite product types,
-- we need a small expression language that lets us pair up and project out things.
--
-- The expression language needs to be able to:
--   - select a free variable
--   - project out the left hand side of a pair
--   - project out the right hand side of a pair
--   - create a new pair
--
-- The process language needs to be able to:
--   - terminate a process
--   - create a new channel
--   - send over a value (selected using the expression language) over a channel
--     (selected using the expression langauge) and continuing
--   - receiving over a channel
--   - composing two processes in parallel
--
-- Each of these pieces of syntax (the variable selection, the expression language,
-- the process language) needs an accompanying well typedness relation, like _∋_∶_ and _⊢_∶_.
-- One difference to note is that processes are untyped, so while expressions will have a type
-- as part of the relation (_⊢_∶_), processes will not (_⊢_).
-- However, things get considerably trickier when dealing with the linear π-calculus,
-- because we need split up and keep track of linear resources.
--
-- The types for the linear π-calculus could look something like this:

-- 0∙ means cannot be used
-- 1∙ means has to be used exactly once
-- ω∙ means can be used as much as we like
data Multiplicity : Set where
  0∙ 1∙ ω∙ : Multiplicity

-- ‵⊤ is an arbitrary base type
-- ‵# i o t is a channel type where
-- i is the input multiplicity,
-- o is the output multiplicity,
-- t is the type of the payload
data Type : Set where
  ‵⊤ : Type
  ‵# : Multiplicity → Multiplicity → Type → Type

Ctx : ℕ → Set
Ctx = Vec Type

variable
  n : ℕ
  s t r : Type
  Γ Δ Θ : Ctx n
  xᵢ yᵢ zᵢ xₒ yₒ zₒ : Multiplicity

-- Once we have those we can now define how to split up resources
-- We first define how to split up multiplicities
data _≔_+₀_ : Multiplicity → Multiplicity → Multiplicity → Set where
  zero   : 0∙ ≔ 0∙ +₀ 0∙
  left   : 1∙ ≔ 1∙ +₀ 0∙
  right  : 1∙ ≔ 0∙ +₀ 1∙
  shared : ω∙ ≔ ω∙ +₀ ω∙

-- Then we lift that to types
data _≔_+₁_ : Type → Type → Type → Set where
  top  : ‵⊤ ≔ ‵⊤ +₁ ‵⊤
  chan : xᵢ         ≔ yᵢ         +₀ zᵢ
       → xₒ         ≔ yₒ         +₀ zₒ
       → ‵# xᵢ xₒ t ≔ ‵# yᵢ yₒ t +₁ ‵# zᵢ zₒ t

-- And then to contexts
data _≔_+₂_ : Ctx n → Ctx n → Ctx n → Set where
  []  : [] ≔ [] +₂ []
  _∷_ : s       ≔ t       +₁ r
      → Γ       ≔ Δ       +₂ Θ
      → (s ∷ Γ) ≔ (t ∷ Δ) +₂ (r ∷ Θ)

-- Now, let's say we have a datatype Proc n for processes with n free variables
-- It has many things (process termination, scope restriction, send, receive, parallel composition)
-- but here I will focus on parallel composition to show how the context splitting works
-- I leave the rest as an exercise :p
data Proc : ℕ → Set where
  _∥_ : Proc n → Proc n → Proc n

variable
  P Q : Proc n

-- The typing rule would then use context splitting as follows
data _⊢_ : Ctx n → Proc n → Set where
  par : Γ ≔ Δ +₂ Θ
      → Δ ⊢ P
      → Θ ⊢ Q
      → Γ ⊢ (P ∥ Q)

-- Hope this helps!