Fun with McBride's General monad

general.agda

module general where
open import Function
import Data.Nat      as N
import Data.Fin      as F
import Data.Maybe    as M
import Relation.Nullary as R

data General (S : Set)(T : S -> Set)(X : Set) : Set where
  !!    : X -> General S T X
  _??_  : (s : S) -> (T s -> General S T X) -> General S T X
infixr 5 _??_

fold : ∀ {ℓ S T X} {Y : Set ℓ}
     → (X → Y) → ((s : S) → (T s → Y) → Y)
     → General S T X → Y
fold r b (!! x) = r x
fold r b (s ?? f) = b s λ ts → fold r b (f ts)

_>>=_ : ∀ {S T X Y} → General S T X → (X → General S T Y) → General S T Y
g >>= f = fold f _??_ g

call : ∀ {S T} → (s : S) → General S T (T s)
call s = s ?? !!

_PiG_ : (S : Set)(T : S → Set) → Set
_PiG_ S T = (s : S) → General S T (T s)

expand : ∀ {S T X} → (S PiG T)
       → General S T X → General S T X
expand f = fold !! (_>>=_ ∘ f)

data Λ : N.ℕ → Set where
  Var : {n : N.ℕ} → F.Fin n → Λ n
  App : {n : N.ℕ} → Λ n → Λ n → Λ n
  Lam : {n : N.ℕ} → Λ (N.suc n) → Λ n

bump : {n : N.ℕ} → N.ℕ → Λ n → Λ (N.suc n)
bump m (Var {n} x) with n N.≤? m
... | R.yes _ = Var (F.inject₁ x)
... | R.no _  = Var (F.suc x)
bump m (App l l₁) = App (bump m l) (bump m l₁)
bump m (Lam l) = Lam (bump (N.suc m) l)

subst : {n : N.ℕ} → Λ n → Λ (N.suc n) → Λ n
subst new (Var F.zero) = new
subst new (Var (F.suc x)) = Var x
subst new (App l l₁) = App (subst new l) (subst new l₁)
subst new (Lam l) = Lam (subst (bump N.zero new) l)

eval : {n : N.ℕ} → Λ n PiG λ _ → Λ n
eval (Var x) = !! (Var x)
eval {n} (App l₁ l₂) = call l₁ >>= go
  where go : Λ n PiG λ _ → Λ n
        go (Var x)     = call l₂ >>= λ l₂' → !! (App (Var x) l₂')
        go (App _ _) = call (App l₁ l₂) -- Impossible
        go (Lam body)    = call (subst l₂ body)
eval (Lam l) = !! (Lam l)

{-# NON_TERMINATING #-}
runDammit : {X S : Set}{T : S → Set} → S PiG T → General S T X → X
runDammit pig (!! x) = x
runDammit pig rest   = runDammit pig (expand pig rest)