Pattern Matching Operads

Pattern.idr

-- So, let's say we have our data type of terms
data Expr : (Nat -> Type) -> Nat -> Type where 
  Var : Fin n -> Expr f n
  In : f n -> (Fin n -> Expr f m) -> Expr f m 

-- And we have the data types of patterns. So far they're identical, but they'll diverge later. 
data Pat : (Nat -> Type) -> Nat -> Type where 
  PVar : Fin n -> Pat f n
  Nest : f n -> (Fin n -> Pat f m) -> Pat f m 

-- We also have a combinator that combines a term and a pattern, if they have the same number of variables
data Match : (Nat -> Type) -> Type where 
  M : Pat f m -> Expr f m -> Match f 

-- Example signature, Addition.
data NatSig : Nat -> Type where 
  Zero : NatSig 0 
  Succ : NatSig 1 
  Add  : NatSig 2 

-- Our goal is to implement addition, ie we will represent this pattern match: 
add : (Nat, Nat) -> Nat
add tup = case tup of 
  (Z, n) => n 
  (S n, m) => add (n, S m) 

-- For simplicity, we represent `Add` as a constructor, rather than a tuple. But tuples can be added.

-- First we represent the patterns, ie the things on the left hand side of =>

-- Add Z n => ...
exPat1 : Pat NatSig 1
exPat1 = Nest Add (\i => case i of
  FZ => Nest Zero absurd -- first argument to Add is Zero
  FS FZ => PVar FZ)      -- second argument to Add is `n`, which is bound to a variable FZ

-- Add (S n) m => ...
exPat2 : Pat NatSig 2
exPat2 = Nest Add (\i => case i of 
  FZ =>  Nest Succ (\i => case i of -- first argument to Add is (S n), so we unwrap S
    FZ => PVar FZ) -- and bind `n` to the variable FZ
  FS FZ => PVar $ FS FZ) -- the second argument `m` is bound to the variable FS FZ

-- Now we represent the right hand side of a case statement.
-- ... => n
exUse1 : Expr NatSig 1
exUse1 = Var FZ -- we return the variable unused

-- ... => Add n (S m)
exUse2 : Expr NatSig 2 
exUse2 = In Add (\i => case i of -- we return `Add` applied to two arguments
  FZ => Var FZ -- the first is the variable FZ
  FS FZ => In Succ (\i => case i of -- the second is the constructor S,  
    FZ => (Var $ FS FZ))) -- which is applied to the variable FS FZ

-- Finally, we combine the pattern and the expression using it 
-- Add Z n => n
exMatch1 : Match NatSig 
exMatch1 = M exPat1 exUse1

-- Add (S m) n => Add n (S m)
exMatch2 : Match NatSig 
exMatch2 = M exPat2 exUse2