Labelled types demo ala "The view from the left" by McBride & McKinna. Labels are a cheap alternative to dependent pattern matching. You can program with eliminators but the type of your goal reflects the dependent pattern match equation that you would have done. Inductive hypotheses are also labeled, and hence you get more type safety from usin…

LabelledAdd1.agda

open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where

----------------------------------------------------------------------

add : (m n : ℕ) → ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' → ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)
  (return n) -- Goal 1
  (λ m' ih → return (suc (call ih))) -- Goal 2
  m

{-

Goal 1: ⟨ "add" ∙ 0 ∙ n ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

Goal 2: ⟨ "add" ∙ suc m' ∙ n ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
ih : ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩
m' : ℕ
n  : ℕ
m  : ℕ

-}

----------------------------------------------------------------------

LabelledAdd2.agda

open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd2 where

----------------------------------------------------------------------

Add : (m n : ℕ) → Set
Add m n = ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩

add : (m n : ℕ) → Add m n
add m = elimℕ (Add m)
  (return zero) -- Goal 1
  (λ n ih → return (suc (call ih))) -- Goal 2

{-

Goal 1: ⟨ "add" ∙ m ∙ 0 ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
m : ℕ

Goal 2: ⟨ "add" ∙ m ∙ suc n ∙ ε ∶ ℕ ⟩
————————————————————————————————————————————————————————————
ih : ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
n  : ℕ
m  : ℕ

-}

----------------------------------------------------------------------

LabelledTypes.agda

{-# OPTIONS --type-in-type #-}
open import Data.Nat
open import Data.String
open import Function
module LabelledTypes where

----------------------------------------------------------------------

elimℕ : (P : ℕ → Set)
  (pz : P zero)
  (ps : (m : ℕ) → P m → P (suc m))
  (n : ℕ)
  → P n
elimℕ P pz ps zero = pz
elimℕ P pz ps (suc n) = ps n (elimℕ P pz ps n)

----------------------------------------------------------------------

infixr 4 _∙_
data Spine : Set where
  ε : Spine
  _∙_ : {A : Set} → A → Spine → Spine

data Label : Set where
  _∙_ : String → Spine → Label

data ⟨_∶_⟩ : Label → Set → Set where
  return : ∀{l A} → A → ⟨ l ∶ A ⟩

call : {l : Label} {A : Set} → ⟨ l ∶ A ⟩ → A
call (return a) = a

----------------------------------------------------------------------